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 1018 articles , 2 standard articles )

Showing results 21 to 40 of 1018.
Sorted by year (citations)

previous 1 2 3 4 ... 49 50 51 next

  1. Kastenbaum, Stéphane; Boyer, Benoît; Talpin, Jean-Pierre: A mechanically verified theory of contracts (2021)
  2. Kohlhase, Michael; Rabe, Florian: Experiences from exporting major proof assistant libraries (2021)
  3. Koutsoukou-Argyraki, Angeliki: Formalising mathematics -- in praxis; a mathematician’s first experiences with Isabelle/HOL and the why and how of getting started (2021)
  4. Koutsoukou-Argyraki, Angeliki: On preserving the computational content of mathematical proofs: toy examples for a formalising strategy (2021)
  5. Mahboubi, Assia; Sibut-Pinote, Thomas: A formal proof of the irrationality of (\zeta(3)) (2021)
  6. Maletzky, Alexander: A generic and executable formalization of signature-based Gröbner basis algorithms (2021)
  7. Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Zohar, Yoni; Barrett, Clark; Tinelli, Cesare: Towards satisfiability modulo parametric bit-vectors (2021)
  8. Nipkow, Tobias; Roßkopf, Simon: Isabelle’s metalogic: formalization and proof checker (2021)
  9. Paulson, Lawrence C.: Ackermann’s function in iterative form: a proof assistant experiment (2021)
  10. Popescu, Andrei; Lammich, Peter; Hou, Ping: CoCon: a conference management system with formally verified document confidentiality (2021)
  11. Popescu, Andrei; Traytel, Dmitriy: Distilling the requirements of Gödel’s incompleteness theorems with a proof assistant (2021)
  12. Reed Oei, Dun Ma, Christian Schulz, Philipp Hieronymi: Pecan: An Automated Theorem Prover for Automatic Sequences using Büchi Automata (2021) arXiv
  13. Rusu, Vlad; Nowak, David: (Co)inductive proof systems for compositional proofs in reachability logic (2021)
  14. Siek, Jeremy G.; Chen, Tianyu: Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi (2021)
  15. Simić, Danijela; Marić, Filip; Boutry, Pierre: Formalization of the Poincaré disc model of hyperbolic geometry (2021)
  16. Sison, Robert; Murray, Toby: Verified secure compilation for mixed-sensitivity concurrent programs (2021)
  17. Steen, Alexander; Benzmüller, Christoph: Extensional higher-order paramodulation in Leo-III (2021)
  18. Streit, David: Experiments in causality and STIT (2021)
  19. Tan, Yong Kiam; Heule, Marijn J. H.; Myreen, Magnus O.: \textttcake_lpr: verified propagation redundancy checking in CakeML (2021)
  20. Tan, Yong Kiam; Platzer, André: Deductive stability proofs for ordinary differential equations (2021)

previous 1 2 3 4 ... 49 50 51 next