Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. The main application is the formalization of mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware or software and proving properties of computer languages and protocols.

This software is also referenced in ORMS.

References in zbMATH (referenced in 598 articles , 1 standard article )

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

1 2 3 ... 28 29 30 next

  1. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
  2. Kaufmann, Matt; Moore, J. Strother: Limited second-order functionality in a first-order setting (2020)
  3. Lammich, Peter: Efficient verified (UN)SAT certificate checking (2020)
  4. Abel, Andreas; Allais, Guillaume; Hameer, Aliya; Pientka, Brigitte; Momigliano, Alberto; Schäfer, Steven; Stark, Kathrin: POPLMark reloaded: mechanizing proofs by logical relations (2019)
  5. Bottesch, Ralph; Haslbeck, Max W.; Thiemann, René: Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL (2019)
  6. Chan, Hing-Lun; Norrish, Michael: Classification of finite fields with applications (2019)
  7. Condoluci, Andrea; Kohlhase, Michael; Müller, Dennis; Rabe, Florian; Sacerdoti Coen, Claudio; Wenzel, Makarius: Relational data across mathematical libraries (2019)
  8. de Gouw, Stijn; de Boer, Frank S.; Bubel, Richard; Hähnle, Reiner; Rot, Jurriaan; Steinhöfel, Dominic: Verifying OpenJDK’s sort method for generic collections (2019)
  9. Eberl, Manuel: Verifying randomised social choice (2019)
  10. Färber, Michael; Kaliszyk, Cezary: Certification of nonclausal connection tableaux proofs (2019)
  11. Fuenmayor, David; Benzmüller, Christoph: Mechanised assessment of complex natural-language arguments using expressive logic combinations (2019)
  12. Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
  13. Gunther, Emmanuel; Pagano, Miguel; Sánchez Terraf, Pedro: First steps towards a formalization of forcing (2019)
  14. Kaliszyk, Cezary (ed.); Brady, Edwin (ed.); Kohlhase, Andrea (ed.); Sacerdoti Coen, Claudio (ed.): Intelligent computer mathematics. 12th international conference, CICM 2019, Prague, Czech Republic, July 8--12, 2019. Proceedings (2019)
  15. Kaliszyk, Cezary; Pąk, Karol: Semantics of Mizar as an Isabelle object logic (2019)
  16. Kunčar, Ondřej; Popescu, Andrei: A consistent foundation for Isabelle/HOL (2019)
  17. Kunčar, Ondřej; Popescu, Andrei: From types to sets by local type definition in higher-order logic (2019)
  18. Lammich, Peter; Lochbihler, Andreas: Automatic refinement to efficient data structures: a comparison of two approaches (2019)
  19. Libal, Tomer; Volpe, Marco: A general proof certification framework for modal logic (2019)
  20. Li, Li-Ming; Shi, Zhi-Ping; Guan, Yong; Zhang, Qian-Ying; Li, Yong-Dong: Formalization of geometric algebra in HOL Light (2019)

1 2 3 ... 28 29 30 next