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

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

1 2 3 ... 8 9 10 next

  1. Hirata, Michikazu; Minamide, Yasuhiko; Sato, Tetsuya: Program logic for higher-order probabilistic programs in Isabelle/HOL (2022)
  2. Huerta y Munive, Jonathan Julián; Struth, Georg: Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL (2022)
  3. Karayel, Emin; Gonzàlez, Edgar: Strong eventual consistency of the collaborative editing framework WOOT (2022)
  4. Koutsoukou-Argyraki, Angeliki; Li, Wenda; Paulson, Lawrence C.: Irrationality and transcendence criteria for infinite series in Isabelle/HOL (2022)
  5. Ambal, Guillaume; Lenglet, Sergueï; Schmitt, Alan: (\mathrmHO\pi) in Coq (2021)
  6. Bordg, Anthony; Lachnitt, Hanna; He, Yijun: Certified quantum computation in Isabelle/HOL (2021)
  7. Butler, D.; Lochbihler, A.; Aspinall, D.; Gascón, A.: Formalising (\varSigma)-protocols and commitment schemes using crypthol (2021)
  8. Cranch, James; Doherty, Simon; Struth, Georg: Convolution and concurrency (2021)
  9. De Lon, Adrian; Koepke, Peter; Lorenzen, Anton; Marti, Adrian; Schütz, Marcel; Sturzenhecker, Erik: Beautiful formalizations in Isabelle/Naproche (2021)
  10. Edmonds, Chelsea; Paulson, Lawrence C.: A modular first formalisation of combinatorial design theory (2021)
  11. Foster, Simon; Nemouchi, Yakoub; Gleirscher, Mario; Wei, Ran; Kelly, Tim: Integration of formal proof into unified assurance cases with Isabelle/SACM (2021)
  12. Foster, Simon; Ye, Kangfeng; Cavalcanti, Ana; Woodcock, Jim: Automated verification of reactive and concurrent programs by calculation (2021)
  13. From, Asta Halkjær: Formalized soundness and completeness of epistemic logic (2021)
  14. From, Asta Halkjær; Eschen, Agnes Moesgård; Villadsen, Jørgen: Formalizing axiomatic systems for propositional logic in Isabelle/HOL (2021)
  15. Grabowski, Adam: Automated comparative study of some generalized rough approximations (2021)
  16. Holliday, Wesley H.; Norman, Chase; Pacuit, Eric: Voting theory in the Lean theorem prover (2021)
  17. Holub, Štěpán; Starosta, Štěpán: Lyndon words formalized in Isabelle/HOL (2021)
  18. Iordache, Viorel; Ciobâcă, Ştefan: Verifying the conversion into CNF in dafny (2021)
  19. Koutsoukou-Argyraki, Angeliki: Formalising mathematics -- in praxis; a mathematician’s first experiences with Isabelle/HOL and the why and how of getting started (2021)
  20. Li, Liyi; Gunter, Elsa L.: A complete semantics of (\mathbbK) and its translation to Isabelle (2021)

1 2 3 ... 8 9 10 next