HOL: Higher-Order Logic
These are the main sources of the Isabelle system for Higher-Order Logic.
There are also several example sessions:
- Algebra
- rings and univariate polynomials
- Auth
- a new approach to verifying authentication protocols
- AxClasses
- a few basic examples of using axiomatic type classes
- Complex
- a development of the complex numbers, the reals, and the hyper-reals,
which are used in non-standard analysis (builds the image HOL-Complex)
- Hoare
- verification of imperative programs (verification conditions are
generated automatically from pre/post conditions and loop invariants)
- HoareParallel
- verification of shared-variable imperative programs a la Owicki-Gries.
(verification conditions are generated automatically)
- Hyperreal
- Nonstandard analysis. Builds on Real and is part of Complex.
- IMP
- mechanization of a large part of a semantics text by Glynn Winskel
- IMPP
- extension of IMP with local variables and mutually recursive
procedures
- Import
- theories imported from other (HOL) theorem provers.
- Induct
- examples of (co)inductive definitions
- IOA
- a simple theory of Input/Output Automata
- Isar_Examples
- several introductory examples using Isabelle/Isar
- Lambda
- fundamental properties of lambda-calculus (Church-Rosser and termination)
- Lattice
- lattices and order structures (in Isabelle/Isar)
- Library
- A collection of generic theories
- Matrix
- two-dimensional matrices
- MicroJava
- formalization of a fragment of Java, together with a corresponding
virtual machine and a specification of its bytecode verifier and a
lightweight bytecode verifier, including proofs of type-safety
- Modelcheck
- basic setup for integration of some model checkers in Isabelle/HOL
- NanoJava
- Haore Logic for a tiny fragment of Java
- NumberTheory
- fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
Fermat/Euler Theorem, Wilson's Theorem, Quadratic Reciprocity
- Prolog
- a (bare-bones) implementation of Lambda-Prolog
- Real
- the real numbers, part of Complex
- Hahn_Banach
- the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
- SET_Protocol
- verification of the SET Protocol
- Subst
- a theory of substitution and unification.
- TLA
- Lamport's Temporal Logic of Actions (with separate example sessions)
- UNITY
- Chandy and Misra's UNITY formalism
- W0
- a precursor of MiniML, without let-expressions
- ex
- miscellaneous examples