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 161 to 178 of 178.
Sorted by year (citations)

previous 1 2 3 ... 7 8 9

  1. Nipkow, Tobias: Verified efficient enumeration of plane graphs modulo isomorphism (2011)
  2. Sternagel, Christian; Thiemann, René: Formalizing Knuth-Bendix orders and Knuth-Bendix completion (2011)
  3. Hales, Thomas C.; Harrison, John; McLaughlin, Sean; Nipkow, Tobias; Obua, Steven; Zumkeller, Roland: A revision of the proof of the Kepler conjecture (2010)
  4. Krauss, Alexander: Partial and nested recursive function definitions in higher-order logic (2010)
  5. Marić, Filip: Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL (2010)
  6. Basin, David; Capkun, Srdjan; Schaller, Patrick; Schmidt, Benedikt: Let’s get physical: Models and methods for real-world security protocols (2009)
  7. Berghofer, Stefan; Reiter, Markus: Formalizing the logic-automaton connection (2009)
  8. Blanchette, Jasmin Christian: Proof pearl: Mechanizing the textbook proof of Huffman’s algorithm (2009)
  9. Calude, Cristian S.; Müller, Christine: Formal proof: reconciling correctness and understanding (2009)
  10. Dabrowski, Frédéric; Pichardie, David: A certified data race analysis for a Java-like language (2009)
  11. Klein, Gerwin: Operating system verification---an overview (2009)
  12. Lochbihler, Andreas: Formalising FinFuns -- generating code for functions as data from Isabelle/HOL (2009)
  13. Marić, Filip: Formalization and implementation of modern SAT solvers (2009)
  14. Nipkow, Tobias: Social choice theory in HOL. Arrow and Gibbard-Satterthwaite (2009)
  15. Lammich, Peter; Müller-Olm, Markus: Conflict analysis of programs with procedures, dynamic thread creation, and monitors (2008)
  16. Owens, Scott; Slind, Konrad: Adapting functional programs to higher order logic (2008)
  17. Barsotti, Damián; Nieto, Leonor Prensa; Tiu, Alwen: Verification of clock synchronization algorithms: experiments on a combination of deductive tools (2007)
  18. Reichbach, J.: Some characterizations of the first-order functional calculus (1963)

previous 1 2 3 ... 7 8 9