webertj@15283:
webertj@15283:
webertj@15582:
webertj@15582:
wenzelm@10163:
wenzelm@10163:
webertj@15582:
webertj@15582:
webertj@15582: HOL/README
webertj@15582:
clasohm@1339:
wenzelm@10163:
wenzelm@10163:
wenzelm@10163: HOL: Higher-Order Logic
clasohm@1339:
wenzelm@10262: These are the main sources of the Isabelle system for Higher-Order Logic.
wenzelm@10163:
wenzelm@10163:
paulson@2080:
wenzelm@10163: There are also several example sessions:
wenzelm@10163:
paulson@2080:
wenzelm@10163: - Algebra
wenzelm@10163:
- rings and univariate polynomials
wenzelm@10163:
wenzelm@10163:
- Auth
wenzelm@10163:
- a new approach to verifying authentication protocols
wenzelm@7303:
wenzelm@10163:
- AxClasses
wenzelm@10163:
- a few basic examples of using axiomatic type classes
wenzelm@10163:
nipkow@15910:
- Complex
kleing@14024:
- a development of the complex numbers, the reals, and the hyper-reals,
kleing@14024: which are used in non-standard analysis (builds the image HOL-Complex)
wenzelm@7303:
wenzelm@10163:
- Hoare
wenzelm@10163:
- verification of imperative programs (verification conditions are
wenzelm@10163: generated automatically from pre/post conditions and loop invariants)
wenzelm@7691:
nipkow@15910:
- HoareParallel
nipkow@15910:
- verification of shared-variable imperative programs a la Owicki-Gries.
nipkow@15910: (verification conditions are generated automatically)
nipkow@15910:
nipkow@15910:
- Hyperreal
nipkow@15910:
- Nonstandard analysis. Builds on Real and is part of Complex.
nipkow@15910:
wenzelm@10163:
- IMP
wenzelm@10163:
- mechanization of a large part of a semantics text by Glynn Winskel
nipkow@7291:
wenzelm@10163:
- IMPP
wenzelm@10163:
- extension of IMP with local variables and mutually recursive
wenzelm@10163: procedures
paulson@2080:
nipkow@15910:
- Import
nipkow@15910:
- theories imported from other (HOL) theorem provers.
wenzelm@10163:
wenzelm@10163:
- Induct
wenzelm@10163:
- examples of (co)inductive definitions
paulson@3125:
nipkow@15910:
- IOA
nipkow@15910:
- a simple theory of Input/Output Automata
nipkow@15910:
wenzelm@10163:
- Isar_examples
wenzelm@10163:
- several introductory examples using Isabelle/Isar
paulson@2080:
wenzelm@10163:
- Lambda
wenzelm@10163:
- fundamental properties of lambda-calculus (Church-Rosser and termination)
paulson@2080:
wenzelm@10163:
- Lattice
wenzelm@10163:
- lattices and order structures (in Isabelle/Isar)
wenzelm@7303:
nipkow@15910:
- Library
nipkow@15910:
- A collection of generic theories
nipkow@15910:
nipkow@15910:
- Matrix
nipkow@15910:
- two-dimensional matrices
nipkow@15910:
wenzelm@10163:
- MicroJava
wenzelm@10163:
- formalization of a fragment of Java, together with a corresponding
wenzelm@10163: virtual machine and a specification of its bytecode verifier and a
nipkow@15910: lightweight bytecode verifier, including proofs of type-safety
nipkow@7291:
wenzelm@10163:
- Modelcheck
wenzelm@10163:
- basic setup for integration of some model checkers in Isabelle/HOL
paulson@7290:
nipkow@15910:
- NanoJava
nipkow@15910:
- Haore Logic for a tiny fragment of Java
nipkow@15910:
wenzelm@10163:
- NumberTheory
wenzelm@10163:
- fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
nipkow@15910: Fermat/Euler Theorem, Wilson's Theorem, Quadratic Reciprocity
wenzelm@7662:
wenzelm@10163:
- Prolog
wenzelm@10163:
- a (bare-bones) implementation of Lambda-Prolog
wenzelm@10163:
nipkow@15910:
- Real
nipkow@15910:
- the real numbers, part of Complex
nipkow@15910:
nipkow@15910:
- Real/HahnBanach
nipkow@15910:
- the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
nipkow@15910:
nipkow@15910:
- SET-Protocol
nipkow@15910:
- verification of the SET Protocol
nipkow@15910:
wenzelm@10163:
- Subst
nipkow@15910:
- a theory of substitution and unification.
paulson@7290:
wenzelm@10163:
- TLA
wenzelm@10163:
- Lamport's Temporal Logic of Actions (with separate example sessions)
nipkow@7291:
wenzelm@10163:
- UNITY
wenzelm@10163:
- Chandy and Misra's UNITY formalism
paulson@7290:
wenzelm@10163:
- W0
wenzelm@10163:
- a precursor of MiniML, without let-expressions
nipkow@7291:
wenzelm@10163:
- ex
wenzelm@10163:
- miscellaneous examples
wenzelm@10163:
wenzelm@10163:
clasohm@1339:
clasohm@1339: Useful references on Higher-Order Logic:
clasohm@1339:
wenzelm@10163:
clasohm@1339:
wenzelm@10163: - P. B. Andrews,
wenzelm@10163: An Introduction to Mathematical Logic and Type Theory
wenzelm@10163: (Academic Press, 1986).
wenzelm@4622:
wenzelm@10163: - A. Church,
wenzelm@10163: A Formulation of the Simple Theory of Types
wenzelm@10163: (Journal of Symbolic Logic, 1940).
wenzelm@4622:
wenzelm@10163: - M. J. C. Gordon and T. F. Melham (editors),
wenzelm@10163: Introduction to HOL: A theorem proving environment for higher order logic
wenzelm@10163: (Cambridge University Press, 1993).
wenzelm@4622:
wenzelm@10163: - J. Lambek and P. J. Scott,
wenzelm@10163: Introduction to Higher Order Categorical Logic
wenzelm@10163: (Cambridge University Press, 1986).
wenzelm@4622:
wenzelm@10163:
clasohm@1339:
wenzelm@10163:
wenzelm@10163: