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

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

  1. Bayer, Jonas; David, Marco; Pal, Abhik; Stock, Benedikt: Beginners’ quest to formalize mathematics: a feasibility study in Isabelle (2019)
  2. Bentkamp, Alexander; Blanchette, Jasmin Christian; Klakow, Dietrich: A formal proof of the expressiveness of deep learning (2019)
  3. Charguéraud, Arthur; Pottier, François: Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits (2019)
  4. Fuenmayor, David; Benzmüller, Christoph: Computational hermeneutics: an integrated approach for the logical analysis of natural-language arguments (2019)
  5. Immler, Fabian; Traut, Christoph: The flow of ODEs: formalization of variational equation and Poincaré map (2019)
  6. Lammich, Peter: Refinement to imperative HOL (2019)
  7. Lammich, Peter; Lochbihler, Andreas: Automatic refinement to efficient data structures: a comparison of two approaches (2019)
  8. Lammich, Peter; Sefidgar, S. Reza: Formalizing network flow algorithms: a refinement approach in Isabelle/HOL (2019)
  9. Li, Wenda; Passmore, Grant Olney; Paulson, Lawrence C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (2019)
  10. Marmsoler, Diego; Gidey, Habtom Kashay: Interactive verification of architectural design patterns in FACTum (2019)
  11. Möller, Bernhard: Geographic wayfinders and space-time algebra (2019)
  12. Nipkow, Tobias; Brinkop, Hauke: Amortized complexity verified (2019)
  13. Sulzmann, Martin; Thiemann, Peter: Derivatives and partial derivatives for regular shuffle expressions (2019)
  14. Wenzel, Makarius: Interaction with formal mathematical documents in Isabelle/PIDE (2019)
  15. Bancerek, Grzegorz; Byliński, Czesław; Grabowski, Adam; Korniłowicz, Artur; Matuszewski, Roman; Naumowicz, Adam; Pąk, Karol: The role of the Mizar mathematical library for interactive proof development in Mizar (2018)
  16. Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph: A verified SAT solver framework with learn, forget, restart, and incrementality (2018)
  17. Breitner, Joachim: The adequacy of Launchbury’s natural semantics for lazy evaluation (2018)
  18. Brunner, Julian; Lammich, Peter: Formal verification of an executable LTL model checker with partial order reduction (2018)
  19. Clochard, Martin; Gondelman, Léon; Pereira, Mário: The matrix reproved (verification pearl) (2018)
  20. Diekmann, Cornelius; Hupel, Lars; Michaelis, Julius; Haslbeck, Maximilian; Carle, Georg: Verified iptables firewall analysis and verification (2018)

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