wenzelm@10163: wenzelm@10163: paulson@2080: clasohm@1339: wenzelm@10163: HOL/README 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: wenzelm@10163:
BCV wenzelm@10163:
generic model of bytecode verification, i.e. data-flow analysis wenzelm@10163: for assembly languages with subtypes wenzelm@7303: wenzelm@10163:
HOL-Real wenzelm@10163:
a development of the reals and hyper-reals, which are used in wenzelm@10163: non-standard analysis (builds the image HOL-Real) wenzelm@7303: wenzelm@10163:
HOL-Real-HahnBanach wenzelm@10163:
the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar) wenzelm@7303: wenzelm@10163:
HOL-Real-ex wenzelm@10163:
miscellaneous real number examples wenzelm@10163: 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: 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: wenzelm@10163:
IOA wenzelm@10163:
a simple theory of Input/Output Automata wenzelm@10163: wenzelm@10163:
Induct wenzelm@10163:
examples of (co)inductive definitions paulson@3125: 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: wenzelm@10163:
Lex paulson@13852:
verification of a simple lexical analyser generator clasohm@1339: 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 wenzelm@10163: lightweight bytecode verifier, including proofs of type-safety. nipkow@7291: wenzelm@10163:
MiniML wenzelm@10163:
formalization of type inference for the language Mini-ML nipkow@7291: wenzelm@10163:
Modelcheck wenzelm@10163:
basic setup for integration of some model checkers in Isabelle/HOL paulson@7290: wenzelm@10163:
NumberTheory wenzelm@10163:
fundamental Theorem of Arithmetic, Chinese Remainder Theorem, wenzelm@10163: Fermat/Euler Theorem, Wilson's Theorem wenzelm@7662: wenzelm@10163:
Prolog wenzelm@10163:
a (bare-bones) implementation of Lambda-Prolog wenzelm@10163: wenzelm@10163:
Subst wenzelm@10163:
defines 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: wenzelm@10163: