webertj@15283: webertj@15283: 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@33026:
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: wenzelm@31795:
Hahn_Banach nipkow@15910:
the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar) nipkow@15910: wenzelm@33028:
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: wenzelm@10163: wenzelm@10163: