Isabelle/HOL

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.


References in zbMATH (referenced in 981 articles , 2 standard articles )

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

1 2 3 ... 48 49 50 next

  1. Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Waldmann, Uwe: Superposition for lambda-free higher-order logic (2021)
  2. Butler, D.; Lochbihler, A.; Aspinall, D.; Gascón, A.: Formalising (\varSigma)-protocols and commitment schemes using crypthol (2021)
  3. Holub, Štěpán; Starosta, Štěpán: Binary intersection formalized (2021)
  4. Hóu, Zhé; Sanan, David; Tiu, Alwen; Liu, Yang; Hoa, Koh Chuen; Dong, Jin Song: An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model (2021)
  5. Koutsoukou-Argyraki, Angeliki: Formalising mathematics -- in praxis; a mathematician’s first experiences with Isabelle/HOL and the why and how of getting started (2021)
  6. Mahboubi, Assia; Sibut-Pinote, Thomas: A formal proof of the irrationality of (\zeta(3)) (2021)
  7. Maletzky, Alexander: A generic and executable formalization of signature-based Gröbner basis algorithms (2021)
  8. Reed Oei, Dun Ma, Christian Schulz, Philipp Hieronymi: Pecan: An Automated Theorem Prover for Automatic Sequences using Büchi Automata (2021) arXiv
  9. Rusu, Vlad; Nowak, David: (Co)inductive proof systems for compositional proofs in reachability logic (2021)
  10. Simić, Danijela; Marić, Filip; Boutry, Pierre: Formalization of the Poincaré disc model of hyperbolic geometry (2021)
  11. Abrahamsson, Oskar: A verified proof checker for higher-order logic (2020)
  12. Abrahamsson, Oskar; Ho, Son; Kanabar, Hrutvik; Kumar, Ramana; Myreen, Magnus O.; Norrish, Michael; Tan, Yong Kiam: Proof-producing synthesis of CakeML from monadic HOL functions (2020)
  13. Albert, Elvira; Bezirgiannis, Nikolaos; De Boer, Frank; Martin-Martin, Enrique: A formal, resource consumption-preserving translation from actors with cooperative scheduling to Haskell (2020)
  14. Ballarin, Clemens: Exploring the structure of an algebra text with locales (2020)
  15. Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
  16. Basin, David A.; Lochbihler, Andreas; Sefidgar, S. Reza: CryptHOL: game-based proofs in higher-order logic (2020)
  17. Benzmüller, Christoph; Fuenmayor, David: Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of Gödel’s ontological argument (2020)
  18. Benzmüller, Christoph; Parent, Xavier; van der Torre, Leendert: Designing normative theories for ethical and legal reasoning: \textscLogiKEyframework, methodology, and tool support (2020)
  19. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
  20. Berghammer, Rudolf; Furusawa, Hitoshi; Guttmann, Walter; Höfner, Peter: Relational characterisations of paths (2020)

1 2 3 ... 48 49 50 next