author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 36862 952b2b102a0a
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "">


  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">


<h2>HOL: Higher-Order Logic</h2>

These are the main sources of the Isabelle system for Higher-Order Logic.


There are also several example sessions:

<dd>rings and univariate polynomials

<dd>a new approach to verifying authentication protocols

<dd>a few basic examples of using axiomatic type classes

<dd>a development of the complex numbers, the reals, and the hyper-reals,
which are used in non-standard analysis (builds the image HOL-Complex)

<dd>verification of imperative programs (verification conditions are
generated automatically from pre/post conditions and loop invariants)

<dd>verification of shared-variable imperative programs a la Owicki-Gries.
(verification conditions are generated automatically)

<dd>Nonstandard analysis. Builds on Real and is part of Complex.

<dd>mechanization of a large part of a semantics text by Glynn Winskel

<dd>extension of IMP with local variables and mutually recursive

<dd>theories imported from other (HOL) theorem provers.

<dd>examples of (co)inductive definitions

<dd>a simple theory of Input/Output Automata

<dd>several introductory examples using Isabelle/Isar

<dd>fundamental properties of lambda-calculus (Church-Rosser and termination)

<dd>lattices and order structures (in Isabelle/Isar)

<dd>A collection of generic theories

<dd>two-dimensional matrices

<dd>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

<dd>basic setup for integration of some model checkers in Isabelle/HOL

<dd>Haore Logic for a tiny fragment of Java

<dd>fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
Fermat/Euler Theorem, Wilson's Theorem, Quadratic Reciprocity

<dd>a (bare-bones) implementation of Lambda-Prolog

<dd>the real numbers, part of Complex

<dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)

<dd>verification of the SET Protocol

<dd>a theory of substitution and unification.

<dd>Lamport's Temporal Logic of Actions (with separate example sessions)

<dd>Chandy and Misra's UNITY formalism

<dd>a precursor of MiniML, without let-expressions

<dd>miscellaneous examples