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

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

  1. Blanchette, Jasmin Christian; Haslbeck, Maximilian; Matichuk, Daniel; Nipkow, Tobias: Mining the Archive of Formal Proofs (2015)
  2. Felgenhauer, Bertram; Middeldorp, Aart; Zankl, Harald; Van Oostrom, Vincent: Layer systems for proving confluence (2015)
  3. Foster, Simon; Struth, Georg: On the fine-structure of regular algebra (2015)
  4. Jacobsen, Charles; Solovyev, Alexey; Gopalakrishnan, Ganesh: A parameterized floating-point formalizaton in HOL Light (2015)
  5. Kerber, Manfred (ed.); Carette, Jacques (ed.); Kaliszyk, Cezary (ed.); Rabe, Florian (ed.); Sorge, Volker (ed.): Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13--17, 2015, Proceedings (2015)
  6. Marić, Filip; Petrović, Danijela: Formalizing complex plane geometry (2015)
  7. Paulson, Lawrence C.: A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle (2015)
  8. Schäge, Sven: Tight security for signature schemes without random oracles (2015)
  9. Sternagel, Christian; Thiemann, René: A framework for developing stand-alone certifiers (2015)
  10. Traytel, Dmitriy; Nipkow, Tobias: Verified decision procedures for MSO on words based on derivatives of regular expressions (2015)
  11. Wenzel, Makarius: Interactive theorem proving from the perspective of Isabelle/Isar (2015)
  12. Zankl, Harald; Felgenhauer, Bertram; Middeldorp, Aart: Labelings for decreasing diagrams (2015)
  13. Alkassar, Eyad; Böhme, Sascha; Mehlhorn, Kurt; Rizkallah, Christine: A framework for the verification of certifying computations (2014)
  14. Bella, Giampaolo: Inductive study of confidentiality: for everyone (2014) ioport
  15. Blanchette, Jasmin Christian; Hölzl, Johannes; Lochbihler, Andreas; Panny, Lorenz; Popescu, Andrei; Traytel, Dmitriy: Truly modular (co)datatypes for Isabelle/HOL (2014)
  16. Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy: Unified classical logic completeness. A coinductive pearl (2014)
  17. Caminati, Marco B.; Kerber, Manfred; Lange, Christoph; Rowat, Colin: Set theory or higher order logic to represent auction concepts in Isabelle? (2014)
  18. Grabowski, Adam: Cauchy mean theorem (2014)
  19. Jakob von Raumer: The Jordan-Hölder Theorem (2014) not zbMATH
  20. Lammich, Peter: Verified efficient implementation of Gabow’s strongly connected component algorithm (2014)

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