- HOL

Classical Higher-order Logic.

- HOL-Algebra

Author: Clemens Ballarin, started 24 September 1999, and many others The Isabelle Algebraic Library.

- HOL-Analysis
- HOL-Analysis-ex
- HOL-Auth

A new approach to verifying authentication protocols.

- HOL-Bali
- HOL-Cardinals

Ordinals and Cardinals, Full Theories.

- HOL-Codegenerator_Test
- HOL-Complex_Analysis
- HOL-Computational_Algebra
- HOL-Corec_Examples

Corecursion Examples.

- HOL-Data_Structures
- HOL-Datatype_Benchmark

Big (co)datatypes.

- HOL-Datatype_Examples

(Co)datatype Examples.

- HOL-Decision_Procs

Various decision procedures, typically involving reflection.

- HOL-Eisbach

The Eisbach proof method language and "match" method.

- HOL-Examples

Notable Examples in Isabelle/HOL.

- HOL-Hahn_Banach

Author: Gertrud Bauer, TU Munich The Hahn-Banach theorem for real vector spaces. This is the proof of the Hahn-Banach theorem for real vectorspaces, following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach theorem is one of the fundamental theorems of functional analysis. It is a conclusion of Zorn's lemma. Two different formaulations of the theorem are presented, one for general real vectorspaces and its application to normed vectorspaces. The theorem says, that every continous linearform, defined on arbitrary subspaces (not only one-dimensional subspaces), can be extended to a continous linearform on the whole vectorspace.

- HOL-Hoare

Verification of imperative programs (verification conditions are generated automatically from pre/post conditions and loop invariants).

- HOL-Hoare_Parallel

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

- HOL-Homology
- HOL-IMP
- HOL-IMPP

Author: David von Oheimb Copyright 1999 TUM IMPP -- An imperative language with procedures. This is an extension of IMP with local variables and mutually recursive procedures. For documentation see "Hoare Logic for Mutual Recursion and Local Variables" (https://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).

- HOL-IOA

Author: Tobias Nipkow and Konrad Slind and Olaf Müller Copyright 1994--1996 TU Muenchen The meta-theory of I/O-Automata in HOL. This formalization has been significantly changed and extended, see HOLCF/IOA. There are also the proofs of two communication protocols which formerly have been here. @inproceedings{Nipkow-Slind-IOA, author={Tobias Nipkow and Konrad Slind}, title={{I/O} Automata in {Isabelle/HOL}}, booktitle={Proc.\ TYPES Workshop 1994}, publisher=Springer, series=LNCS, note={To appear}} ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz and @inproceedings{Mueller-Nipkow, author={Olaf M\"uller and Tobias Nipkow}, title={Combining Model Checking and Deduction for {I/O}-Automata}, booktitle={Proc.\ TACAS Workshop}, organization={Aarhus University, BRICS report}, year=1995} ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz

- HOL-Imperative_HOL
- HOL-Import
- HOL-Induct

Examples of (Co)Inductive Definitions. Comb proves the Church-Rosser theorem for combinators (see http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz). Mutil is the famous Mutilated Chess Board problem (see http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz). PropLog proves the completeness of a formalization of propositional logic (see http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz). Exp demonstrates the use of iterated inductive definitions to reason about mutually recursive relations.

- HOL-Isar_Examples

Miscellaneous Isabelle/Isar examples.

- HOL-Lattice

Author: Markus Wenzel, TU Muenchen Basic theory of lattices and orders.

- HOL-Library

Classical Higher-order Logic -- batteries included.

- HOL-Matrix_LP

Two-dimensional matrices and linear programming.

- HOL-Metis_Examples

Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen Testing Metis and Sledgehammer.

- HOL-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.

- HOL-Mirabelle
- HOL-Mirabelle-ex
- HOL-Mutabelle
- HOL-NanoJava

Hoare Logic for a tiny fragment of Java.

- HOL-Nitpick_Examples

Author: Jasmin Blanchette, TU Muenchen Copyright 2009

- HOL-Nominal
- HOL-Nominal-Examples
- HOL-Nonstandard_Analysis

Nonstandard analysis.

- HOL-Nonstandard_Analysis-Examples
- HOL-Number_Theory

Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.

- HOL-Predicate_Compile_Examples
- HOL-Probability
- HOL-Probability-ex
- HOL-Prolog

Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) A bare-bones implementation of Lambda-Prolog. This is a simple exploratory implementation of Lambda-Prolog in HOL, including some minimal examples (in Test.thy) and a more typical example of a little functional language and its type system.

- HOL-Proofs

HOL-Main with explicit proof terms.

- HOL-Proofs-Extraction

Examples for program extraction in Higher-Order Logic.

- HOL-Proofs-Lambda

Lambda Calculus in de Bruijn's Notation. This session defines lambda-calculus terms with de Bruijn indixes and proves confluence of beta, eta and beta+eta. The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).

- HOL-Proofs-ex
- HOL-Quickcheck_Benchmark
- HOL-Quickcheck_Examples
- HOL-Quotient_Examples

Author: Cezary Kaliszyk and Christian Urban

- HOL-Real_Asymp
- HOL-Real_Asymp-Manual
- HOL-Record_Benchmark

Big records.

- HOL-SET_Protocol

Verification of the SET Protocol.

- HOL-SMT_Examples
- HOL-SPARK
- HOL-SPARK-Examples
- HOL-SPARK-Manual
- HOL-Statespace
- HOL-TLA

Lamport's Temporal Logic of Actions.

- HOL-TLA-Buffer
- HOL-TLA-Inc
- HOL-TLA-Memory
- HOL-TPTP

Author: Jasmin Blanchette, TU Muenchen Author: Nik Sultana, University of Cambridge Copyright 2011 TPTP-related extensions.

- HOL-Types_To_Sets

Experimental extension of Higher-Order Logic to allow translation of types to sets.

- HOL-UNITY

Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge Verifying security protocols using Chandy and Misra's UNITY formalism.

- HOL-Unix
- HOL-ZF
- HOL-ex

Miscellaneous examples for Higher-Order Logic.

- HOLCF

Author: Franz Regensburger Author: Brian Huffman HOLCF -- a semantic extension of HOL by the LCF logic.

- HOLCF-FOCUS

FOCUS: a theory of stream-processing functions Isabelle/HOLCF. For introductions to FOCUS, see "The Design of Distributed Systems - An Introduction to FOCUS" http://www4.in.tum.de/publ/html.php?e=2 "Specification and Refinement of a Buffer of Length One" http://www4.in.tum.de/publ/html.php?e=15 "Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321

- HOLCF-IMP

IMP -- A WHILE-language and its Semantics. This is the HOLCF-based denotational semantics of a simple WHILE-language.

- HOLCF-Library
- HOLCF-Tutorial
- HOLCF-ex

Miscellaneous examples for HOLCF.

- IOA

Author: Olaf Müller Copyright 1997 TU München A formalization of I/O automata in HOLCF. The distribution contains simulation relations, temporal logic, and an abstraction theory. Everything is based upon a domain-theoretic model of finite and infinite sequences.

- IOA-ABP

Author: Olaf Müller The Alternating Bit Protocol performed in I/O-Automata: combining IOA with Model Checking. Theory Correctness contains the proof of the abstraction from unbounded channels to finite ones. File Check.ML contains a simple ModelChecker prototype checking Spec against the finite version of the ABP-protocol.

- IOA-NTP

Author: Tobias Nipkow & Konrad Slind A network transmission protocol, performed in the I/O automata formalization by Olaf Müller.

- IOA-Storage

Author: Olaf Müller Memory storage case study.

- IOA-ex

Author: Olaf Müller