Isabelle

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

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

1 2 3 ... 19 20 21 next

  1. Aransay, Jesús; Divasón, Jose: A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem (2017)
  2. Bowles, Juliana; Caminati, Marco B.: A verified algorithm enumerating event structures (2017)
  3. Felgenhauer, Bertram; Thiemann, René: Reachability, confluence, and termination analysis with state-compatible automata (2017)
  4. Glück, Roland: Algebraic investigation of connected components (2017)
  5. Kaliszyk, Cezary; Pąk, Karol: Presentation and manipulation of Mizar properties in an Isabelle object logic (2017)
  6. Kunčar, Ondřej; Popescu, Andrei: Comprehending Isabelle/HOL’s consistency (2017)
  7. Lampropoulos, Leonidas; Gallois-Wong, Diane; Hriţcu, Cătălin; Hughes, John; Pierce, Benjamin C.; Xia, Li-yao: Beginner’s luck: a language for property-based generators (2017)
  8. Maletzky, Alexander; Windsteiger, Wolfgang: The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema (2017)
  9. Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian: Classification of alignments between concepts of formal mathematical systems (2017)
  10. Rabe, Florian: Morphism axioms (2017)
  11. Stucke, Insa: Reasoning about cardinalities of relations with applications supported by proof assistants (2017)
  12. Aransay, Jesús; Divasón, Jose: Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL (2016)
  13. Arthan, Rob: On definitions of constants and types in HOL (2016)
  14. Bengtson, Jesper; Parrow, Joachim; Weber, Tjark: Psi-calculi in Isabelle (2016)
  15. Bettini, Lorenzo: Implementing type systems for the IDE with Xsemantics (2016)
  16. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  17. Calude, Cristian S.; Thompson, Declan: Incompleteness, undecidability and automated proofs (invited talk) (2016)
  18. Dougherty, Daniel J.; de’Liguoro, Ugo; Liquori, Luigi; Stolze, Claude: A realizability interpretation for intersection and union types (2016)
  19. Kerber, Manfred; Lange, Christoph; Rowat, Colin: An introduction to mechanized reasoning (2016)
  20. Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott: Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (2016)

1 2 3 ... 19 20 21 next