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

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

1 2 3 ... 7 8 9 next

  1. Ambal, Guillaume; Lenglet, Sergueï; Schmitt, Alan: (\mathrmHO\pi) in Coq (2021)
  2. Bordg, Anthony; Lachnitt, Hanna; He, Yijun: Certified quantum computation in Isabelle/HOL (2021)
  3. Butler, D.; Lochbihler, A.; Aspinall, D.; Gascón, A.: Formalising (\varSigma)-protocols and commitment schemes using crypthol (2021)
  4. Foster, Simon; Ye, Kangfeng; Cavalcanti, Ana; Woodcock, Jim: Automated verification of reactive and concurrent programs by calculation (2021)
  5. Grabowski, Adam: Automated comparative study of some generalized rough approximations (2021)
  6. Koutsoukou-Argyraki, Angeliki: Formalising mathematics -- in praxis; a mathematician’s first experiences with Isabelle/HOL and the why and how of getting started (2021)
  7. Mahboubi, Assia; Sibut-Pinote, Thomas: A formal proof of the irrationality of (\zeta(3)) (2021)
  8. Popescu, Andrei; Lammich, Peter; Hou, Ping: CoCon: a conference management system with formally verified document confidentiality (2021)
  9. Popescu, Andrei; Traytel, Dmitriy: Distilling the requirements of Gödel’s incompleteness theorems with a proof assistant (2021)
  10. Rusu, Vlad; Nowak, David: (Co)inductive proof systems for compositional proofs in reachability logic (2021)
  11. Simić, Danijela; Marić, Filip; Boutry, Pierre: Formalization of the Poincaré disc model of hyperbolic geometry (2021)
  12. Sison, Robert; Murray, Toby: Verified secure compilation for mixed-sensitivity concurrent programs (2021)
  13. Thiemann, René: A Perron-Frobenius theorem for deciding matrix growth (2021)
  14. Ballarin, Clemens: Exploring the structure of an algebra text with locales (2020)
  15. Basin, David A.; Lochbihler, Andreas; Sefidgar, S. Reza: CryptHOL: game-based proofs in higher-order logic (2020)
  16. Benzmüller, Christoph; Fuenmayor, David: Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of Gödel’s ontological argument (2020)
  17. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
  18. Bisping, Benjamin; Nestmann, Uwe; Peters, Kirstin: Coupled similarity: the first 32 years (2020)
  19. Divasón, Jose; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa: A verified implementation of the Berlekamp-Zassenhaus factorization algorithm (2020)
  20. Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias: Verified analysis of random binary tree structures (2020)

1 2 3 ... 7 8 9 next