Archive Formal Proofs

Isabelle’s Archive of Formal Proofs (AFP): Mining the Archive of Formal Proofs. The Archive of Formal Proofs is a vast collection of computer-checked proofs developed using the proof assistant Isabelle. We perform an in-depth analysis of the archive, looking at various properties of the proof developments, including size, dependencies, and proof style. This gives some insights into the nature of formal proofs.


References in zbMATH (referenced in 178 articles , 1 standard article )

Showing results 141 to 160 of 178.
Sorted by year (citations)

previous 1 2 3 ... 6 7 8 9 next

  1. Omodeo, Eugenio G.; Tomescu, Alexandru I.: Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets (2014)
  2. Wu, Chunhan; Zhang, Xingyuan; Urban, Christian: A formalisation of the Myhill-Nerode theorem based on regular expressions (2014)
  3. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2013)
  4. Cavalcanti, Ana; Mota, Alexandre; Woodcock, Jim: Simulink timed models for program verification (2013)
  5. Sabel, David; Schmidt-Schauß, Manfred: A two-valued logic for properties of strict functional programs allowing partial functions (2013)
  6. Sternagel, Christian: Proof pearl: A mechanized proof of GHC’s mergesort (2013)
  7. Wenzel, Makarius: Shared-memory multiprocessing for interactive theorem proving (2013)
  8. Armstrong, Alasdair; Struth, Georg: Automated reasoning in higher-order regular algebra (2012)
  9. Bourke, Timothy; Daum, Matthias; Klein, Gerwin; Kolanski, Rafal: Challenges and experiences in managing large-scale proofs (2012)
  10. Hofheinz, Dennis; Kiltz, Eike: Programmable hash functions and their applications (2012)
  11. Krauss, Alexander; Nipkow, Tobias: Proof Pearl: regular expression equivalence and relation algebra (2012)
  12. Lammich, Peter; Tuerk, Thomas: Applying data refinement for monadic programs to Hopcroft’s algorithm (2012)
  13. Preoteasa, Viorel; Back, Ralph-Johan: Invariant diagrams with data refinement (2012)
  14. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2011)
  15. Gammie, Peter: Verified synthesis of knowledge-based programs in finite synchronous environments (2011)
  16. Horozal, Fulya; Iacob, Alin; Jucovschi, Constantin; Kohlhase, Michael; Rabe, Florian: Combining source, content, presentation, narration, and relational representation (2011)
  17. Jiang, Dongchen; Nipkow, Tobias: Proof pearl: the marriage theorem (2011)
  18. Joye, Marc: How (not) to design strong-RSA signatures (2011)
  19. Lochbihler, Andreas; Bulwahn, Lukas: Animating the formalised semantics of a Java-like language (2011)
  20. Marić, Filip; Janičić, Predrag: Formalization of abstract state transition systems for SAT (2011)

previous 1 2 3 ... 6 7 8 9 next