Tool support for logics of programs
Basic concepts of the generic theorem prover Isabelle are presented. Main features of the prover are the following. A higher-order syntax supports variable binding (it uses typed \(\lambda\)-calculus to represent syntax of terms, formulas and rules). Unknowns in goals allow refinement and automatic proof search. A generic framework supports a wide range of notations and methods. The classical reasoner and simplifier let us construct proofs of realistic size. Isabelle implements two set theories. Isabelle/ZF is built upon first-order logic using the standard Zermelo-Fraenkel axioms. Isabelle/HOL (high-order logic) includes a polymorphically typed set theory, with sets represented by predicates. The prover supports inductive and co-inductive relations. Also an application of Isabelle to proofs about cryptographic protocols is presented. For the entire collection see [Zbl 0874.00040].
- Set theory for verification. I: From foundations to functions
- The foundation of a generic theorem prover
- Equational reasoning in Isabelle
- Isabelle's metalogic: formalization and proof checker
- A formalization and proof checker for Isabelle's metalogic
- Structured formal development in Isabelle
- Building Formal Method Tools in the Isabelle/Isar Framework
- Support logic programming
- scientific article; zbMATH DE number 65526 (Why is no real title available?)
- scientific article; zbMATH DE number 1543300 (Why is no real title available?)
- Isabelle/HOL/GST: a formal proof environment for generalized set theories
This page was built for publication: Tool support for logics of programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4364537)
