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 139 articles , 1 standard article )

Showing results 1 to 20 of 139.
Sorted by year (citations)

1 2 3 ... 5 6 7 next

  1. Basin, David A.; Lochbihler, Andreas; Sefidgar, S. Reza: CryptHOL: game-based proofs in higher-order logic (2020)
  2. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
  3. Bisping, Benjamin; Nestmann, Uwe; Peters, Kirstin: Coupled similarity: the first 32 years (2020)
  4. Divasón, Jose; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa: A verified implementation of the Berlekamp-Zassenhaus factorization algorithm (2020)
  5. Foster, Simon; Cavalcanti, Ana; Canham, Samuel; Woodcock, Jim; Zeyda, Frank: Unifying theories of reactive design contracts (2020)
  6. Gouëzel, Sébastien; Karlsson, Anders: Subadditive and multiplicative ergodic theorems (2020)
  7. Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa: A verified implementation of algebraic numbers in Isabelle/HOL (2020)
  8. Kirchner, Daniel; Benzmüller, Christoph; Zalta, Edward N.: Mechanizing Principia Logico-Metaphysica in functional type-theory (2020)
  9. Li, Wenda; Paulson, Lawrence C.: Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL (2020)
  10. Bayer, Jonas; David, Marco; Pal, Abhik; Stock, Benedikt: Beginners’ quest to formalize mathematics: a feasibility study in Isabelle (2019)
  11. Bentkamp, Alexander; Blanchette, Jasmin Christian; Klakow, Dietrich: A formal proof of the expressiveness of deep learning (2019)
  12. Charguéraud, Arthur; Pottier, François: Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits (2019)
  13. Immler, Fabian; Traut, Christoph: The flow of ODEs: formalization of variational equation and Poincaré map (2019)
  14. Lammich, Peter: Refinement to imperative HOL (2019)
  15. Lammich, Peter; Lochbihler, Andreas: Automatic refinement to efficient data structures: a comparison of two approaches (2019)
  16. Lammich, Peter; Sefidgar, S. Reza: Formalizing network flow algorithms: a refinement approach in Isabelle/HOL (2019)
  17. Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (2019)
  18. Marmsoler, Diego; Gidey, Habtom Kashay: Interactive verification of architectural design patterns in FACTum (2019)
  19. Möller, Bernhard: Geographic wayfinders and space-time algebra (2019)
  20. Nipkow, Tobias; Brinkop, Hauke: Amortized complexity verified (2019)

1 2 3 ... 5 6 7 next