Isabelle/HOL sessions

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-Combinatorics
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 for 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-ex

Some arbitrary small test case for Mirabelle.
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 and experiments for Isabelle/HOL.
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