# 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-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-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-IMP
HOL-IMPP

```    Author:     David von Oheimb

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

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,
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
```
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.

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

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

Verifying security protocols using Chandy and Misra's UNITY formalism.
```
HOL-Unix
HOL-Word
HOL-Word-SMT_Examples
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 Mueller

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 Mueller

The Alternating Bit Protocol performed in I/O-Automata.
```
IOA-NTP

```    Author:     Tobias Nipkow & Konrad Slind

A network transmission protocol, performed in the
I/O automata formalization by Olaf Mueller.
```
IOA-Storage

```    Author:     Olaf Mueller

Memory storage case study.
```
IOA-ex

```    Author:     Olaf Mueller
```