topic = Computer science/Functional programming
date = 20141013
license = LGPL
abstract =
We implemented a command that can be used to easily generate
elements of a restricted type {x :: 'a. P x},
provided the definition is of the form
f ys = (if check ys then Some(generate ys :: 'a) else None) where
ys is a list of variables y1 ... yn and
check ys ==> P(generate ys) can be proved.
In principle, such a definition is also directly possible using the
lift_definition command. However, then this definition will not be
suitable for codegeneration. To this end, we automated a more complex
construction of Joachim Breitner which is amenable for codegeneration, and
where the test check ys will only be performed once. In the
automation, one auxiliary type is created, and Isabelle's lifting and
transferpackage is invoked several times.
notify = rene.thiemann@uibk.ac.at
[Coinductive]
title = Coinductive
topic = Computer science/Functional programming
author = Andreas Lochbihler
contributors = Johannes Hölzl
date = 20100212
abstract = This article collects formalisations of generalpurpose coinductive data types and sets. Currently, it contains coinductive natural numbers, coinductive lists, i.e. lazy lists or streams, infinite streams, coinductive terminated lists, coinductive resumptions, a library of operations on coinductive lists, and a version of König's lemma as an application for coinductive lists.
The initial theory was contributed by Paulson and Wenzel. Extensions and other coinductive formalisations of general interest are welcome.
extrahistory =
Change history:
[20100610]:
coinductive lists: setup for quotient package
(revision 015574f3bf3c)
[20100628]:
new codatatype terminated lazy lists
(revision e12de475c558)
[20100804]:
terminated lazy lists: setup for quotient package;
more lemmas
(revision 6ead626f1d01)
[20100817]:
Koenig's lemma as an example application for coinductive lists
(revision f81ce373fa96)
[20110201]:
lazy implementation of coinductive (terminated) lists for the code generator
(revision 6034973dce83)
[20110720]:
new codatatype resumption
(revision 811364c776c7)
[20120627]:
new codatatype stream with operations (with contributions by Peter Gammie)
(revision dd789a56473c)
[20130313]:
construct codatatypes with the BNF package and adjust the definitions and proofs,
setup for lifting and transfer packages
(revision f593eda5b2c0)
[20130920]:
stream theory uses type and operations from HOL/BNF/Examples/Stream
(revision 692809b2b262)
[20140403]:
ccpo structure on codatatypes used to define ldrop, ldropWhile, lfilter, lconcat as least fixpoint;
ccpo topology on coinductive lists contributed by Johannes Hölzl;
added examples
(revision 23cd8156bd42)
notify = mail@andreaslochbihler.de
[StreamFusion]
title = Stream Fusion
author = Brian Huffman
topic = Computer science/Functional programming
date = 20090429
abstract = Stream Fusion is a system for removing intermediate list structures from Haskell programs; it consists of a Haskell library along with several compiler rewrite rules. (The library is available online.)
These theories contain a formalization of much of the Stream Fusion library in HOLCF. Lazy list and stream types are defined, along with coercions between the two types, as well as an equivalence relation for streams that generate the same list. List and stream versions of map, filter, foldr, enumFromTo, append, zipWith, and concatMap are defined, and the stream versions are shown to respect stream equivalence.
notify = brianh@cs.pdx.edu
[Tycon]
title = Type Constructor Classes and Monad Transformers
author = Brian Huffman
date = 20120626
topic = Computer science/Functional programming
abstract =
These theories contain a formalization of first class type constructors
and axiomatic constructor classes for HOLCF. This work is described
in detail in the ICFP 2012 paper Formal Verification of Monad
Transformers by the author. The formalization is a revised and
updated version of earlier joint work with Matthews and White.
Based on the hierarchy of type classes in Haskell, we define classes
for functors, monads, monadplus, etc. Each one includes all the
standard laws as axioms. We also provide a new user command,
tycondef, for defining new type constructors in HOLCF. Using tycondef,
we instantiate the type class hierarchy with various monads and monad
transformers.
notify = huffman@in.tum.de
[CoreC++]
title = CoreC++
author = Daniel Wasserrab
date = 20060515
topic = Computer science/Programming languages/Language definitions
abstract = We present an operational semantics and type safety proof for multiple inheritance in C++. The semantics models the behavior of method calls, field accesses, and two forms of casts in C++ class hierarchies. For explanations see the OOPSLA 2006 paper by Wasserrab, Nipkow, Snelting and Tip.
notify = nipkow@in.tum.de
[FeatherweightJava]
title = A Theory of Featherweight Java in Isabelle/HOL
author = J. Nathan Foster , Dimitrios Vytiniotis
date = 20060331
topic = Computer science/Programming languages/Language definitions
abstract = We formalize the type system, smallstep operational semantics, and type soundness proof for Featherweight Java, a simple object calculus, in Isabelle/HOL.
notify = kleing@cse.unsw.edu.au
[Jinja]
title = Jinja is not Java
author = Gerwin Klein , Tobias Nipkow
date = 20050601
topic = Computer science/Programming languages/Language definitions
abstract = We introduce Jinja, a Javalike programming language with a formal semantics designed to exhibit core features of the Java language architecture. Jinja is a compromise between realism of the language and tractability and clarity of the formal semantics. The following aspects are formalised: a big and a small step operational semantics for Jinja and a proof of their equivalence; a type system and a definite initialisation analysis; a type safety proof of the small step semantics; a virtual machine (JVM), its operational semantics and its type system; a type safety proof for the JVM; a bytecode verifier, i.e. data flow analyser for the JVM; a correctness proof of the bytecode verifier w.r.t. the type system; a compiler and a proof that it preserves semantics and welltypedness. The emphasis of this work is not on particular language features but on providing a unified model of the source language, the virtual machine and the compiler. The whole development has been carried out in the theorem prover Isabelle/HOL.
notify = kleing@cse.unsw.edu.au, nipkow@in.tum.de
[JinjaThreads]
title = Jinja with Threads
author = Andreas Lochbihler
date = 20071203
topic = Computer science/Programming languages/Language definitions
abstract = We extend the Jinja source code semantics by Klein and Nipkow with Javastyle arrays and threads. Concurrency is captured in a generic framework semantics for adding concurrency through interleaving to a sequential semantics, which features dynamic thread creation, interthread communication via shared memory, lock synchronisation and joins. Also, threads can suspend themselves and be notified by others. We instantiate the framework with the adapted versions of both Jinja source and byte code and show type safety for the multithreaded case. Equally, the compiler from source to byte code is extended, for which we prove weak bisimilarity between the source code small step semantics and the defensive Jinja virtual machine. On top of this, we formalise the JMM and show the DRF guarantee and consistency. For description of the different parts, see Lochbihler's papers at FOOL 2008, ESOP 2010, ITP 2011, and ESOP 2012.
extrahistory =
Change history:
[20080423]:
added bytecode formalisation with arrays and threads, added thread joins
(revision f74a8be156a7)
[20090427]:
added verified compiler from source code to bytecode;
encapsulate native methods in separate semantics
(revision e4f26541e58a)
[20091130]:
extended compiler correctness proof to infinite and deadlocking computations
(revision e50282397435)
[20100608]:
added thread interruption;
new abstract memory model with sequential consistency as implementation
(revision 0cb9e8dbd78d)
[20100628]:
new thread interruption model
(revision c0440d0a1177)
[20101015]:
preliminary version of the Java memory model for source code
(revision 02fee0ef3ca2)
[20101216]:
improved version of the Java memory model, also for bytecode
executable scheduler for source code semantics
(revision 1f41c1842f5a)
[20110202]:
simplified code generator setup
new random scheduler
(revision 3059dafd013f)
[20110721]:
new interruption model,
generalized JMM proof of DRF guarantee,
allow class Object to declare methods and fields,
simplified subtyping relation,
corrected division and modulo implementation
(revision 46e4181ed142)
[20120216]:
added example programs
(revision bf0b06c8913d)
[20121121]:
type safety proof for the Java memory model,
allow spurious wakeups
(revision 76063d860ae0)
[20130516]:
support for nondeterministic memory allocators
(revision cc3344a49ced)
[20171020]:
add an atomic compareandswap operation for volatile fields
(revision a6189b1d6b30)
notify = mail@andreaslochbihler.de
[LocallyNamelessSigma]
title = Locally Nameless Sigma Calculus
author = Ludovic Henrio , Florian Kammüller , Bianca Lutz , Henry Sudhof
date = 20100430
topic = Computer science/Programming languages/Language definitions
abstract = We present a Theory of Objects based on the original functional sigmacalculus by Abadi and Cardelli but with an additional parameter to methods. We prove confluence of the operational semantics following the outline of Nipkow's proof of confluence for the lambdacalculus reusing his theory Commutation, a generic diamond lemma reduction. We furthermore formalize a simple type system for our sigmacalculus including a proof of type safety. The entire development uses the concept of Locally Nameless representation for binders. We reuse an earlier proof of confluence for a simpler sigmacalculus based on de Bruijn indices and lists to represent objects.
notify = nipkow@in.tum.de
[Attack_Trees]
title = Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems
author = Florian Kammueller
topic = Computer science/Security
date = 20200427
notify = florian.kammuller@gmail.com
abstract =
In this article, we present a proof theory for Attack Trees. Attack
Trees are a well established and useful model for the construction of
attacks on systems since they allow a stepwise exploration of high
level attacks in application scenarios. Using the expressiveness of
Higher Order Logic in Isabelle, we develop a generic
theory of Attack Trees with a statebased semantics based on Kripke
structures and CTL. The resulting framework
allows mechanically supported logic analysis of the metatheory of the
proof calculus of Attack Trees and at the same time the developed
proof theory enables application to case studies. A central
correctness and completeness result proved in Isabelle establishes a
connection between the notion of Attack Tree validity and CTL. The
application is illustrated on the example of a healthcare IoT system
and GDPR compliance verification.
[AutoFocusStream]
title = AutoFocus Stream Processing for SingleClocking and MultiClocking Semantics
author = David Trachtenherz <>
date = 20110223
topic = Computer science/Programming languages/Language definitions
abstract = We formalize the AutoFocus Semantics (a timesynchronous subset of the Focus formalism) as stream processing functions on finite and infinite message streams represented as finite/infinite lists. The formalization comprises both the conventional singleclocking semantics (uniform global clock for all components and communications channels) and its extension to multiclocking semantics (internal execution clocking of a component may be a multiple of the external communication clocking). The semantics is defined by generic stream processing functions making it suitable for simulation/code generation in Isabelle/HOL. Furthermore, a number of AutoFocus semantics properties are formalized using definitions from the IntervalLogic theories.
notify = nipkow@in.tum.de
[FocusStreamsCaseStudies]
title = Stream Processing Components: Isabelle/HOL Formalisation and Case Studies
author = Maria Spichkova
date = 20131114
topic = Computer science/Programming languages/Language definitions
abstract = This set of theories presents an Isabelle/HOL formalisation of stream processing components introduced
in Focus,
a framework for formal specification and development of interactive systems.
This is an extended and updated version of the formalisation, which was
elaborated within the methodology "Focus on Isabelle".
In addition, we also applied the formalisation on three case studies
that cover different application areas: process control (Steam Boiler System),
data transmission (FlexRay communication protocol),
memory and processing components (AutomotiveGateway System).
notify = lp15@cam.ac.uk, maria.spichkova@rmit.edu.au
[Isabelle_Meta_Model]
title = A MetaModel for the Isabelle API
author = Frédéric Tuong , Burkhart Wolff
date = 20150916
topic = Computer science/Programming languages/Language definitions
abstract =
We represent a theory of (a fragment of) Isabelle/HOL in
Isabelle/HOL. The purpose of this exercise is to write packages for
domainspecific specifications such as class models, Bmachines, ...,
and generally speaking, any domainspecific languages whose
abstract syntax can be defined by a HOL "datatype". On this basis, the
Isabelle codegenerator can then be used to generate code for global
context transformations as well as tactic code.
Consequently the package is geared towards
parsing, printing and codegeneration to the Isabelle API.
It is at the moment not sufficiently rich for doing meta theory on
Isabelle itself. Extensions in this direction are possible though.
Moreover, the chosen fragment is fairly rudimentary. However it should be
easily adapted to one's needs if a package is written on top of it.
The supported API contains types, terms, transformation of
global context like definitions and datatype declarations as well
as infrastructure for Isarsetups.
This theory is drawn from the
Featherweight OCL
project where
it is used to construct a package for objectoriented datatype theories
generated from UML class diagrams. The Featherweight OCL, for example, allows for
both the direct execution of compiled tactic code by the Isabelle API
as well as the generation of ".thy"files for debugging purposes.
Gained experience from this project shows that the compiled code is sufficiently
efficient for practical purposes while being based on a formal model
on which properties of the package can be proven such as termination of certain
transformations, correctness, etc.
notify = tuong@users.gforge.inria.fr, wolff@lri.fr
[Clean]
title = Clean  An Abstract Imperative Programming Language and its Theory
author = Frédéric Tuong , Burkhart Wolff
topic = Computer science/Programming languages, Computer science/Semantics
date = 20191004
notify = wolff@lri.fr, ftuong@lri.fr
abstract =
Clean is based on a simple, abstract execution model for an imperative
target language. “Abstract” is understood in contrast to “Concrete
Semantics”; alternatively, the term “shallowstyle embedding” could be
used. It strives for a typesafe notion of programvariables, an
incremental construction of the typed statespace, support of
incremental verification, and openworld extensibility of new type
definitions being intertwined with the program definitions. Clean is
based on a “nofrills” stateexception monad with the usual
definitions of bind and unit for the compositional glue of statebased
computations. Clean offers conditionals and loops supporting Clike
controlflow operators such as break and return. The statespace
construction is based on the extensible record package. Direct
recursion of procedures is supported. Clean’s design strives for
extreme simplicity. It is geared towards symbolic execution and proven
correct verification tools. The underlying libraries of this package,
however, deliberately restrict themselves to the most elementary
infrastructure for these tasks. The package is intended to serve as
demonstrator semantic backend for Isabelle/C, or for the
testgeneration techniques.
[PCF]
title = Logical Relations for PCF
author = Peter Gammie
date = 20120701
topic = Computer science/Programming languages/Lambda calculi
abstract = We apply Andy Pitts's methods of defining relations over domains to
several classical results in the literature. We show that the Y
combinator coincides with the domaintheoretic fixpoint operator,
that parallelor and the Plotkin existential are not definable in
PCF, that the continuation semantics for PCF coincides with the
direct semantics, and that our domaintheoretic semantics for PCF is
adequate for reasoning about contextual equivalence in an
operational semantics. Our version of PCF is untyped and has both
strict and nonstrict function abstractions. The development is
carried out in HOLCF.
notify = peteg42@gmail.com
[POPLmarkdeBruijn]
title = POPLmark Challenge Via de Bruijn Indices
author = Stefan Berghofer
date = 20070802
topic = Computer science/Programming languages/Lambda calculi
abstract = We present a solution to the POPLmark challenge designed by Aydemir et al., which has as a goal the formalization of the metatheory of System F_{<:}. The formalization is carried out in the theorem prover Isabelle/HOL using an encoding based on de Bruijn indices. We start with a relatively simple formalization covering only the basic features of System F_{<:}, and explain how it can be extended to also cover records and more advanced binding constructs.
notify = berghofe@in.tum.de
[LammlNormalization]
title = Strong Normalization of Moggis's Computational Metalanguage
author = Christian Doczkal
date = 20100829
topic = Computer science/Programming languages/Lambda calculi
abstract = Handling variable binding is one of the main difficulties in formal proofs. In this context, Moggi's computational metalanguage serves as an interesting case study. It features monadic types and a commuting conversion rule that rearranges the binding structure. Lindley and Stark have given an elegant proof of strong normalization for this calculus. The key construction in their proof is a notion of relational TTlifting, using stacks of elimination contexts to obtain a GirardTait style logical relation. I give a formalization of their proof in Isabelle/HOLNominal with a particular emphasis on the treatment of bound variables.
notify = doczkal@ps.unisaarland.de, nipkow@in.tum.de
[MiniML]
title = Mini ML
author = Wolfgang Naraschewski <>, Tobias Nipkow
date = 20040319
topic = Computer science/Programming languages/Type systems
abstract = This theory defines the type inference rules and the type inference algorithm W for MiniML (simplytyped lambda terms with let) due to Milner. It proves the soundness and completeness of W w.r.t. the rules.
notify = kleing@cse.unsw.edu.au
[Simpl]
title = A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment
author = Norbert Schirmer <>
date = 20080229
topic = Computer science/Programming languages/Language definitions, Computer science/Programming languages/Logics
license = LGPL
abstract = We present the theory of Simpl, a sequential imperative programming language. We introduce its syntax, its semantics (big and smallstep operational semantics) and Hoare logics for both partial as well as total correctness. We prove soundness and completeness of the Hoare logic. We integrate and automate the Hoare logic in Isabelle/HOL to obtain a practically usable verification environment for imperative programs. Simpl is independent of a concrete programming language but expressive enough to cover all common language features: mutually recursive procedures, abrupt termination and exceptions, runtime faults, local and global variables, pointers and heap, expressions with side effects, pointers to procedures, partial application and closures, dynamic method invocation and also unbounded nondeterminism.
notify = kleing@cse.unsw.edu.au, norbert.schirmer@web.de
[Separation_Algebra]
title = Separation Algebra
author = Gerwin Klein , Rafal Kolanski , Andrew Boyton
date = 20120511
topic = Computer science/Programming languages/Logics
license = BSD
abstract = We present a generic type class implementation of separation algebra for Isabelle/HOL as well as lemmas and generic tactics which can be used directly for any instantiation of the type class.
The ex directory contains example instantiations that include structures such as a heap or virtual memory.
The abstract separation algebra is based upon "Abstract Separation Logic" by Calcagno et al. These theories are also the basis of the ITP 2012 rough diamond "Mechanised Separation Algebra" by the authors.
The aim of this work is to support and significantly reduce the effort for future separation logic developments in Isabelle/HOL by factoring out the part of separation logic that can be treated abstractly once and for all. This includes developing typical default rule sets for reasoning as well as automated tactic support for separation logic.
notify = kleing@cse.unsw.edu.au, rafal.kolanski@nicta.com.au
[Separation_Logic_Imperative_HOL]
title = A Separation Logic Framework for Imperative HOL
author = Peter Lammich , Rene Meis
date = 20121114
topic = Computer science/Programming languages/Logics
license = BSD
abstract =
We provide a framework for separationlogic based correctness proofs of
Imperative HOL programs. Our framework comes with a set of proof methods to
automate canonical tasks such as verification condition generation and
frame inference. Moreover, we provide a set of examples that show the
applicability of our framework. The examples include algorithms on lists,
hashtables, and unionfind trees. We also provide abstract interfaces for
lists, maps, and sets, that allow to develop generic imperative algorithms
and use datarefinement techniques.
As we target Imperative HOL, our programs can be translated to
efficiently executable code in various target languages, including
ML, OCaml, Haskell, and Scala.
notify = lammich@in.tum.de
[Inductive_Confidentiality]
title = Inductive Study of Confidentiality
author = Giampaolo Bella
date = 20120502
topic = Computer science/Security
abstract = This document contains the full theory files accompanying article Inductive Study of Confidentiality  for Everyone in Formal Aspects of Computing. They aim at an illustrative and didactic presentation of the Inductive Method of protocol analysis, focusing on the treatment of one of the main goals of security protocols: confidentiality against a threat model. The treatment of confidentiality, which in fact forms a key aspect of all protocol analysis tools, has been found cryptic by many learners of the Inductive Method, hence the motivation for this work. The theory files in this document guide the reader step by step towards design and proof of significant confidentiality theorems. These are developed against two threat models, the standard DolevYao and a more audacious one, the General Attacker, which turns out to be particularly useful also for teaching purposes.
notify = giamp@dmi.unict.it
[Possibilistic_Noninterference]
title = Possibilistic Noninterference
author = Andrei Popescu , Johannes Hölzl
date = 20120910
topic = Computer science/Security, Computer science/Programming languages/Type systems
abstract = We formalize a wide variety of Volpano/Smithstyle noninterference
notions for a while language with parallel composition.
We systematize and classify these notions according to
compositionality w.r.t. the language constructs. Compositionality
yields sound syntactic criteria (a.k.a. type systems) in a uniform way.
An article
about these proofs is published in the proceedings
of the conference Certified Programs and Proofs 2012.
notify = hoelzl@in.tum.de
[SIFUM_Type_Systems]
title = A Formalization of Assumptions and Guarantees for Compositional Noninterference
author = Sylvia Grewe , Heiko Mantel , Daniel Schoepe
date = 20140423
topic = Computer science/Security, Computer science/Programming languages/Type systems
abstract = Research in informationflow security aims at developing methods to
identify undesired information leaks within programs from private
(high) sources to public (low) sinks. For a concurrent system, it is
desirable to have compositional analysis methods that allow for
analyzing each thread independently and that nevertheless guarantee
that the parallel composition of successfully analyzed threads
satisfies a global security guarantee. However, such a compositional
analysis should not be overly pessimistic about what an environment
might do with shared resources. Otherwise, the analysis will reject
many intuitively secure programs.
The paper "Assumptions and Guarantees for Compositional
Noninterference" by Mantel et. al. presents one solution for this problem:
an approach for compositionally reasoning about noninterference in
concurrent programs via relyguaranteestyle reasoning. We present an
Isabelle/HOL formalization of the concepts and proofs of this approach.
notify =
[Dependent_SIFUM_Type_Systems]
title = A Dependent Security Type System for Concurrent Imperative Programs
author = Toby Murray , Robert Sison<>, Edward Pierzchalski<>, Christine Rizkallah
notify = toby.murray@unimelb.edu.au
date = 20160625
topic = Computer science/Security, Computer science/Programming languages/Type systems
abstract =
The paper "Compositional Verification and Refinement of Concurrent
ValueDependent Noninterference" by Murray et. al. (CSF 2016) presents
a dependent security type system for compositionally verifying a
valuedependent noninterference property, defined in (Murray, PLAS
2015), for concurrent programs. This development formalises that
security definition, the type system and its soundness proof, and
demonstrates its application on some small examples. It was derived
from the SIFUM_Type_Systems AFP entry, by Sylvia Grewe, Heiko Mantel
and Daniel Schoepe, and whose structure it inherits.
extrahistory =
Change history:
[20160819]:
Removed unused "stop" parameter and "stop_no_eval" assumption from the sifum_security locale.
(revision dbc482d36372)
[20160927]:
Added security locale support for the imposition of requirements on the initial memory.
(revision cce4ceb74ddb)
[Dependent_SIFUM_Refinement]
title = Compositional SecurityPreserving Refinement for Concurrent Imperative Programs
author = Toby Murray , Robert Sison<>, Edward Pierzchalski<>, Christine Rizkallah
notify = toby.murray@unimelb.edu.au
date = 20160628
topic = Computer science/Security
abstract =
The paper "Compositional Verification and Refinement of Concurrent
ValueDependent Noninterference" by Murray et. al. (CSF 2016) presents
a compositional theory of refinement for a valuedependent
noninterference property, defined in (Murray, PLAS 2015), for
concurrent programs. This development formalises that refinement
theory, and demonstrates its application on some small examples.
extrahistory =
Change history:
[20160819]:
Removed unused "stop" parameters from the sifum_refinement locale.
(revision dbc482d36372)
[20160902]:
TobyM extended "simple" refinement theory to be usable for all bisimulations.
(revision 547f31c25f60)
[RelationalIncorrectnessLogic]
title = An UnderApproximate Relational Logic
author = Toby Murray
topic = Computer science/Programming languages/Logics, Computer science/Security
date = 20200312
notify = toby.murray@unimelb.edu.au
abstract =
Recently, authors have proposed underapproximate logics for reasoning
about programs. So far, all such logics have been confined to
reasoning about individual program behaviours. Yet there exist many
overapproximate relational logics for reasoning about pairs of
programs and relating their behaviours. We present the first
underapproximate relational logic, for the simple imperative language
IMP. We prove our logic is both sound and complete. Additionally, we
show how reasoning in this logic can be decomposed into nonrelational
reasoning in an underapproximate Hoare logic, mirroring Beringer’s
result for overapproximate relational logics. We illustrate the
application of our logic on some small examples in which we provably
demonstrate the presence of insecurity.
[Strong_Security]
title = A Formalization of Strong Security
author = Sylvia Grewe , Alexander Lux , Heiko Mantel , Jens Sauer
date = 20140423
topic = Computer science/Security, Computer science/Programming languages/Type systems
abstract = Research in informationflow security aims at developing methods to
identify undesired information leaks within programs from private
sources to public sinks. Noninterference captures this
intuition. Strong security from Sabelfeld and Sands
formalizes noninterference for concurrent systems.
We present an Isabelle/HOL formalization of strong security for
arbitrary security lattices (Sabelfeld and Sands use
a twoelement security lattice in the original publication).
The formalization includes
compositionality proofs for strong security and a soundness proof
for a security type system that checks strong security for programs
in a simple while language with dynamic thread creation.
Our formalization of the security type system is abstract in the
language for expressions and in the semantic side conditions for
expressions. It can easily be instantiated with different syntactic
approximations for these side conditions. The soundness proof of
such an instantiation boils down to showing that these syntactic
approximations imply the semantic side conditions.
notify =
[WHATandWHERE_Security]
title = A Formalization of Declassification with WHATandWHERESecurity
author = Sylvia Grewe , Alexander Lux , Heiko Mantel , Jens Sauer
date = 20140423
topic = Computer science/Security, Computer science/Programming languages/Type systems
abstract = Research in informationflow security aims at developing methods to
identify undesired information leaks within programs from private
sources to public sinks. Noninterference captures this intuition by
requiring that no information whatsoever flows from private sources
to public sinks. However, in practice this definition is often too
strict: Depending on the intuitive desired security policy, the
controlled declassification of certain private information (WHAT) at
certain points in the program (WHERE) might not result in an
undesired information leak.
We present an Isabelle/HOL formalization of such a security property
for controlled declassification, namely WHAT&WHEREsecurity from
"SchedulerIndependent Declassification" by Lux, Mantel, and Perner.
The formalization includes
compositionality proofs for and a soundness proof for a security
type system that checks for programs in a simple while language with
dynamic thread creation.
Our formalization of the security type system is abstract in the
language for expressions and in the semantic side conditions for
expressions. It can easily be instantiated with different syntactic
approximations for these side conditions. The soundness proof of
such an instantiation boils down to showing that these syntactic
approximations imply the semantic side conditions.
This Isabelle/HOL formalization uses theories from the entry
Strong Security.
notify =
[VolpanoSmith]
title = A Correctness Proof for the Volpano/Smith Security Typing System
author = Gregor Snelting , Daniel Wasserrab
date = 20080902
topic = Computer science/Programming languages/Type systems, Computer science/Security
abstract = The Volpano/Smith/Irvine security type systems requires that variables are annotated as high (secret) or low (public), and provides typing rules which guarantee that secret values cannot leak to public output ports. This property of a program is called confidentiality. For a simple whilelanguage without threads, our proof shows that typeability in the Volpano/Smith system guarantees noninterference. Noninterference means that if two initial states for program execution are lowequivalent, then the final states are lowequivalent as well. This indeed implies that secret values cannot leak to public ports. The proof defines an abstract syntax and operational semantics for programs, formalizes noninterference, and then proceeds by rule induction on the operational semantics. The mathematically most intricate part is the treatment of implicit flows. Note that the Volpano/Smith system is not flowsensitive and thus quite unprecise, resulting in false alarms. However, due to the correctness property, all potential breaks of confidentiality are discovered.
notify =
[AbstractHoareLogics]
title = Abstract Hoare Logics
author = Tobias Nipkow
date = 20060808
topic = Computer science/Programming languages/Logics
abstract = These therories describe Hoare logics for a number of imperative language constructs, from whileloops to mutually recursive procedures. Both partial and total correctness are treated. In particular a proof system for total correctness of recursive procedures in the presence of unbounded nondeterminism is presented.
notify = nipkow@in.tum.de
[Stone_Algebras]
title = Stone Algebras
author = Walter Guttmann
notify = walter.guttmann@canterbury.ac.nz
date = 20160906
topic = Mathematics/Order
abstract =
A range of algebras between lattices and Boolean algebras generalise
the notion of a complement. We develop a hierarchy of these
pseudocomplemented algebras that includes Stone algebras.
Independently of this theory we study filters based on partial orders.
Both theories are combined to prove Chen and Grätzer's construction
theorem for Stone algebras. The latter involves extensive reasoning
about algebraic structures in addition to reasoning in algebraic
structures.
[Kleene_Algebra]
title = Kleene Algebra
author = Alasdair Armstrong <>, Georg Struth , Tjark Weber
date = 20130115
topic = Computer science/Programming languages/Logics, Computer science/Automata and formal languages, Mathematics/Algebra
abstract =
These files contain a formalisation of variants of Kleene algebras and
their most important models as axiomatic type classes in Isabelle/HOL.
Kleene algebras are foundational structures in computing with
applications ranging from automata and language theory to computational
modeling, program construction and verification.
We start with formalising dioids, which are additively idempotent
semirings, and expand them by axiomatisations of the Kleene star for
finite iteration and an omega operation for infinite iteration. We
show that powersets over a given monoid, (regular) languages, sets of
paths in a graph, sets of computation traces, binary relations and
formal power series form Kleene algebras, and consider further models
based on lattices, maxplus semirings and minplus semirings. We also
demonstrate that dioids are closed under the formation of matrices
(proofs for Kleene algebras remain to be completed).
On the one hand we have aimed at a reference formalisation of variants
of Kleene algebras that covers a wide range of variants and the core
theorems in a structured and modular way and provides readable proofs
at text book level. On the other hand, we intend to use this algebraic
hierarchy and its models as a generic algebraic middlelayer from which
programming applications can quickly be explored, implemented and verified.
notify = g.struth@sheffield.ac.uk, tjark.weber@it.uu.se
[KAT_and_DRA]
title = Kleene Algebra with Tests and Demonic Refinement Algebras
author = Alasdair Armstrong <>, Victor B. F. Gomes , Georg Struth
date = 20140123
topic = Computer science/Programming languages/Logics, Computer science/Automata and formal languages, Mathematics/Algebra
abstract =
We formalise Kleene algebra with tests (KAT) and demonic refinement
algebra (DRA) in Isabelle/HOL. KAT is relevant for program verification
and correctness proofs in the partial correctness setting. While DRA
targets similar applications in the context of total correctness. Our
formalisation contains the two most important models of these algebras:
binary relations in the case of KAT and predicate transformers in the
case of DRA. In addition, we derive the inference rules for Hoare logic
in KAT and its relational model and present a simple formally verified
program verification tool prototype based on the algebraic approach.
notify = g.struth@dcs.shef.ac.uk
[KAD]
title = Kleene Algebras with Domain
author = Victor B. F. Gomes , Walter Guttmann , Peter Höfner , Georg Struth , Tjark Weber
date = 20160412
topic = Computer science/Programming languages/Logics, Computer science/Automata and formal languages, Mathematics/Algebra
abstract =
Kleene algebras with domain are Kleene algebras endowed with an
operation that maps each element of the algebra to its domain of
definition (or its complement) in abstract fashion. They form a simple
algebraic basis for Hoare logics, dynamic logics or predicate
transformer semantics. We formalise a modular hierarchy of algebras
with domain and antidomain (domain complement) operations in
Isabelle/HOL that ranges from domain and antidomain semigroups to
modal Kleene algebras and divergence Kleene algebras. We link these
algebras with models of binary relations and program traces. We
include some examples from modal logics, termination and program
analysis.
notify = walter.guttman@canterbury.ac.nz, g.struth@sheffield.ac.uk, tjark.weber@it.uu.se
[Regular_Algebras]
title = Regular Algebras
author = Simon Foster , Georg Struth
date = 20140521
topic = Computer science/Automata and formal languages, Mathematics/Algebra
abstract =
Regular algebras axiomatise the equational theory of regular expressions as induced by
regular language identity. We use Isabelle/HOL for a detailed systematic study of regular
algebras given by Boffa, Conway, Kozen and Salomaa. We investigate the relationships between
these classes, formalise a soundness proof for the smallest class (Salomaa's) and obtain
completeness of the largest one (Boffa's) relative to a deep result by Krob. In addition
we provide a large collection of regular identities in the general setting of Boffa's axiom.
Our regular algebra hierarchy is orthogonal to the Kleene algebra hierarchy in the Archive
of Formal Proofs; we have not aimed at an integration for pragmatic reasons.
notify = simon.foster@york.ac.uk, g.struth@sheffield.ac.uk
[BytecodeLogicJmlTypes]
title = A Bytecode Logic for JML and Types
author = Lennart Beringer <>, Martin Hofmann
date = 20081212
topic = Computer science/Programming languages/Logics
abstract = This document contains the Isabelle/HOL sources underlying the paper A bytecode logic for JML and types by Beringer and Hofmann, updated to Isabelle 2008. We present a program logic for a subset of sequential Java bytecode that is suitable for representing both, features found in highlevel specification language JML as well as interpretations of highlevel type systems. To this end, we introduce a finegrained collection of assertions, including strong invariants, local annotations and VDMreminiscent partialcorrectness specifications. Thanks to a goaloriented structure and interpretation of judgements, verification may proceed without recourse to an additional control flow analysis. The suitability for interpreting intensional type systems is illustrated by the proofcarryingcode style encoding of a type system for a firstorder functional language which guarantees a constant upper bound on the number of objects allocated throughout an execution, be the execution terminating or nonterminating. Like the published paper, the formal development is restricted to a comparatively small subset of the JVML, lacking (among other features) exceptions, arrays, virtual methods, and static fields. This shortcoming has been overcome meanwhile, as our paper has formed the basis of the Mobius base logic, a program logic for the full sequential fragment of the JVML. Indeed, the present formalisation formed the basis of a subsequent formalisation of the Mobius base logic in the proof assistant Coq, which includes a proof of soundness with respect to the Bicolano operational semantics by Pichardie.
notify =
[DataRefinementIBP]
title = Semantics and Data Refinement of Invariant Based Programs
author = Viorel Preoteasa , RalphJohan Back
date = 20100528
topic = Computer science/Programming languages/Logics
abstract = The invariant based programming is a technique of constructing correct programs by first identifying the basic situations (pre and postconditions and invariants) that can occur during the execution of the program, and then defining the transitions and proving that they preserve the invariants. Data refinement is a technique of building correct programs working on concrete datatypes as refinements of more abstract programs. In the theories presented here we formalize the predicate transformer semantics for invariant based programs and their data refinement.
extrahistory =
Change history:
[20120105]: Moved some general complete lattice properties to the AFP entry Lattice Properties.
Changed the definition of the data refinement relation to be more general and updated all corresponding theorems.
Added new syntax for demonic and angelic update statements.
notify = viorel.preoteasa@aalto.fi
[RefinementReactive]
title = Formalization of Refinement Calculus for Reactive Systems
author = Viorel Preoteasa
date = 20141008
topic = Computer science/Programming languages/Logics
abstract =
We present a formalization of refinement calculus for reactive systems.
Refinement calculus is based on monotonic predicate transformers
(monotonic functions from sets of poststates to sets of prestates),
and it is a powerful formalism for reasoning about imperative programs.
We model reactive systems as monotonic property transformers
that transform sets of output infinite sequences into sets of input
infinite sequences. Within this semantics we can model
refinement of reactive systems, (unbounded) angelic and
demonic nondeterminism, sequential composition, and
other semantic properties. We can model systems that may
fail for some inputs, and we can model compatibility of systems.
We can specify systems that have liveness properties using
linear temporal logic, and we can refine system specifications
into systems based on symbolic transitions systems, suitable
for implementations.
notify = viorel.preoteasa@aalto.fi
[SIFPL]
title = Secure information flow and program logics
author = Lennart Beringer <>, Martin Hofmann
date = 20081110
topic = Computer science/Programming languages/Logics, Computer science/Security
abstract = We present interpretations of type systems for secure information flow in Hoare logic, complementing previous encodings in relational program logics. We first treat the imperative language IMP, extended by a simple procedure call mechanism. For this language we consider baseline noninterference in the style of Volpano et al. and the flowsensitive type system by Hunt and Sands. In both cases, we show how typing derivations may be used to automatically generate proofs in the program logic that certify the absence of illicit flows. We then add instructions for object creation and manipulation, and derive appropriate proof rules for baseline noninterference. As a consequence of our work, standard verification technology may be used for verifying that a concrete program satisfies the noninterference property.
The present proof development represents an update of the formalisation underlying our paper [CSF 2007] and is intended to resolve any ambiguities that may be present in the paper.
notify = lennart.beringer@ifi.lmu.de
[TLA]
title = A Definitional Encoding of TLA* in Isabelle/HOL
author = Gudmund Grov , Stephan Merz
date = 20111119
topic = Computer science/Programming languages/Logics
abstract = We mechanise the logic TLA*
[Merz 1999],
an extension of Lamport's Temporal Logic of Actions (TLA)
[Lamport 1994]
for specifying and reasoning
about concurrent and reactive systems. Aiming at a framework for mechanising] the verification of TLA (or TLA*) specifications, this contribution reuses
some elements from a previous axiomatic encoding of TLA in Isabelle/HOL
by the second author [Merz 1998], which has been part of the Isabelle
distribution. In contrast to that previous work, we give here a shallow,
definitional embedding, with the following highlights:
 a theory of infinite sequences, including a formalisation of the concepts of stuttering invariance central to TLA and TLA*;
 a definition of the semantics of TLA*, which extends TLA by a mutuallyrecursive definition of formulas and preformulas, generalising TLA action formulas;
 a substantial set of derived proof rules, including the TLA* axioms and Lamport's proof rules for system verification;
 a set of examples illustrating the usage of Isabelle/TLA* for reasoning about systems.
Note that this work is unrelated to the ongoing development of a proof system
for the specification language TLA+, which includes an encoding of TLA+ as a
new Isabelle object logic [Chaudhuri et al 2010].
notify = ggrov@inf.ed.ac.uk
[CompilingExceptionsCorrectly]
title = Compiling Exceptions Correctly
author = Tobias Nipkow
date = 20040709
topic = Computer science/Programming languages/Compiling
abstract = An exception compilation scheme that dynamically creates and removes exception handler entries on the stack. A formalization of an article of the same name by Hutton and Wright.
notify = nipkow@in.tum.de
[NormByEval]
title = Normalization by Evaluation
author = Klaus Aehlig , Tobias Nipkow
date = 20080218
topic = Computer science/Programming languages/Compiling
abstract = This article formalizes normalization by evaluation as implemented in Isabelle. Lambda calculus plus term rewriting is compiled into a functional program with pattern matching. It is proved that the result of a successful evaluation is a) correct, i.e. equivalent to the input, and b) in normal form.
notify = nipkow@in.tum.de
[ProgramConflictAnalysis]
title = Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors
topic = Computer science/Programming languages/Static analysis
author = Peter Lammich , Markus MüllerOlm
date = 20071214
abstract = In this work we formally verify the soundness and precision of a static program analysis that detects conflicts (e. g. data races) in programs with procedures, thread creation and monitors with the Isabelle theorem prover. As common in static program analysis, our program model abstracts guarded branching by nondeterministic branching, but completely interprets the call/return behavior of procedures, synchronization by monitors, and thread creation. The analysis is based on the observation that all conflicts already occur in a class of particularly restricted schedules. These restricted schedules are suited to constraintsystembased program analysis. The formalization is based upon a flowgraphbased program model with an operational semantics as reference point.
notify = peter.lammich@unimuenster.de
[ShiversCFA]
title = Shivers' Control Flow Analysis
topic = Computer science/Programming languages/Static analysis
author = Joachim Breitner
date = 20101116
abstract =
In his dissertation, Olin Shivers introduces a concept of control flow graphs
for functional languages, provides an algorithm to statically derive a safe
approximation of the control flow graph and proves this algorithm correct. In
this research project, Shivers' algorithms and proofs are formalized
in the HOLCF extension of HOL.
notify = mail@joachimbreitner.de, nipkow@in.tum.de
[Slicing]
title = Towards Certified Slicing
author = Daniel Wasserrab
date = 20080916
topic = Computer science/Programming languages/Static analysis
abstract = Slicing is a widelyused technique with applications in e.g. compiler technology and software security. Thus verification of algorithms in these areas is often based on the correctness of slicing, which should ideally be proven independent of concrete programming languages and with the help of wellknown verifying techniques such as proof assistants. As a first step in this direction, this contribution presents a framework for dynamic and static intraprocedural slicing based on control flow and program dependence graphs. Abstracting from concrete syntax we base the framework on a graph representation of the program fulfilling certain structural and wellformedness properties.
The formalization consists of the basic framework (in subdirectory Basic/), the correctness proof for dynamic slicing (in subdirectory Dynamic/), the correctness proof for static intraprocedural slicing (in subdirectory StaticIntra/) and instantiations of the framework with a simple While language (in subdirectory While/) and the sophisticated objectoriented bytecode language of Jinja (in subdirectory JinjaVM/). For more information on the framework, see the TPHOLS 2008 paper by Wasserrab and Lochbihler and the PLAS 2009 paper by Wasserrab et al.
notify =
[HRBSlicing]
title = Backing up Slicing: Verifying the Interprocedural TwoPhase HorwitzRepsBinkley Slicer
author = Daniel Wasserrab
date = 20091113
topic = Computer science/Programming languages/Static analysis
abstract = After verifying dynamic and static interprocedural slicing, we present a modular framework for static interprocedural slicing. To this end, we formalized the standard twophase slicer from Horwitz, Reps and Binkley (see their TOPLAS 12(1) 1990 paper) together with summary edges as presented by Reps et al. (see FSE 1994). The framework is again modular in the programming language by using an abstract CFG, defined via structural and wellformedness properties. Using a weak simulation between the original and sliced graph, we were able to prove the correctness of static interprocedural slicing. We also instantiate our framework with a simple While language with procedures. This shows that the chosen abstractions are indeed valid.
notify = nipkow@in.tum.de
[WorkerWrapper]
title = The Worker/Wrapper Transformation
author = Peter Gammie
date = 20091030
topic = Computer science/Programming languages/Transformations
abstract = Gill and Hutton formalise the worker/wrapper transformation, building on the work of Launchbury and PeytonJones who developed it as a way of changing the type at which a recursive function operates. This development establishes the soundness of the technique and several examples of its use.
notify = peteg42@gmail.com, nipkow@in.tum.de
[JiveDataStoreModel]
title = Jive Data and Store Model
author = Nicole Rauch , Norbert Schirmer <>
date = 20050620
license = LGPL
topic = Computer science/Programming languages/Misc
abstract = This document presents the formalization of an objectoriented data and store model in Isabelle/HOL. This model is being used in the Java Interactive Verification Environment, Jive.
notify = kleing@cse.unsw.edu.au, schirmer@in.tum.de
[HotelKeyCards]
title = Hotel Key Card System
author = Tobias Nipkow
date = 20060909
topic = Computer science/Security
abstract = Two models of an electronic hotel key card system are contrasted: a state based and a trace based one. Both are defined, verified, and proved equivalent in the theorem prover Isabelle/HOL. It is shown that if a guest follows a certain safety policy regarding her key cards, she can be sure that nobody but her can enter her room.
notify = nipkow@in.tum.de
[RSAPSS]
title = SHA1, RSA, PSS and more
author = Christina Lindenberg <>, Kai Wirt <>
date = 20050502
topic = Computer science/Security/Cryptography
abstract = Formal verification is getting more and more important in computer science. However the state of the art formal verification methods in cryptography are very rudimentary. These theories are one step to provide a tool box allowing the use of formal methods in every aspect of cryptography. Moreover we present a proof of concept for the feasibility of verification techniques to a standard signature algorithm.
notify = nipkow@in.tum.de
[InformationFlowSlicing]
title = Information Flow Noninterference via Slicing
author = Daniel Wasserrab
date = 20100323
topic = Computer science/Security
abstract =
In this contribution, we show how correctness proofs for intra and interprocedural slicing can be used to prove
that slicing is able to guarantee information flow noninterference.
Moreover, we also illustrate how to lift the control flow graphs of the
respective frameworks such that they fulfil the additional assumptions
needed in the noninterference proofs. A detailed description of the
intraprocedural proof and its interplay with the slicing framework can be
found in the PLAS'09 paper by Wasserrab et al.
This entry contains the part for intraprocedural slicing. See entry
InformationFlowSlicing_Inter
for the interprocedural part.
extrahistory =
Change history:
[20160610]: The original entry InformationFlowSlicing contained both
the inter and intraprocedural case was split into
two for easier maintenance.
notify =
[InformationFlowSlicing_Inter]
title = InterProcedural Information Flow Noninterference via Slicing
author = Daniel Wasserrab
date = 20100323
topic = Computer science/Security
abstract =
In this contribution, we show how correctness proofs for intra and interprocedural slicing can be used to prove
that slicing is able to guarantee information flow noninterference.
Moreover, we also illustrate how to lift the control flow graphs of the
respective frameworks such that they fulfil the additional assumptions
needed in the noninterference proofs. A detailed description of the
intraprocedural proof and its interplay with the slicing framework can be
found in the PLAS'09 paper by Wasserrab et al.
This entry contains the part for interprocedural slicing. See entry
InformationFlowSlicing
for the intraprocedural part.
extrahistory =
Change history:
[20160610]: The original entry InformationFlowSlicing contained both
the inter and intraprocedural case was split into
two for easier maintenance.
notify =
[ComponentDependencies]
title = Formalisation and Analysis of Component Dependencies
author = Maria Spichkova
date = 20140428
topic = Computer science/System description languages
abstract = This set of theories presents a formalisation in Isabelle/HOL of data dependencies between components. The approach allows to analyse system structure oriented towards efficient checking of system: it aims at elaborating for a concrete system, which parts of the system are necessary to check a given property.
notify = maria.spichkova@rmit.edu.au
[VerifiedProver]
title = A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic
author = Tom Ridge <>
date = 20040928
topic = Logic/General logic/Mechanization of proofs
abstract = Soundness and completeness for a system of first order logic are formally proved, building on James Margetson's formalization of work by Wainer and Wallen. The completeness proofs naturally suggest an algorithm to derive proofs. This algorithm, which can be implemented tail recursively, is formalized in Isabelle/HOL. The algorithm can be executed via the rewriting tactics of Isabelle. Alternatively, the definitions can be exported to OCaml, yielding a directly executable program.
notify = lp15@cam.ac.uk
[Completeness]
title = Completeness theorem
author = James Margetson <>, Tom Ridge <>
date = 20040920
topic = Logic/Proof theory
abstract = The completeness of firstorder logic is proved, following the first five pages of Wainer and Wallen's chapter of the book Proof Theory by Aczel et al., CUP, 1992. Their presentation of formulas allows the proofs to use symmetry arguments. Margetson formalized this theorem by early 2000. The Isar conversion is thanks to Tom Ridge. A paper describing the formalization is available [pdf].
notify = lp15@cam.ac.uk
[Ordinal]
title = Countable Ordinals
author = Brian Huffman
date = 20051111
topic = Logic/Set theory
abstract = This development defines a wellordered type of countable ordinals. It includes notions of continuous and normal functions, recursively defined functions over ordinals, least fixedpoints, and derivatives. Much of ordinal arithmetic is formalized, including exponentials and logarithms. The development concludes with formalizations of Cantor Normal Form and Veblen hierarchies over normal functions.
notify = lcp@cl.cam.ac.uk
[Ordinals_and_Cardinals]
title = Ordinals and Cardinals
author = Andrei Popescu
date = 20090901
topic = Logic/Set theory
abstract = We develop a basic theory of ordinals and cardinals in Isabelle/HOL, up to the point where some cardinality facts relevant for the ``working mathematician" become available. Unlike in set theory, here we do not have at hand canonical notions of ordinal and cardinal. Therefore, here an ordinal is merely a wellorder relation and a cardinal is an ordinal minim w.r.t. order embedding on its field.
extrahistory =
Change history:
[20120925]: This entry has been discontinued because it is now part of the Isabelle distribution.
notify = uuomul@yahoo.com, nipkow@in.tum.de
[FOLFitting]
title = FirstOrder Logic According to Fitting
author = Stefan Berghofer
contributors = Asta Halkjær From
date = 20070802
topic = Logic/General logic/Classical firstorder logic
abstract = We present a formalization of parts of Melvin Fitting's book "FirstOrder Logic and Automated Theorem Proving". The formalization covers the syntax of firstorder logic, its semantics, the model existence theorem, a natural deduction proof calculus together with a proof of correctness and completeness, as well as the LöwenheimSkolem theorem.
extrahistory =
Change history:
[20180721]: Proved completeness theorem for open formulas. Proofs are now written in the declarative style. Enumeration of pairs and datatypes is automated using the Countable theory.
notify = berghofe@in.tum.de
[Epistemic_Logic]
title = Epistemic Logic
author = Asta Halkjær From
topic = Logic/General logic/Logics of knowledge and belief
date = 20181029
notify = ahfrom@dtu.dk
abstract =
This work is a formalization of epistemic logic with countably many
agents. It includes proofs of soundness and completeness for the axiom
system K. The completeness proof is based on the textbook
"Reasoning About Knowledge" by Fagin, Halpern, Moses and
Vardi (MIT Press 1995).
[SequentInvertibility]
title = Invertibility in Sequent Calculi
author = Peter Chapman <>
date = 20090828
topic = Logic/Proof theory
license = LGPL
abstract = The invertibility of the rules of a sequent calculus is important for guiding proof search and can be used in some formalised proofs of Cut admissibility. We present sufficient conditions for when a rule is invertible with respect to a calculus. We illustrate the conditions with examples. It must be noted we give purely syntactic criteria; no guarantees are given as to the suitability of the rules.
notify = pc@cs.standrews.ac.uk, nipkow@in.tum.de
[LinearQuantifierElim]
title = Quantifier Elimination for Linear Arithmetic
author = Tobias Nipkow
date = 20080111
topic = Logic/General logic/Decidability of theories
abstract = This article formalizes quantifier elimination procedures for dense linear orders, linear real arithmetic and Presburger arithmetic. In each case both a DNFbased nonelementary algorithm and one or more (doubly) exponential NNFbased algorithms are formalized, including the wellknown algorithms by Ferrante and Rackoff and by Cooper. The NNFbased algorithms for dense linear orders are new but based on Ferrante and Rackoff and on an algorithm by Loos and Weisspfenning which simulates infenitesimals. All algorithms are directly executable. In particular, they yield reflective quantifier elimination procedures for HOL itself. The formalization makes heavy use of locales and is therefore highly modular.
notify = nipkow@in.tum.de
[NatIntervalLogic]
title = Interval Temporal Logic on Natural Numbers
author = David Trachtenherz <>
date = 20110223
topic = Logic/General logic/Temporal logic
abstract = We introduce a theory of temporal logic operators using sets of natural numbers as time domain, formalized in a shallow embedding manner. The theory comprises special natural intervals (theory IL_Interval: open and closed intervals, continuous and modulo intervals, interval traversing results), operators for shifting intervals to left/right on the number axis as well as expanding/contracting intervals by constant factors (theory IL_IntervalOperators.thy), and ultimately definitions and results for unary and binary temporal operators on arbitrary natural sets (theory IL_TemporalOperators).
notify = nipkow@in.tum.de
[RecursionTheoryI]
title = Recursion Theory I
author = Michael Nedzelsky <>
date = 20080405
topic = Logic/Computability
abstract = This document presents the formalization of introductory material from recursion theory  definitions and basic properties of primitive recursive functions, Cantor pairing function and computably enumerable sets (including a proof of existence of a onecomplete computably enumerable set and a proof of the Rice's theorem).
notify = MichaelNedzelsky@yandex.ru
[FreeBooleanAlgebra]
topic = Logic/General logic/Classical propositional logic
title = Free Boolean Algebra
author = Brian Huffman
date = 20100329
abstract = This theory defines a type constructor representing the free Boolean algebra over a set of generators. Values of type (α)formula represent propositional formulas with uninterpreted variables from type α, ordered by implication. In addition to all the standard Boolean algebra operations, the library also provides a function for building homomorphisms to any other Boolean algebra type.
notify = brianh@cs.pdx.edu
[Sort_Encodings]
title = Sound and Complete Sort Encodings for FirstOrder Logic
author = Jasmin Christian Blanchette , Andrei Popescu
date = 20130627
topic = Logic/General logic/Mechanization of proofs
abstract =
This is a formalization of the soundness and completeness properties
for various efficient encodings of sorts in unsorted firstorder logic
used by Isabelle's Sledgehammer tool.
Essentially, the encodings proceed as follows:
a manysorted problem is decorated with (as few as possible) tags or
guards that make the problem monotonic; then sorts can be soundly
erased.
The development employs a formalization of manysorted firstorder logic
in clausal form (clauses, structures and the basic properties
of the satisfaction relation), which could be of interest as the starting
point for other formalizations of firstorder logic metatheory.
notify = uuomul@yahoo.com
[Lambda_Free_RPOs]
title = Formalization of Recursive Path Orders for LambdaFree HigherOrder Terms
author = Jasmin Christian Blanchette , Uwe Waldmann , Daniel Wand
date = 20160923
topic = Logic/Rewriting
abstract = This Isabelle/HOL formalization defines recursive path orders (RPOs) for higherorder terms without lambdaabstraction and proves many useful properties about them. The main order fully coincides with the standard RPO on firstorder terms also in the presence of currying, distinguishing it from previous work. An optimized variant is formalized as well. It appears promising as the basis of a higherorder superposition calculus.
notify = jasmin.blanchette@gmail.com
[Lambda_Free_KBOs]
title = Formalization of Knuth–Bendix Orders for LambdaFree HigherOrder Terms
author = Heiko Becker , Jasmin Christian Blanchette , Uwe Waldmann , Daniel Wand
date = 20161112
topic = Logic/Rewriting
abstract = This Isabelle/HOL formalization defines Knuth–Bendix orders for higherorder terms without lambdaabstraction and proves many useful properties about them. The main order fully coincides with the standard transfinite KBO with subterm coefficients on firstorder terms. It appears promising as the basis of a higherorder superposition calculus.
notify = jasmin.blanchette@gmail.com
[Lambda_Free_EPO]
title = Formalization of the Embedding Path Order for LambdaFree HigherOrder Terms
author = Alexander Bentkamp
topic = Logic/Rewriting
date = 20181019
notify = a.bentkamp@vu.nl
abstract =
This Isabelle/HOL formalization defines the Embedding Path Order (EPO)
for higherorder terms without lambdaabstraction and proves many
useful properties about it. In contrast to the lambdafree recursive
path orders, it does not fully coincide with RPO on firstorder terms,
but it is compatible with arbitrary higherorder contexts.
[Nested_Multisets_Ordinals]
title = Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals
author = Jasmin Christian Blanchette , Mathias Fleury , Dmitriy Traytel
date = 20161112
topic = Logic/Rewriting
abstract = This Isabelle/HOL formalization introduces a nested multiset datatype and defines Dershowitz and Manna's nested multiset order. The order is proved well founded and linear. By removing one constructor, we transform the nested multisets into hereditary multisets. These are isomorphic to the syntactic ordinals—the ordinals can be recursively expressed in Cantor normal form. Addition, subtraction, multiplication, and linear orders are provided on this type.
notify = jasmin.blanchette@gmail.com
[AbstractRewriting]
title = Abstract Rewriting
topic = Logic/Rewriting
date = 20100614
author = Christian Sternagel , René Thiemann
license = LGPL
abstract =
We present an Isabelle formalization of abstract rewriting (see, e.g.,
the book by Baader and Nipkow). First, we define standard relations like
joinability, meetability, conversion, etc. Then, we
formalize important properties of abstract rewrite systems, e.g.,
confluence and strong normalization. Our main concern is on strong
normalization, since this formalization is the basis of CeTA (which is
mainly about strong normalization of term rewrite systems). Hence lemmas
involving strong normalization constitute by far the biggest part of this
theory. One of those is Newman's lemma.
extrahistory =
Change history:
[20100917]: Added theories defining several (ordered)
semirings related to strong normalization and giving some standard
instances.
[20131016]: Generalized deltaorders from rationals to Archimedean fields.
notify = christian.sternagel@uibk.ac.at, rene.thiemann@uibk.ac.at
[First_Order_Terms]
title = FirstOrder Terms
author = Christian Sternagel , René Thiemann
topic = Logic/Rewriting, Computer science/Algorithms
license = LGPL
date = 20180206
notify = c.sternagel@gmail.com, rene.thiemann@uibk.ac.at
abstract =
We formalize basic results on firstorder terms, including matching and a
firstorder unification algorithm, as well as wellfoundedness of the
subsumption order. This entry is part of the Isabelle
Formalization of Rewriting IsaFoR,
where firstorder terms are omnipresent: the unification algorithm is
used to certify several confluence and termination techniques, like
criticalpair computation and dependency graph approximations; and the
subsumption order is a crucial ingredient for completion.
[FreeGroups]
title = Free Groups
author = Joachim Breitner
date = 20100624
topic = Mathematics/Algebra
abstract =
Free Groups are, in a sense, the most generic kind of group. They
are defined over a set of generators with no additional relations in between
them. They play an important role in the definition of group presentations
and in other fields. This theory provides the definition of Free Group as
the set of fully canceled words in the generators. The universal property is
proven, as well as some isomorphisms results about Free Groups.
extrahistory =
Change history:
[20111211]: Added the Ping Pong Lemma.
notify =
[CofGroups]
title = An Example of a Cofinitary Group in Isabelle/HOL
author = Bart Kastermans
date = 20090804
topic = Mathematics/Algebra
abstract = We formalize the usual proof that the group generated by the function k > k + 1 on the integers gives rise to a cofinitary group.
notify = nipkow@in.tum.de
[GroupRingModule]
title = Groups, Rings and Modules
author = Hidetsune Kobayashi <>, L. Chen <>, H. Murao <>
date = 20040518
topic = Mathematics/Algebra
abstract = The theory of groups, rings and modules is developed to a great depth. Group theory results include Zassenhaus's theorem and the JordanHoelder theorem. The ring theory development includes ideals, quotient rings and the Chinese remainder theorem. The module development includes the Nakayama lemma, exact sequences and Tensor products.
notify = lp15@cam.ac.uk
[RobbinsConjecture]
title = A Complete Proof of the Robbins Conjecture
author = Matthew WamplerDoty <>
date = 20100522
topic = Mathematics/Algebra
abstract = This document gives a formalization of the proof of the Robbins conjecture, following A. Mann, A Complete Proof of the Robbins Conjecture, 2003.
notify = nipkow@in.tum.de
[Valuation]
title = Fundamental Properties of Valuation Theory and Hensel's Lemma
author = Hidetsune Kobayashi <>
date = 20070808
topic = Mathematics/Algebra
abstract = Convergence with respect to a valuation is discussed as convergence of a Cauchy sequence. Cauchy sequences of polynomials are defined. They are used to formalize Hensel's lemma.
notify = lp15@cam.ac.uk
[Rank_Nullity_Theorem]
title = RankNullity Theorem in Linear Algebra
author = Jose Divasón , Jesús Aransay
topic = Mathematics/Algebra
date = 20130116
abstract = In this contribution, we present some formalizations based on the HOLMultivariateAnalysis session of Isabelle. Firstly, a generalization of several theorems of such library are presented. Secondly, some definitions and proofs involving Linear Algebra and the four fundamental subspaces of a matrix are shown. Finally, we present a proof of the result known in Linear Algebra as the ``RankNullity Theorem'', which states that, given any linear map f from a finite dimensional vector space V to a vector space W, then the dimension of V is equal to the dimension of the kernel of f (which is a subspace of V) and the dimension of the range of f (which is a subspace of W). The proof presented here is based on the one given by Sheldon Axler in his book Linear Algebra Done Right. As a corollary of the previous theorem, and taking advantage of the relationship between linear maps and matrices, we prove that, for every matrix A (which has associated a linear map between finite dimensional vector spaces), the sum of its null space and its column space (which is equal to the range of the linear map) is equal to the number of columns of A.
extrahistory =
Change history:
[20140714]: Added some generalizations that allow us to formalize the RankNullity Theorem over finite dimensional vector spaces, instead of over the more particular euclidean spaces. Updated abstract.
notify = jose.divasonm@unirioja.es, jesusmaria.aransay@unirioja.es
[Affine_Arithmetic]
title = Affine Arithmetic
author = Fabian Immler
date = 20140207
topic = Mathematics/Analysis
abstract =
We give a formalization of affine forms as abstract representations of zonotopes.
We provide affine operations as well as overapproximations of some nonaffine operations like multiplication and division.
Expressions involving those operations can automatically be turned into (executable) functions approximating the original
expression in affine arithmetic.
extrahistory =
Change history:
[20150131]: added algorithm for zonotope/hyperplane intersection
[20170920]: linear approximations for all symbols from the floatarith data
type
notify = immler@in.tum.de
[Laplace_Transform]
title = Laplace Transform
author = Fabian Immler
topic = Mathematics/Analysis
date = 20190814
notify = fimmler@cs.cmu.edu
abstract =
This entry formalizes the Laplace transform and concrete Laplace
transforms for arithmetic functions, frequency shift, integration and
(higher) differentiation in the time domain. It proves Lerch's
lemma and uniqueness of the Laplace transform for continuous
functions. In order to formalize the foundational assumptions, this
entry contains a formalization of piecewise continuous functions and
functions of exponential order.
[Cauchy]
title = Cauchy's Mean Theorem and the CauchySchwarz Inequality
author = Benjamin Porter <>
date = 20060314
topic = Mathematics/Analysis
abstract = This document presents the mechanised proofs of two popular theorems attributed to Augustin Louis Cauchy  Cauchy's Mean Theorem and the CauchySchwarz Inequality.
notify = kleing@cse.unsw.edu.au
[Integration]
title = Integration theory and random variables
author = Stefan Richter
date = 20041119
topic = Mathematics/Analysis
abstract = Lebesguestyle integration plays a major role in advanced probability. We formalize concepts of elementary measure theory, realvalued random variables as Borelmeasurable functions, and a stepwise inductive definition of the integral itself. All proofs are carried out in human readable style using the Isar language.
extranote = Note: This article is of historical interest only. Lebesguestyle integration and probability theory are now available as part of the Isabelle/HOL distribution (directory Probability).
notify = richter@informatik.rwthaachen.de, nipkow@in.tum.de, hoelzl@in.tum.de
[Ordinary_Differential_Equations]
title = Ordinary Differential Equations
author = Fabian Immler , Johannes Hölzl
topic = Mathematics/Analysis
date = 20120426
abstract =
Session OrdinaryDifferentialEquations formalizes ordinary differential equations (ODEs) and initial value
problems. This work comprises proofs for local and global existence of unique solutions
(PicardLindelöf theorem). Moreover, it contains a formalization of the (continuous or even
differentiable) dependency of the flow on initial conditions as the flow of ODEs.
Not in the generated document are the following sessions:
 HOLODENumerics:
Rigorous numerical algorithms for computing enclosures of solutions based on RungeKutta methods
and affine arithmetic. Reachability analysis with splitting and reduction at hyperplanes.
 HOLODEExamples:
Applications of the numerical algorithms to concrete systems of ODEs.
 Lorenz_C0, Lorenz_C1:
Verified algorithms for checking C1information according to Tucker's proof,
computation of C0information.
extrahistory =
Change history:
[20140213]: added an implementation of the Euler method based on affine arithmetic
[20160414]: added flow and variational equation
[20160803]: numerical algorithms for reachability analysis (using secondorder RungeKutta methods, splitting, and reduction) implemented using Lammich's framework for automatic refinement
[20170920]: added Poincare map and propagation of variational equation in
reachability analysis, verified algorithms for C1information and computations
for C0information of the Lorenz attractor.
notify = immler@in.tum.de, hoelzl@in.tum.de
[Polynomials]
title = Executable Multivariate Polynomials
author = Christian Sternagel , René Thiemann , Alexander Maletzky , Fabian Immler , Florian Haftmann , Andreas Lochbihler , Alexander Bentkamp
date = 20100810
topic = Mathematics/Analysis, Mathematics/Algebra, Computer science/Algorithms/Mathematical
license = LGPL
abstract =
We define multivariate polynomials over arbitrary (ordered) semirings in
combination with (executable) operations like addition, multiplication,
and substitution. We also define (weak) monotonicity of polynomials and
comparison of polynomials where we provide standard estimations like
absolute positiveness or the more recent approach of Neurauter, Zankl,
and Middeldorp. Moreover, it is proven that strongly normalizing
(monotone) orders can be lifted to strongly normalizing (monotone) orders
over polynomials. Our formalization was performed as part of the IsaFoR/CeTAsystem
which contains several termination techniques. The provided theories have
been essential to formalize polynomial interpretations.
This formalization also contains an abstract representation as coefficient functions with finite
support and a type of powerproducts. If this type is ordered by a linear (term) ordering, various
additional notions, such as leading powerproduct, leading coefficient etc., are introduced as
well. Furthermore, a lot of generic properties of, and functions on, multivariate polynomials are
formalized, including the substitution and evaluation homomorphisms, embeddings of polynomial rings
into larger rings (i.e. with one additional indeterminate), homogenization and dehomogenization of
polynomials, and the canonical isomorphism between R[X,Y] and R[X][Y].
extrahistory =
Change history:
[20100917]: Moved theories on arbitrary (ordered) semirings to Abstract Rewriting.
[20161028]: Added abstract representation of polynomials and authors Maletzky/Immler.
[20180123]: Added authors Haftmann, Lochbihler after incorporating
their formalization of multivariate polynomials based on Polynomial mappings.
Moved material from Bentkamp's entry "Deep Learning".
[20190418]: Added material about polynomials whose powerproducts are represented themselves
by polynomial mappings.
notify = rene.thiemann@uibk.ac.at, christian.sternagel@uibk.ac.at, alexander.maletzky@risc.jku.at, immler@in.tum.de
[Sqrt_Babylonian]
title = Computing Nth Roots using the Babylonian Method
author = René Thiemann
date = 20130103
topic = Mathematics/Analysis
license = LGPL
abstract =
We implement the Babylonian method to compute nth roots of numbers.
We provide precise algorithms for naturals, integers and rationals, and
offer an approximation algorithm for square roots over linear ordered fields. Moreover, there
are precise algorithms to compute the floor and the ceiling of nth roots.
extrahistory =
Change history:
[20131016]: Added algorithms to compute floor and ceiling of sqrt of integers.
[20140711]: Moved NthRoot_Impl from RealImpl to this entry.
notify = rene.thiemann@uibk.ac.at
[Sturm_Sequences]
title = Sturm's Theorem
author = Manuel Eberl
date = 20140111
topic = Mathematics/Analysis
abstract = Sturm's Theorem states that polynomial sequences with certain
properties, socalled Sturm sequences, can be used to count the number
of real roots of a real polynomial. This work contains a proof of
Sturm's Theorem and code for constructing Sturm sequences efficiently.
It also provides the “sturm” proof method, which can decide certain
statements about the roots of real polynomials, such as “the polynomial
P has exactly n roots in the interval I” or “P(x) > Q(x) for all x
∈ ℝ”.
notify = eberlm@in.tum.de
[Sturm_Tarski]
title = The SturmTarski Theorem
author = Wenda Li
date = 20140919
topic = Mathematics/Analysis
abstract = We have formalized the SturmTarski theorem (also referred as the Tarski theorem), which generalizes Sturm's theorem. Sturm's theorem is usually used as a way to count distinct real roots, while the SturmTarksi theorem forms the basis for Tarski's classic quantifier elimination for real closed field.
notify = wl302@cam.ac.uk
[Markov_Models]
title = Markov Models
author = Johannes Hölzl , Tobias Nipkow
date = 20120103
topic = Mathematics/Probability theory, Computer science/Automata and formal languages
abstract = This is a formalization of Markov models in Isabelle/HOL. It
builds on Isabelle's probability theory. The available models are
currently DiscreteTime Markov Chains and a extensions of them with
rewards.
As application of these models we formalize probabilistic model
checking of pCTL formulas, analysis of IPv4 address allocation in
ZeroConf and an analysis of the anonymity of the Crowds protocol.
See here for the corresponding paper.
notify = hoelzl@in.tum.de
[Probabilistic_System_Zoo]
title = A Zoo of Probabilistic Systems
author = Johannes Hölzl ,
Andreas Lochbihler ,
Dmitriy Traytel
date = 20150527
topic = Computer science/Automata and formal languages
abstract =
Numerous models of probabilistic systems are studied in the literature.
Coalgebra has been used to classify them into system types and compare their
expressiveness. We formalize the resulting hierarchy of probabilistic system
types by modeling the semantics of the different systems as codatatypes.
This approach yields simple and concise proofs, as bisimilarity coincides
with equality for codatatypes.
This work is described in detail in the ITP 2015 publication by the authors.
notify = traytel@in.tum.de
[Density_Compiler]
title = A Verified Compiler for Probability Density Functions
author = Manuel Eberl , Johannes Hölzl , Tobias Nipkow
date = 20141009
topic = Mathematics/Probability theory, Computer science/Programming languages/Compiling
abstract =
Bhat et al. [TACAS 2013] developed an inductive compiler that computes
density functions for probability spaces described by programs in a
probabilistic functional language. In this work, we implement such a
compiler for a modified version of this language within the theorem prover
Isabelle and give a formal proof of its soundness w.r.t. the semantics of
the source and target language. Together with Isabelle's code generation
for inductive predicates, this yields a fully verified, executable density
compiler. The proof is done in two steps: First, an abstract compiler
working with abstract functions modelled directly in the theorem prover's
logic is defined and proved sound. Then, this compiler is refined to a
concrete version that returns a targetlanguage expression.
An article with the same title and authors is published in the proceedings
of ESOP 2015.
A detailed presentation of this work can be found in the first author's
master's thesis.
notify = hoelzl@in.tum.de
[CAVA_Automata]
title = The CAVA Automata Library
author = Peter Lammich
date = 20140528
topic = Computer science/Automata and formal languages
abstract =
We report on the graph and automata library that is used in the fully
verified LTL model checker CAVA.
As most components of CAVA use some type of graphs or automata, a common
automata library simplifies assembly of the components and reduces
redundancy.
The CAVA Automata Library provides a hierarchy of graph and automata
classes, together with some standard algorithms.
Its object oriented design allows for sharing of algorithms, theorems,
and implementations between its classes, and also simplifies extensions
of the library.
Moreover, it is integrated into the Automatic Refinement Framework,
supporting automatic refinement of the abstract automata types to
efficient data structures.
Note that the CAVA Automata Library is work in progress. Currently, it
is very specifically tailored towards the requirements of the CAVA model
checker.
Nevertheless, the formalization techniques presented here allow an
extension of the library to a wider scope. Moreover, they are not
limited to graph libraries, but apply to class hierarchies in general.
The CAVA Automata Library is described in the paper: Peter Lammich, The
CAVA Automata Library, Isabelle Workshop 2014.
notify = lammich@in.tum.de
[LTL]
title = Linear Temporal Logic
author = Salomon Sickert
contributors = Benedikt Seidl
date = 20160301
topic = Logic/General logic/Temporal logic, Computer science/Automata and formal languages
abstract =
This theory provides a formalisation of linear temporal logic (LTL)
and unifies previous formalisations within the AFP. This entry
establishes syntax and semantics for this logic and decouples it from
existing entries, yielding a common environment for theories reasoning
about LTL. Furthermore a parser written in SML and an executable
simplifier are provided.
extrahistory =
Change history:
[20190312]:
Support for additional operators, implementation of common equivalence relations,
definition of syntactic fragments of LTL and the minimal disjunctive normal form.
notify = sickert@in.tum.de
[LTL_to_GBA]
title = Converting LinearTime Temporal Logic to Generalized Büchi Automata
author = Alexander Schimpf , Peter Lammich
date = 20140528
topic = Computer science/Automata and formal languages
abstract =
We formalize lineartime temporal logic (LTL) and the algorithm by Gerth
et al. to convert LTL formulas to generalized Büchi automata.
We also formalize some syntactic rewrite rules that can be applied to
optimize the LTL formula before conversion.
Moreover, we integrate the Stuttering Equivalence AFPEntry by Stefan
Merz, adapting the lemma that nextfree LTL formula cannot distinguish
between stuttering equivalent runs to our setting.
We use the Isabelle Refinement and Collection framework, as well as the
Autoref tool, to obtain a refined version of our algorithm, from which
efficiently executable code can be extracted.
notify = lammich@in.tum.de
[Gabow_SCC]
title = Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm
author = Peter Lammich
date = 20140528
topic = Computer science/Algorithms/Graph, Mathematics/Graph theory
abstract =
We present an Isabelle/HOL formalization of Gabow's algorithm for
finding the strongly connected components of a directed graph.
Using data refinement techniques, we extract efficient code that
performs comparable to a reference implementation in Java.
Our style of formalization allows for reusing large parts of the proofs
when defining variants of the algorithm. We demonstrate this by
verifying an algorithm for the emptiness check of generalized Büchi
automata, reusing most of the existing proofs.
notify = lammich@in.tum.de
[Promela]
title = Promela Formalization
author = René Neumann
date = 20140528
topic = Computer science/System description languages
abstract =
We present an executable formalization of the language Promela, the
description language for models of the model checker SPIN. This
formalization is part of the work for a completely verified model
checker (CAVA), but also serves as a useful (and executable!)
description of the semantics of the language itself, something that is
currently missing.
The formalization uses three steps: It takes an abstract syntax tree
generated from an SML parser, removes syntactic sugar and enriches it
with type information. This further gets translated into a transition
system, on which the semantic engine (read: successor function) operates.
notify =
[CAVA_LTL_Modelchecker]
title = A Fully Verified Executable LTL Model Checker
author = Javier Esparza ,
Peter Lammich ,
René Neumann ,
Tobias Nipkow ,
Alexander Schimpf ,
JanGeorg Smaus
date = 20140528
topic = Computer science/Automata and formal languages
abstract =
We present an LTL model checker whose code has been completely verified
using the Isabelle theorem prover. The checker consists of over 4000
lines of ML code. The code is produced using the Isabelle Refinement
Framework, which allows us to split its correctness proof into (1) the
proof of an abstract version of the checker, consisting of a few hundred
lines of ``formalized pseudocode'', and (2) a verified refinement step
in which mathematical sets and other abstract structures are replaced by
implementations of efficient structures like redblack trees and
functional arrays. This leads to a checker that,
while still slower than unverified checkers, can already be used as a
trusted reference implementation against which advanced implementations
can be tested.
An early version of this model checker is described in the
CAV 2013 paper
with the same title.
notify = lammich@in.tum.de
[Fermat3_4]
title = Fermat's Last Theorem for Exponents 3 and 4 and the Parametrisation of Pythagorean Triples
author = Roelof Oosterhuis <>
date = 20070812
topic = Mathematics/Number theory
abstract = This document presents the mechanised proofs of
 Fermat's Last Theorem for exponents 3 and 4 and
 the parametrisation of Pythagorean Triples.
notify = nipkow@in.tum.de, roelofoosterhuis@gmail.com
[PerfectNumberThm]
title = Perfect Number Theorem
author = Mark Ijbema
date = 20091122
topic = Mathematics/Number theory
abstract = These theories present the mechanised proof of the Perfect Number Theorem.
notify = nipkow@in.tum.de
[SumSquares]
title = Sums of Two and Four Squares
author = Roelof Oosterhuis <>
date = 20070812
topic = Mathematics/Number theory
abstract = This document presents the mechanised proofs of the following results: any prime number of the form 4m+1 can be written as the sum of two squares;
 any natural number can be written as the sum of four squares
notify = nipkow@in.tum.de, roelofoosterhuis@gmail.com
[Lehmer]
title = Lehmer's Theorem
author = Simon Wimmer , Lars Noschinski
date = 20130722
topic = Mathematics/Number theory
abstract = In 1927, Lehmer presented criterions for primality, based on the converse of Fermat's litte theorem. This work formalizes the second criterion from Lehmer's paper, a necessary and sufficient condition for primality.
As a side product we formalize some properties of Euler's phifunction,
the notion of the order of an element of a group, and the cyclicity of the multiplicative group of a finite field.
notify = noschinl@gmail.com, simon.wimmer@tum.de
[Pratt_Certificate]
title = Pratt's Primality Certificates
author = Simon Wimmer , Lars Noschinski
date = 20130722
topic = Mathematics/Number theory
abstract = In 1975, Pratt introduced a proof system for certifying primes. He showed that a number p is prime iff a primality certificate for p exists. By showing a logarithmic upper bound on the length of the certificates in size of the prime number, he concluded that the decision problem for prime numbers is in NP. This work formalizes soundness and completeness of Pratt's proof system as well as an upper bound for the size of the certificate.
notify = noschinl@gmail.com, simon.wimmer@tum.de
[Monad_Memo_DP]
title = Monadification, Memoization and Dynamic Programming
author = Simon Wimmer , Shuwei Hu , Tobias Nipkow
topic = Computer science/Programming languages/Transformations, Computer science/Algorithms, Computer science/Functional programming
date = 20180522
notify = wimmers@in.tum.de
abstract =
We present a lightweight framework for the automatic verified
(functional or imperative) memoization of recursive functions. Our
tool can turn a pure Isabelle/HOL function definition into a
monadified version in a state monad or the Imperative HOL heap monad,
and prove a correspondence theorem. We provide a variety of memory
implementations for the two types of monads. A number of simple
techniques allow us to achieve bottomup computation and
spaceefficient memoization. The framework’s utility is demonstrated
on a number of representative dynamic programming problems. A detailed
description of our work can be found in the accompanying paper [2].
[Probabilistic_Timed_Automata]
title = Probabilistic Timed Automata
author = Simon Wimmer , Johannes Hölzl
topic = Mathematics/Probability theory, Computer science/Automata and formal languages
date = 20180524
notify = wimmers@in.tum.de, hoelzl@in.tum.de
abstract =
We present a formalization of probabilistic timed automata (PTA) for
which we try to follow the formula MDP + TA = PTA as far as possible:
our work starts from our existing formalizations of Markov decision
processes (MDP) and timed automata (TA) and combines them modularly.
We prove the fundamental result for probabilistic timed automata: the
region construction that is known from timed automata carries over to
the probabilistic setting. In particular, this allows us to prove that
minimum and maximum reachability probabilities can be computed via a
reduction to MDP model checking, including the case where one wants to
disregard unrealizable behavior. Further information can be found in
our ITP paper [2].
[Hidden_Markov_Models]
title = Hidden Markov Models
author = Simon Wimmer
topic = Mathematics/Probability theory, Computer science/Algorithms
date = 20180525
notify = wimmers@in.tum.de
abstract =
This entry contains a formalization of hidden Markov models [3] based
on Johannes Hölzl's formalization of discrete time Markov chains
[1]. The basic definitions are provided and the correctness of two
main (dynamic programming) algorithms for hidden Markov models is
proved: the forward algorithm for computing the likelihood of an
observed sequence, and the Viterbi algorithm for decoding the most
probable hidden state sequence. The Viterbi algorithm is made
executable including memoization. Hidden markov models have various
applications in natural language processing. For an introduction see
Jurafsky and Martin [2].
[ArrowImpossibilityGS]
title = Arrow and GibbardSatterthwaite
author = Tobias Nipkow
date = 20080901
topic = Mathematics/Games and economics
abstract = This article formalizes two proofs of Arrow's impossibility theorem due to Geanakoplos and derives the GibbardSatterthwaite theorem as a corollary. One formalization is based on utility functions, the other one on strict partial orders.
An article about these proofs is found here.
notify = nipkow@in.tum.de
[SenSocialChoice]
title = Some classical results in Social Choice Theory
author = Peter Gammie
date = 20081109
topic = Mathematics/Games and economics
abstract = Drawing on Sen's landmark work "Collective Choice and Social Welfare" (1970), this development proves Arrow's General Possibility Theorem, Sen's Liberal Paradox and May's Theorem in a general setting. The goal was to make precise the classical statements and proofs of these results, and to provide a foundation for more recent results such as the GibbardSatterthwaite and DugganSchwartz theorems.
notify = nipkow@in.tum.de
[Vickrey_Clarke_Groves]
title = VCG  Combinatorial VickreyClarkeGroves Auctions
author = Marco B. Caminati <>, Manfred Kerber , Christoph Lange, Colin Rowat
date = 20150430
topic = Mathematics/Games and economics
abstract =
A VCG auction (named after their inventors Vickrey, Clarke, and
Groves) is a generalization of the singlegood, second price Vickrey
auction to the case of a combinatorial auction (multiple goods, from
which any participant can bid on each possible combination). We
formalize in this entry VCG auctions, including tiebreaking and prove
that the functions for the allocation and the price determination are
welldefined. Furthermore we show that the allocation function
allocates goods only to participants, only goods in the auction are
allocated, and no good is allocated twice. We also show that the price
function is nonnegative. These properties also hold for the
automatically extracted Scala code.
notify = mnfrd.krbr@gmail.com
[Topology]
title = Topology
author = Stefan Friedrich <>
date = 20040426
topic = Mathematics/Topology
abstract = This entry contains two theories. The first, Topology, develops the basic notions of general topology. The second, which can be viewed as a demonstration of the first, is called LList_Topology. It develops the topology of lazy lists.
notify = lcp@cl.cam.ac.uk
[Knot_Theory]
title = Knot Theory
author = T.V.H. Prathamesh
date = 20160120
topic = Mathematics/Topology
abstract =
This work contains a formalization of some topics in knot theory.
The concepts that were formalized include definitions of tangles, links,
framed links and link/tangle equivalence. The formalization is based on a
formulation of links in terms of tangles. We further construct and prove the
invariance of the Bracket polynomial. Bracket polynomial is an invariant of
framed links closely linked to the Jones polynomial. This is perhaps the first
attempt to formalize any aspect of knot theory in an interactive proof assistant.
notify = prathamesh@imsc.res.in
[Graph_Theory]
title = Graph Theory
author = Lars Noschinski
date = 20130428
topic = Mathematics/Graph theory
abstract = This development provides a formalization of directed graphs, supporting (labelled) multiedges and infinite graphs. A polymorphic edge type allows edges to be treated as pairs of vertices, if multiedges are not required. Formalized properties are i.a. walks (and related concepts), connectedness and subgraphs and basic properties of isomorphisms.
This formalization is used to prove characterizations of Euler Trails, Shortest Paths and Kuratowski subgraphs.
notify = noschinl@gmail.com
[Planarity_Certificates]
title = Planarity Certificates
author = Lars Noschinski
date = 20151111
topic = Mathematics/Graph theory
abstract =
This development provides a formalization of planarity based on
combinatorial maps and proves that Kuratowski's theorem implies
combinatorial planarity.
Moreover, it contains verified implementations of programs checking
certificates for planarity (i.e., a combinatorial map) or nonplanarity
(i.e., a Kuratowski subgraph).
notify = noschinl@gmail.com
[MaxCardMatching]
title = Maximum Cardinality Matching
author = Christine Rizkallah
date = 20110721
topic = Mathematics/Graph theory
abstract =
A matching in a graph G is a subset M of the
edges of G such that no two share an endpoint. A matching has maximum
cardinality if its cardinality is at least as large as that of any other
matching. An oddset cover OSC of a graph G is a
labeling of the nodes of G with integers such that every edge of
G is either incident to a node labeled 1 or connects two nodes
labeled with the same number i ≥ 2.
This article proves Edmonds theorem:
Let M be a matching in a graph G and let OSC be an
oddset cover of G.
For any i ≥ 0, let n(i) be the number of nodes
labeled i. If M = n(1) +
∑_{i ≥ 2}(n(i) div 2),
then M is a maximum cardinality matching.
notify = nipkow@in.tum.de
[Girth_Chromatic]
title = A Probabilistic Proof of the GirthChromatic Number Theorem
author = Lars Noschinski
date = 20120206
topic = Mathematics/Graph theory
abstract = This works presents a formalization of the GirthChromatic number theorem in graph theory, stating that graphs with arbitrarily large girth and chromatic number exist. The proof uses the theory of Random Graphs to prove the existence with probabilistic arguments.
notify = noschinl@gmail.com
[Random_Graph_Subgraph_Threshold]
title = Properties of Random Graphs  Subgraph Containment
author = Lars Hupel
date = 20140213
topic = Mathematics/Graph theory, Mathematics/Probability theory
abstract = Random graphs are graphs with a fixed number of vertices, where each edge is present with a fixed probability. We are interested in the probability that a random graph contains a certain pattern, for example a cycle or a clique. A very high edge probability gives rise to perhaps too many edges (which degrades performance for many algorithms), whereas a low edge probability might result in a disconnected graph. We prove a theorem about a threshold probability such that a higher edge probability will asymptotically almost surely produce a random graph with the desired subgraph.
notify = hupel@in.tum.de
[FlyspeckTame]
title = Flyspeck I: Tame Graphs
author = Gertrud Bauer <>, Tobias Nipkow
date = 20060522
topic = Mathematics/Graph theory
abstract =
These theories present the verified enumeration of tame plane graphs
as defined by Thomas C. Hales in his proof of the Kepler Conjecture in his
book Dense Sphere Packings. A Blueprint for Formal Proofs. [CUP 2012].
The values of the constants in the definition of tameness are identical to
those in the Flyspeck project.
The IJCAR 2006 paper by Nipkow, Bauer and Schultz refers to the original version of Hales' proof,
the ITP 2011 paper by Nipkow refers to the Blueprint version of the proof.
extrahistory =
Change history:
[20101102]: modified theories to reflect the modified definition of tameness in Hales' revised proof.
[20140703]: modified constants in def of tameness and Archive according to the final state of the Flyspeck proof.
notify = nipkow@in.tum.de
[Well_Quasi_Orders]
title = WellQuasiOrders
author = Christian Sternagel
date = 20120413
topic = Mathematics/Combinatorics
abstract = Based on Isabelle/HOL's type class for preorders,
we introduce a type class for wellquasiorders (wqo)
which is characterized by the absence of "bad" sequences
(our proofs are along the lines of the proof of NashWilliams,
from which we also borrow terminology). Our main results are
instantiations for the product type, the list type, and a type of finite trees,
which (almost) directly follow from our proofs of (1) Dickson's Lemma, (2)
Higman's Lemma, and (3) Kruskal's Tree Theorem. More concretely:
 If the sets A and B are wqo then their Cartesian product is wqo.
 If the set A is wqo then the set of finite lists over A is wqo.
 If the set A is wqo then the set of finite trees over A is wqo.
The research was funded by the Austrian Science Fund (FWF): J3202.
extrahistory =
Change history:
[20120611]: Added Kruskal's Tree Theorem.
[20121219]: New variant of Kruskal's tree theorem for terms (as opposed to
variadic terms, i.e., trees), plus finite version of the tree theorem as
corollary.
[20130516]: Simplified construction of minimal bad sequences.
[20140709]: Simplified proofs of Higman's lemma and Kruskal's tree theorem,
based on homogeneous sequences.
[20160103]: An alternative proof of Higman's lemma by open induction.
[20170608]: Proved (classical) equivalence to inductive definition of
almostfull relations according to the ITP 2012 paper "Stop When You Are
AlmostFull" by Vytiniotis, Coquand, and Wahlstedt.
notify = c.sternagel@gmail.com
[Marriage]
title = Hall's Marriage Theorem
author = Dongchen Jiang , Tobias Nipkow
date = 20101217
topic = Mathematics/Combinatorics
abstract = Two proofs of Hall's Marriage Theorem: one due to Halmos and Vaughan, one due to Rado.
extrahistory =
Change history:
[20110909]: Added Rado's proof
notify = nipkow@in.tum.de
[Bondy]
title = Bondy's Theorem
author = Jeremy Avigad , Stefan Hetzl
date = 20121027
topic = Mathematics/Combinatorics
abstract = A proof of Bondy's theorem following B. Bollabas, Combinatorics, 1986, Cambridge University Press.
notify = avigad@cmu.edu, hetzl@logic.at
[RamseyInfinite]
title = Ramsey's theorem, infinitary version
author = Tom Ridge <>
date = 20040920
topic = Mathematics/Combinatorics
abstract = This formalization of Ramsey's theorem (infinitary version) is taken from Boolos and Jeffrey, Computability and Logic, 3rd edition, Chapter 26. It differs slightly from the text by assuming a slightly stronger hypothesis. In particular, the induction hypothesis is stronger, holding for any infinite subset of the naturals. This avoids the rather peculiar mapping argument between kj and aikj on p.263, which is unnecessary and slightly mars this really beautiful result.
notify = lp15@cam.ac.uk
[Derangements]
title = Derangements Formula
author = Lukas Bulwahn
date = 20150627
topic = Mathematics/Combinatorics
abstract =
The Derangements Formula describes the number of fixpointfree permutations
as a closed formula. This theorem is the 88th theorem in a list of the
``Top 100 Mathematical Theorems''.
notify = lukas.bulwahn@gmail.com
[Euler_Partition]
title = Euler's Partition Theorem
author = Lukas Bulwahn
date = 20151119
topic = Mathematics/Combinatorics
abstract =
Euler's Partition Theorem states that the number of partitions with only
distinct parts is equal to the number of partitions with only odd parts.
The combinatorial proof follows John Harrison's HOL Light formalization.
This theorem is the 45th theorem of the Top 100 Theorems list.
notify = lukas.bulwahn@gmail.com
[Discrete_Summation]
title = Discrete Summation
author = Florian Haftmann
contributors = Amine Chaieb <>
date = 20140413
topic = Mathematics/Combinatorics
abstract = These theories introduce basic concepts and proofs about discrete summation: shifts, formal summation, falling factorials and stirling numbers. As proof of concept, a simple summation conversion is provided.
notify = florian.haftmann@informatik.tumuenchen.de
[Open_Induction]
title = Open Induction
author = Mizuhito Ogawa <>, Christian Sternagel
date = 20121102
topic = Mathematics/Combinatorics
abstract =
A proof of the open induction schema based on J.C. Raoult, Proving open properties by induction, Information Processing Letters 29, 1988, pp.1923.
This research was supported by the Austrian Science Fund (FWF): J3202.
notify = c.sternagel@gmail.com
[Category]
title = Category Theory to Yoneda's Lemma
author = Greg O'Keefe
date = 20050421
topic = Mathematics/Category theory
license = LGPL
abstract = This development proves Yoneda's lemma and aims to be readable by humans. It only defines what is needed for the lemma: categories, functors and natural transformations. Limits, adjunctions and other important concepts are not included.
extrahistory =
Change history:
[20100423]: The definition of the constant equinumerous was slightly too weak in the original submission and has been fixed in revision 8c2b5b3c995f.
notify = lcp@cl.cam.ac.uk
[Category2]
title = Category Theory
author = Alexander Katovsky
date = 20100620
topic = Mathematics/Category theory
abstract = This article presents a development of Category Theory in Isabelle/HOL. A Category is defined using records and locales. Functors and Natural Transformations are also defined. The main result that has been formalized is that the Yoneda functor is a full and faithful embedding. We also formalize the completeness of many sorted monadic equational logic. Extensive use is made of the HOLZF theory in both cases. For an informal description see here [pdf].
notify = alexander.katovsky@cantab.net
[FunWithFunctions]
title = Fun With Functions
author = Tobias Nipkow
date = 20080826
topic = Mathematics/Misc
abstract = This is a collection of cute puzzles of the form ``Show that if a function satisfies the following constraints, it must be ...'' Please add further examples to this collection!
notify = nipkow@in.tum.de
[FunWithTilings]
title = Fun With Tilings
author = Tobias Nipkow , Lawrence C. Paulson
date = 20081107
topic = Mathematics/Misc
abstract = Tilings are defined inductively. It is shown that one form of mutilated chess board cannot be tiled with dominoes, while another one can be tiled with Lshaped tiles. Please add further fun examples of this kind!
notify = nipkow@in.tum.de
[LazyListsII]
title = Lazy Lists II
author = Stefan Friedrich <>
date = 20040426
topic = Computer science/Data structures
abstract = This theory contains some useful extensions to the LList (lazy list) theory by Larry Paulson, including finite, infinite, and positive llists over an alphabet, as well as the new constants take and drop and the prefix order of llists. Finally, the notions of safety and liveness in the sense of Alpern and Schneider (1985) are defined.
notify = lcp@cl.cam.ac.uk
[Ribbon_Proofs]
title = Ribbon Proofs
author = John Wickerson <>
date = 20130119
topic = Computer science/Programming languages/Logics
abstract = This document concerns the theory of ribbon proofs: a diagrammatic proof system, based on separation logic, for verifying program correctness. We include the syntax, proof rules, and soundness results for two alternative formalisations of ribbon proofs. Compared to traditional proof outlines, ribbon proofs emphasise the structure of a proof, so are intelligible and pedagogical. Because they contain less redundancy than proof outlines, and allow each proof step to be checked locally, they may be more scalable. Where proof outlines are cumbersome to modify, ribbon proofs can be visually manoeuvred to yield proofs of variant programs.
notify =
[Koenigsberg_Friendship]
title = The Königsberg Bridge Problem and the Friendship Theorem
author = Wenda Li
date = 20130719
topic = Mathematics/Graph theory
abstract = This development provides a formalization of undirected graphs and simple graphs, which are based on Benedikt Nordhoff and Peter Lammich's simple formalization of labelled directed graphs in the archive. Then, with our formalization of graphs, we show both necessary and sufficient conditions for Eulerian trails and circuits as well as the fact that the Königsberg Bridge Problem does not have a solution. In addition, we show the Friendship Theorem in simple graphs.
notify =
[Tree_Decomposition]
title = Tree Decomposition
author = Christoph Dittmann
notify =
date = 20160531
topic = Mathematics/Graph theory
abstract =
We formalize tree decompositions and tree width in Isabelle/HOL,
proving that trees have treewidth 1. We also show that every edge of
a tree decomposition is a separation of the underlying graph. As an
application of this theorem we prove that complete graphs of size n
have treewidth n1.
[Menger]
title = Menger's Theorem
author = Christoph Dittmann
topic = Mathematics/Graph theory
date = 20170226
notify = isabelle@christophd.de
abstract =
We present a formalization of Menger's Theorem for directed and
undirected graphs in Isabelle/HOL. This wellknown result shows that
if two nonadjacent distinct vertices u, v in a directed graph have no
separator smaller than n, then there exist n internally
vertexdisjoint paths from u to v. The version for undirected graphs
follows immediately because undirected graphs are a special case of
directed graphs.
[IEEE_Floating_Point]
title = A Formal Model of IEEE Floating Point Arithmetic
author = Lei Yu
contributors = Fabian Hellauer , Fabian Immler
date = 20130727
topic = Computer science/Data structures
abstract = This development provides a formal model of IEEE754 floatingpoint arithmetic. This formalization, including formal specification of the standard and proofs of important properties of floatingpoint arithmetic, forms the foundation for verifying programs with floatingpoint computation. There is also a code generation setup for floats so that we can execute programs using this formalization in functional programming languages.
notify = lp15@cam.ac.uk, immler@in.tum.de
extrahistory =
Change history:
[20170925]: Added conversions from and to software floating point numbers
(by Fabian Hellauer and Fabian Immler).
[20180205]: 'Modernized' representation following the formalization in HOL4:
former "float_format" and predicate "is_valid" is now encoded in a type "('e, 'f) float" where
'e and 'f encode the size of exponent and fraction.
[Native_Word]
title = Native Word
author = Andreas Lochbihler
contributors = Peter Lammich
date = 20130917
topic = Computer science/Data structures
abstract = This entry makes machine words and machine arithmetic available for code generation from Isabelle/HOL. It provides a common abstraction that hides the differences between the different target languages. The code generator maps these operations to the APIs of the target languages. Apart from that, we extend the available bit operations on types int and integer, and map them to the operations in the target languages.
extrahistory =
Change history:
[20131106]:
added conversion function between native words and characters
(revision fd23d9a7fe3a)
[20140331]:
added words of default size in the target language (by Peter Lammich)
(revision 25caf5065833)
[20141006]:
proper test setup with compilation and execution of tests in all target languages
(revision 5d7a1c9ae047)
[20170902]:
added 64bit words (revision c89f86244e3c)
[20180715]:
added cast operators for defaultsize words (revision fc1f1fb8dd30)
notify = mail@andreaslochbihler.de
[XML]
title = XML
author = Christian Sternagel , René Thiemann
date = 20141003
topic = Computer science/Functional programming, Computer science/Data structures
abstract =
This entry provides an XML library for Isabelle/HOL. This includes parsing
and pretty printing of XML trees as well as combinators for transforming XML
trees into arbitrary userdefined data. The main contribution of this entry is
an interface (fit for code generation) that allows for communication between
verified programs formalized in Isabelle/HOL and the outside world via XML.
This library was developed as part of the IsaFoR/CeTA project
to which we refer for examples of its usage.
notify = c.sternagel@gmail.com, rene.thiemann@uibk.ac.at
[HereditarilyFinite]
title = The Hereditarily Finite Sets
author = Lawrence C. Paulson
date = 20131117
topic = Logic/Set theory
abstract = The theory of hereditarily finite sets is formalised, following
the development of Swierczkowski.
An HF set is a finite collection of other HF sets; they enjoy an induction principle
and satisfy all the axioms of ZF set theory apart from the axiom of infinity, which is negated.
All constructions that are possible in ZF set theory (Cartesian products, disjoint sums, natural numbers,
functions) without using infinite sets are possible here.
The definition of addition for the HF sets follows Kirby.
This development forms the foundation for the Isabelle proof of Gödel's incompleteness theorems,
which has been formalised separately.
extrahistory =
Change history:
[20150223]: Added the theory "Finitary" defining the class of types that can be embedded in hf, including int, char, option, list, etc.
notify = lp15@cam.ac.uk
[Incompleteness]
title = Gödel's Incompleteness Theorems
author = Lawrence C. Paulson
date = 20131117
topic = Logic/Proof theory
abstract = Gödel's two incompleteness theorems are formalised, following a careful presentation by Swierczkowski, in the theory of hereditarily finite sets. This represents the first ever machineassisted proof of the second incompleteness theorem. Compared with traditional formalisations using Peano arithmetic (see e.g. Boolos), coding is simpler, with no need to formalise the notion
of multiplication (let alone that of a prime number)
in the formalised calculus upon which the theorem is based.
However, other technical problems had to be solved in order to complete the argument.
notify = lp15@cam.ac.uk
[Finite_Automata_HF]
title = Finite Automata in Hereditarily Finite Set Theory
author = Lawrence C. Paulson
date = 20150205
topic = Computer science/Automata and formal languages
abstract = Finite Automata, both deterministic and nondeterministic, for regular languages.
The MyhillNerode Theorem. Closure under intersection, concatenation, etc.
Regular expressions define regular languages. Closure under reversal;
the powerset construction mapping NFAs to DFAs. Left and right languages; minimal DFAs.
Brzozowski's minimization algorithm. Uniqueness up to isomorphism of minimal DFAs.
notify = lp15@cam.ac.uk
[DecreasingDiagrams]
title = Decreasing Diagrams
author = Harald Zankl
license = LGPL
date = 20131101
topic = Logic/Rewriting
abstract = This theory contains a formalization of decreasing diagrams showing that any locally decreasing abstract rewrite system is confluent. We consider the valley (van Oostrom, TCS 1994) and the conversion version (van Oostrom, RTA 2008) and closely follow the original proofs. As an application we prove Newman's lemma.
notify = Harald.Zankl@uibk.ac.at
[DecreasingDiagramsII]
title = Decreasing Diagrams II
author = Bertram Felgenhauer
license = LGPL
date = 20150820
topic = Logic/Rewriting
abstract = This theory formalizes the commutation version of decreasing diagrams for ChurchRosser modulo. The proof follows Felgenhauer and van Oostrom (RTA 2013). The theory also provides important specializations, in particular van Oostrom’s conversion version (TCS 2008) of decreasing diagrams.
notify = bertram.felgenhauer@uibk.ac.at
[GoedelGod]
title = Gödel's God in Isabelle/HOL
author = Christoph Benzmüller , Bruno Woltzenlogel Paleo
date = 20131112
topic = Logic/Philosophical aspects
abstract = Dana Scott's version of Gödel's proof of God's existence is formalized in quantified
modal logic KB (QML KB).
QML KB is modeled as a fragment of classical higherorder logic (HOL);
thus, the formalization is essentially a formalization in HOL.
notify = lp15@cam.ac.uk, c.benzmueller@fuberlin.de
[Types_Tableaus_and_Goedels_God]
title = Types, Tableaus and Gödel’s God in Isabelle/HOL
author = David Fuenmayor , Christoph Benzmüller
topic = Logic/Philosophical aspects
date = 20170501
notify = davfuenmayor@gmail.com, c.benzmueller@gmail.com
abstract =
A computerformalisation of the essential parts of Fitting's
textbook "Types, Tableaus and Gödel's God" in
Isabelle/HOL is presented. In particular, Fitting's (and
Anderson's) variant of the ontological argument is verified and
confirmed. This variant avoids the modal collapse, which has been
criticised as an undesirable sideeffect of Kurt Gödel's (and
Dana Scott's) versions of the ontological argument.
Fitting's work is employing an intensional higherorder modal
logic, which we shallowly embed here in classical higherorder logic.
We then utilize the embedded logic for the formalisation of
Fitting's argument. (See also the earlier AFP entry ``Gödel's God in Isabelle/HOL''.)
[GewirthPGCProof]
title = Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL
author = David Fuenmayor , Christoph Benzmüller
topic = Logic/Philosophical aspects
date = 20181030
notify = davfuenmayor@gmail.com, c.benzmueller@gmail.com
abstract =
An ambitious ethical theory Alan Gewirth's "Principle of
Generic Consistency" is encoded and analysed in Isabelle/HOL.
Gewirth's theory has stirred much attention in philosophy and
ethics and has been proposed as a potential means to bound the impact
of artificial general intelligence.
extrahistory =
Change history:
[20190409]:
added proof for a stronger variant of the PGC and examplary inferences
(revision 88182cb0a2f6)
[Lowe_Ontological_Argument]
title = Computerassisted Reconstruction and Assessment of E. J. Lowe's Modal Ontological Argument
author = David Fuenmayor , Christoph Benzmüller
topic = Logic/Philosophical aspects
date = 20170921
notify = davfuenmayor@gmail.com, c.benzmueller@gmail.com
abstract =
Computers may help us to understand not just verify philosophical
arguments. By utilizing modern proof assistants in an iterative
interpretive process, we can reconstruct and assess an argument by
fully formal means. Through the mechanization of a variant of St.
Anselm's ontological argument by E. J. Lowe, which is a
paradigmatic example of a naturallanguage argument with strong ties
to metaphysics and religion, we offer an ideal showcase for our
computerassisted interpretive method.
[AnselmGod]
title = Anselm's God in Isabelle/HOL
author = Ben Blumson
topic = Logic/Philosophical aspects
date = 20170906
notify = benblumson@gmail.com
abstract =
Paul Oppenheimer and Edward Zalta's formalisation of
Anselm's ontological argument for the existence of God is
automated by embedding a free logic for definite descriptions within
Isabelle/HOL.
[Tail_Recursive_Functions]
title = A General Method for the Proof of Theorems on Tailrecursive Functions
author = Pasquale Noce
date = 20131201
topic = Computer science/Functional programming
abstract =
Tailrecursive function definitions are sometimes more straightforward than
alternatives, but proving theorems on them may be roundabout because of the
peculiar form of the resulting recursion induction rules.
This paper describes a proof method that provides a general solution to
this problem by means of suitable invariants over inductive sets, and
illustrates the application of such method by examining two case studies.
notify = pasquale.noce.lavoro@gmail.com
[CryptoBasedCompositionalProperties]
title = Compositional Properties of CryptoBased Components
author = Maria Spichkova
date = 20140111
topic = Computer science/Security
abstract = This paper presents an Isabelle/HOL set of theories which allows the specification of cryptobased components and the verification of their composition properties wrt. cryptographic aspects. We introduce a formalisation of the security property of data secrecy, the corresponding definitions and proofs. Please note that here we import the Isabelle/HOL theory ListExtras.thy, presented in the AFP entry FocusStreamsCaseStudiesAFP.
notify = maria.spichkova@rmit.edu.au
[Featherweight_OCL]
title = Featherweight OCL: A Proposal for a MachineChecked Formal Semantics for OCL 2.5
author = Achim D. Brucker , Frédéric Tuong , Burkhart Wolff
date = 20140116
topic = Computer science/System description languages
abstract = The Unified Modeling Language (UML) is one of the few
modeling languages that is widely used in industry. While
UML is mostly known as diagrammatic modeling language
(e.g., visualizing class models), it is complemented by a
textual language, called Object Constraint Language
(OCL). The current version of OCL is based on a fourvalued
logic that turns UML into a formal language. Any type
comprises the elements "invalid" and "null" which are
propagated as strict and nonstrict, respectively.
Unfortunately, the former semiformal semantics of this
specification language, captured in the "Annex A" of the
OCL standard, leads to different interpretations of corner
cases. We formalize the core of OCL: denotational
definitions, a logical calculus and operational rules that
allow for the execution of OCL expressions by a mixture of
term rewriting and code compilation. Our formalization
reveals several inconsistencies and contradictions in the
current version of the OCL standard. Overall, this document
is intended to provide the basis for a machinechecked text
"Annex A" of the OCL standard targeting at tool
implementors.
extrahistory =
Change history:
[20151013]:
afpdevel@ea3b38fc54d6 and
holtestgen@12148
Update of Featherweight OCL including a change in the abstract.
[20140116]:
afpdevel@9091ce05cb20 and
holtestgen@10241
New Entry: Featherweight OCL
notify = brucker@spamfence.net, tuong@users.gforge.inria.fr, wolff@lri.fr
[Relation_Algebra]
title = Relation Algebra
author = Alasdair Armstrong <>,
Simon Foster ,
Georg Struth ,
Tjark Weber
date = 20140125
topic = Mathematics/Algebra
abstract = Tarski's algebra of binary relations is formalised along the lines of
the standard textbooks of Maddux and Schmidt and Ströhlein. This
includes relationalgebraic concepts such as subidentities, vectors and
a domain operation as well as various notions associated to functions.
Relation algebras are also expanded by a reflexive transitive closure
operation, and they are linked with Kleene algebras and models of binary
relations and Boolean matrices.
notify = g.struth@sheffield.ac.uk, tjark.weber@it.uu.se
[PSemigroupsConvolution]
title = Partial Semigroups and Convolution Algebras
author = Brijesh Dongol , Victor B. F. Gomes , Ian J. Hayes , Georg Struth
topic = Mathematics/Algebra
date = 20170613
notify = g.struth@sheffield.ac.uk, victor.gomes@cl.cam.ac.uk
abstract =
Partial Semigroups are relevant to the foundations of quantum
mechanics and combinatorics as well as to interval and separation
logics. Convolution algebras can be understood either as algebras of
generalised binary modalities over ternary Kripke frames, in
particular over partial semigroups, or as algebras of quantalevalued
functions which are equipped with a convolutionstyle operation of
multiplication that is parametrised by a ternary relation. Convolution
algebras provide algebraic semantics for various substructural logics,
including categorial, relevance and linear logics, for separation
logic and for interval logics; they cover quantitative and qualitative
applications. These mathematical components for partial semigroups and
convolution algebras provide uniform foundations from which models of
computation based on relations, program traces or pomsets, and
verification components for separation or interval temporal logics can
be built with little effort.
[Secondary_Sylow]
title = Secondary Sylow Theorems
author = Jakob von Raumer
date = 20140128
topic = Mathematics/Algebra
abstract = These theories extend the existing proof of the first Sylow theorem
(written by Florian Kammueller and L. C. Paulson) by what are often
called the second, third and fourth Sylow theorems. These theorems
state propositions about the number of Sylow psubgroups of a group
and the fact that they are conjugate to each other. The proofs make
use of an implementation of group actions and their properties.
notify = psxjv4@nottingham.ac.uk
[Jordan_Hoelder]
title = The JordanHölder Theorem
author = Jakob von Raumer
date = 20140909
topic = Mathematics/Algebra
abstract = This submission contains theories that lead to a formalization of the proof of the JordanHölder theorem about composition series of finite groups. The theories formalize the notions of isomorphism classes of groups, simple groups, normal series, composition series, maximal normal subgroups. Furthermore, they provide proofs of the second isomorphism theorem for groups, the characterization theorem for maximal normal subgroups as well as many useful lemmas about normal subgroups and factor groups. The proof is inspired by course notes of Stuart Rankin.
notify = psxjv4@nottingham.ac.uk
[Cayley_Hamilton]
title = The CayleyHamilton Theorem
author = Stephan Adelsberger ,
Stefan Hetzl ,
Florian Pollak
date = 20140915
topic = Mathematics/Algebra
abstract =
This document contains a proof of the CayleyHamilton theorem
based on the development of matrices in HOL/Multivariate Analysis.
notify = stvienna@gmail.com
[Probabilistic_Noninterference]
title = Probabilistic Noninterference
author = Andrei Popescu , Johannes Hölzl
date = 20140311
topic = Computer science/Security
abstract = We formalize a probabilistic noninterference for a multithreaded language with uniform scheduling, where probabilistic behaviour comes from both the scheduler and the individual threads. We define notions probabilistic noninterference in two variants: resumptionbased and tracebased. For the resumptionbased notions, we prove compositionality w.r.t. the language constructs and establish sound typesystemlike syntactic criteria. This is a formalization of the mathematical development presented at CPP 2013 and CALCO 2013. It is the probabilistic variant of the Possibilistic Noninterference AFP entry.
notify = hoelzl@in.tum.de
[HyperCTL]
title = A shallow embedding of HyperCTL*
author = Markus N. Rabe , Peter Lammich , Andrei Popescu
date = 20140416
topic = Computer science/Security, Logic/General logic/Temporal logic
abstract = We formalize HyperCTL*, a temporal logic for expressing security properties. We
first define a shallow embedding of HyperCTL*, within which we prove inductive and coinductive
rules for the operators. Then we show that a HyperCTL* formula captures GoguenMeseguer
noninterference, a landmark information flow property. We also define a deep embedding and
connect it to the shallow embedding by a denotational semantics, for which we prove sanity w.r.t.
dependence on the free variables. Finally, we show that under some finiteness assumptions about
the model, noninterference is given by a (finitary) syntactic formula.
notify = uuomul@yahoo.com
[Bounded_Deducibility_Security]
title = BoundedDeducibility Security
author = Andrei Popescu , Peter Lammich
date = 20140422
topic = Computer science/Security
abstract = This is a formalization of boundeddeducibility security (BD
security), a flexible notion of informationflow security applicable
to arbitrary inputoutput automata. It generalizes Sutherland's
classic notion of nondeducibility by factoring in declassification
bounds and trigger, whereas nondeducibility states that, in a
system, information cannot flow between specified sources and sinks,
BD security indicates upper bounds for the flow and triggers under
which these upper bounds are no longer guaranteed.
notify = uuomul@yahoo.com, lammich@in.tum.de
[Network_Security_Policy_Verification]
title = Network Security Policy Verification
author = Cornelius Diekmann
date = 20140704
topic = Computer science/Security
abstract =
We present a unified theory for verifying network security policies.
A security policy is represented as directed graph.
To check highlevel security goals, security invariants over the policy are
expressed. We cover monotonic security invariants, i.e. prohibiting more does not harm
security. We provide the following contributions for the security invariant theory.
 Secure autocompletion of scenariospecific knowledge, which eases usability.
 Security violations can be repaired by tightening the policy iff the
security invariants hold for the denyall policy.
 An algorithm to compute a security policy.
 A formalization of stateful connection semantics in network security mechanisms.
 An algorithm to compute a secure stateful implementation of a policy.
 An executable implementation of all the theory.
 Examples, ranging from an aircraft cabin data network to the analysis
of a large realworld firewall.
 More examples: A fully automated translation of highlevel security goals to both
firewall and SDN configurations (see Examples/Distributed_WebApp.thy).
For a detailed description, see
 C. Diekmann, A. Korsten, and G. Carle.
Demonstrating
topoS: Theoremproverbased synthesis of secure network configurations.
In 2nd International Workshop on Management of SDN and NFV Systems, manSDN/NFV, Barcelona, Spain, November 2015.
 C. Diekmann, S.A. Posselt, H. Niedermayer, H. Kinkelin, O. Hanka, and G. Carle.
Verifying Security Policies using Host Attributes.
In FORTE, 34th IFIP International Conference on Formal Techniques for Distributed Objects,
Components and Systems, Berlin, Germany, June 2014.
 C. Diekmann, L. Hupel, and G. Carle. Directed Security Policies:
A Stateful Network Implementation.
In J. Pang and Y. Liu, editors, Engineering Safety and Security Systems,
volume 150 of Electronic Proceedings in Theoretical Computer Science,
pages 2034, Singapore, May 2014. Open Publishing Association.
extrahistory =
Change history:
[20150414]:
Added Distributed WebApp example and improved graphviz visualization
(revision 4dde08ca2ab8)
notify = diekmann@net.in.tum.de
[Abstract_Completeness]
title = Abstract Completeness
author = Jasmin Christian Blanchette , Andrei Popescu , Dmitriy Traytel
date = 20140416
topic = Logic/Proof theory
abstract = A formalization of an abstract property of possibly infinite derivation trees (modeled by a codatatype), representing the core of a proof (in Beth/Hintikka style) of the firstorder logic completeness theorem, independent of the concrete syntax or inference rules. This work is described in detail in the IJCAR 2014 publication by the authors.
The abstract proof can be instantiated for a wide range of Gentzen and tableau systems as well as various flavors of FOLe.g., with or without predicates, equality, or sorts. Here, we give only a toy example instantiation with classical propositional logic. A more serious instancemanysorted FOL with equalityis described elsewhere [Blanchette and Popescu, FroCoS 2013].
notify = traytel@in.tum.de
[Pop_Refinement]
title = PopRefinement
author = Alessandro Coglio
date = 20140703
topic = Computer science/Programming languages/Misc
abstract = Poprefinement is an approach to stepwise refinement, carried out inside an interactive theorem prover by constructing a monotonically decreasing sequence of predicates over deeply embedded target programs. The sequence starts with a predicate that characterizes the possible implementations, and ends with a predicate that characterizes a unique program in explicit syntactic form. Poprefinement enables more requirements (e.g. programlevel and nonfunctional) to be captured in the initial specification and preserved through refinement. Security requirements expressed as hyperproperties (i.e. predicates over sets of traces) are always preserved by poprefinement, unlike the popular notion of refinement as trace set inclusion. Two simple examples in Isabelle/HOL are presented, featuring programlevel requirements, nonfunctional requirements, and hyperproperties.
notify = coglio@kestrel.edu
[VectorSpace]
title = Vector Spaces
author = Holden Lee
date = 20140829
topic = Mathematics/Algebra
abstract = This formalisation of basic linear algebra is based completely on locales, building off HOLAlgebra. It includes basic definitions: linear combinations, span, linear independence; linear transformations; interpretation of function spaces as vector spaces; the direct sum of vector spaces, sum of subspaces; the replacement theorem; existence of bases in finitedimensional; vector spaces, definition of dimension; the ranknullity theorem. Some concepts are actually defined and proved for modules as they also apply there. Infinitedimensional vector spaces are supported, but dimension is only supported for finitedimensional vector spaces. The proofs are standard; the proofs of the replacement theorem and ranknullity theorem roughly follow the presentation in Linear Algebra by Friedberg, Insel, and Spence. The ranknullity theorem generalises the existing development in the Archive of Formal Proof (originally using type classes, now using a mix of type classes and locales).
notify = holdenl@princeton.edu
[Special_Function_Bounds]
title = RealValued Special Functions: Upper and Lower Bounds
author = Lawrence C. Paulson
date = 20140829
topic = Mathematics/Analysis
abstract = This development proves upper and lower bounds for several familiar realvalued functions. For sin, cos, exp and sqrt, it defines and verifies infinite families of upper and lower bounds, mostly based on Taylor series expansions. For arctan, ln and exp, it verifies a finite collection of upper and lower bounds, originally obtained from the functions' continued fraction expansions using the computer algebra system Maple. A common theme in these proofs is to take the difference between a function and its approximation, which should be zero at one point, and then consider the sign of the derivative. The immediate purpose of this development is to verify axioms used by MetiTarski, an automatic theorem prover for realvalued special functions. Crucial to MetiTarski's operation is the provision of upper and lower bounds for each function of interest.
notify = lp15@cam.ac.uk
[Landau_Symbols]
title = Landau Symbols
author = Manuel Eberl
date = 20150714
topic = Mathematics/Analysis
abstract = This entry provides Landau symbols to describe and reason about the asymptotic growth of functions for sufficiently large inputs. A number of simplification procedures are provided for additional convenience: cancelling of dominated terms in sums under a Landau symbol, cancelling of common factors in products, and a decision procedure for Landau expressions containing products of powers of functions like x, ln(x), ln(ln(x)) etc.
notify = eberlm@in.tum.de
[Error_Function]
title = The Error Function
author = Manuel Eberl
topic = Mathematics/Analysis
date = 20180206
notify = eberlm@in.tum.de
abstract =
This entry provides the definitions and basic properties of
the complex and real error function erf and the complementary error
function erfc. Additionally, it gives their full asymptotic
expansions.
[Akra_Bazzi]
title = The AkraBazzi theorem and the Master theorem
author = Manuel Eberl
date = 20150714
topic = Mathematics/Analysis
abstract = This article contains a formalisation of the AkraBazzi method
based on a proof by Leighton. It is a generalisation of the wellknown
Master Theorem for analysing the complexity of Divide & Conquer algorithms.
We also include a generalised version of the Master theorem based on the
AkraBazzi theorem, which is easier to apply than the AkraBazzi theorem
itself.
Some proof methods that facilitate applying the Master theorem are also
included. For a more detailed explanation of the formalisation and the
proof methods, see the accompanying paper (publication forthcoming).
notify = eberlm@in.tum.de
[Dirichlet_Series]
title = Dirichlet Series
author = Manuel Eberl
topic = Mathematics/Number theory
date = 20171012
notify = eberlm@in.tum.de
abstract =
This entry is a formalisation of much of Chapters 2, 3, and 11 of
Apostol's “Introduction to Analytic Number
Theory”. This includes:
 Definitions and
basic properties for several numbertheoretic functions (Euler's
φ, Möbius μ, Liouville's λ,
the divisor function σ, von Mangoldt's
Λ)
 Executable code for most of these
functions, the most efficient implementations using the factoring
algorithm by Thiemann et al.
 Dirichlet products and formal Dirichlet series
 Analytic results connecting convergent formal Dirichlet
series to complex functions
 Euler product
expansions
 Asymptotic estimates of
numbertheoretic functions including the density of squarefree
integers and the average number of divisors of a natural
number
These results are useful as a basis for
developing more numbertheoretic results, such as the Prime Number
Theorem.
[Gauss_Sums]
title = Gauss Sums and the Pólya–Vinogradov Inequality
author = Rodrigo Raya , Manuel Eberl
topic = Mathematics/Number theory
date = 20191210
notify = manuel.eberl@tum.de
abstract =
This article provides a full formalisation of Chapter 8 of
Apostol's Introduction
to Analytic Number Theory. Subjects that are
covered are:
 periodic arithmetic
functions and their finite Fourier series
 (generalised) Ramanujan sums
 Gauss sums
and separable characters
 induced moduli and
primitive characters
 the
Pólya—Vinogradov inequality
[Zeta_Function]
title = The Hurwitz and Riemann ζ Functions
author = Manuel Eberl
topic = Mathematics/Number theory, Mathematics/Analysis
date = 20171012
notify = eberlm@in.tum.de
abstract =
This entry builds upon the results about formal and analytic Dirichlet
series to define the Hurwitz ζ function ζ(a,s) and,
based on that, the Riemann ζ function ζ(s).
This is done by first defining them for ℜ(z) > 1
and then successively extending the domain to the left using the
Euler–MacLaurin formula.
Apart from the most basic facts such as analyticity, the following
results are provided:
 the Stieltjes constants and the Laurent expansion of
ζ(s) at s = 1
 the nonvanishing of ζ(s)
for ℜ(z) ≥ 1
 the relationship between ζ(a,s) and Γ
 the special values at negative integers and positive even integers
 Hurwitz's formula and the reflection formula for ζ(s)
 the
Hadjicostas–Chapman formula
The entry also contains Euler's analytic proof of the infinitude of primes,
based on the fact that ζ(s) has a pole at s = 1.
[Linear_Recurrences]
title = Linear Recurrences
author = Manuel Eberl
topic = Mathematics/Analysis
date = 20171012
notify = eberlm@in.tum.de
abstract =
Linear recurrences with constant coefficients are an
interesting class of recurrence equations that can be solved
explicitly. The most famous example are certainly the Fibonacci
numbers with the equation f(n) =
f(n1) +
f(n  2) and the quite
nonobvious closed form
(φ^{n}

(φ)^{n})
/ √5 where φ is the golden ratio.
In this work, I build on existing tools in
Isabelle – such as formal power series and polynomial
factorisation algorithms – to develop a theory of these
recurrences and derive a fully executable solver for them that can be
exported to programming languages like Haskell.
[Lambert_W]
title = The Lambert W Function on the Reals
author = Manuel Eberl
topic = Mathematics/Analysis
date = 20200424
notify = eberlm@in.tum.de
abstract =
The Lambert W function is a multivalued
function defined as the inverse function of x
↦ x
e^{x}. Besides numerous
applications in combinatorics, physics, and engineering, it also
frequently occurs when solving equations containing both
e^{x} and
x, or both x and log
x.
This article provides a
definition of the two realvalued branches
W_{0}(x)
and
W_{1}(x)
and proves various properties such as basic identities and
inequalities, monotonicity, differentiability, asymptotic expansions,
and the MacLaurin series of
W_{0}(x)
at x = 0.
[Cartan_FP]
title = The Cartan Fixed Point Theorems
author = Lawrence C. Paulson
date = 20160308
topic = Mathematics/Analysis
abstract =
The Cartan fixed point theorems concern the group of holomorphic
automorphisms on a connected open set of C^{n}. Ciolli et al.
have formalised the onedimensional case of these theorems in HOL
Light. This entry contains their proofs, ported to Isabelle/HOL. Thus
it addresses the authors' remark that "it would be important to write
a formal proof in a language that can be read by both humans and
machines".
notify = lp15@cam.ac.uk
[Gauss_Jordan]
title = GaussJordan Algorithm and Its Applications
author = Jose Divasón , Jesús Aransay
topic = Computer science/Algorithms/Mathematical
date = 20140903
abstract = The GaussJordan algorithm states that any matrix over a field can be transformed by means of elementary row operations to a matrix in reduced row echelon form. The formalization is based on the Rank Nullity Theorem entry of the AFP and on the HOLMultivariateAnalysis session of Isabelle, where matrices are represented as functions over finite types. We have set up the code generator to make this representation executable. In order to improve the performance, a refinement to immutable arrays has been carried out. We have formalized some of the applications of the GaussJordan algorithm. Thanks to this development, the following facts can be computed over matrices whose elements belong to a field: Ranks, Determinants, Inverses, Bases and dimensions and Solutions of systems of linear equations. Code can be exported to SML and Haskell.
notify = jose.divasonm@unirioja.es, jesusmaria.aransay@unirioja.es
[Echelon_Form]
title = Echelon Form
author = Jose Divasón , Jesús Aransay
topic = Computer science/Algorithms/Mathematical, Mathematics/Algebra
date = 20150212
abstract = We formalize an algorithm to compute the Echelon Form of a matrix. We have proved its existence over Bézout domains and made it executable over Euclidean domains, such as the integer ring and the univariate polynomials over a field. This allows us to compute determinants, inverses and characteristic polynomials of matrices. The work is based on the HOLMultivariate Analysis library, and on both the GaussJordan and CayleyHamilton AFP entries. As a byproduct, some algebraic structures have been implemented (principal ideal domains, Bézout domains...). The algorithm has been refined to immutable arrays and code can be generated to functional languages as well.
notify = jose.divasonm@unirioja.es, jesusmaria.aransay@unirioja.es
[QR_Decomposition]
title = QR Decomposition
author = Jose Divasón , Jesús Aransay
topic = Computer science/Algorithms/Mathematical, Mathematics/Algebra
date = 20150212
abstract = QR decomposition is an algorithm to decompose a real matrix A into the product of two other matrices Q and R, where Q is orthogonal and R is invertible and upper triangular. The algorithm is useful for the least squares problem; i.e., the computation of the best approximation of an unsolvable system of linear equations. As a sideproduct, the GramSchmidt process has also been formalized. A refinement using immutable arrays is presented as well. The development relies, among others, on the AFP entry "Implementing field extensions of the form Q[sqrt(b)]" by René Thiemann, which allows execution of the algorithm using symbolic computations. Verified code can be generated and executed using floats as well.
extrahistory =
Change history:
[20150618]: The second part of the Fundamental Theorem of Linear Algebra has been generalized to more general inner product spaces.
notify = jose.divasonm@unirioja.es, jesusmaria.aransay@unirioja.es
[Hermite]
title = Hermite Normal Form
author = Jose Divasón , Jesús Aransay
topic = Computer science/Algorithms/Mathematical, Mathematics/Algebra
date = 20150707
abstract = Hermite Normal Form is a canonical matrix analogue of Reduced Echelon Form, but involving matrices over more general rings. In this work we formalise an algorithm to compute the Hermite Normal Form of a matrix by means of elementary row operations, taking advantage of the Echelon Form AFP entry. We have proven the correctness of such an algorithm and refined it to immutable arrays. Furthermore, we have also formalised the uniqueness of the Hermite Normal Form of a matrix. Code can be exported and some examples of execution involving integer matrices and polynomial matrices are presented as well.
notify = jose.divasonm@unirioja.es, jesusmaria.aransay@unirioja.es
[Imperative_Insertion_Sort]
title = Imperative Insertion Sort
author = Christian Sternagel
date = 20140925
topic = Computer science/Algorithms
abstract = The insertion sort algorithm of Cormen et al. (Introduction to Algorithms) is expressed in Imperative HOL and proved to be correct and terminating. For this purpose we also provide a theory about imperative loop constructs with accompanying induction/invariant rules for proving partial and total correctness. Furthermore, the formalized algorithm is fit for code generation.
notify = lp15@cam.ac.uk
[Stream_Fusion_Code]
title = Stream Fusion in HOL with Code Generation
author = Andreas Lochbihler , Alexandra Maximova
date = 20141010
topic = Computer science/Functional programming
abstract = Stream Fusion is a system for removing intermediate list data structures from functional programs, in particular Haskell. This entry adapts stream fusion to Isabelle/HOL and its code generator. We define stream types for finite and possibly infinite lists and stream versions for most of the fusible list functions in the theories List and Coinductive_List, and prove them correct with respect to the conversion functions between lists and streams. The Stream Fusion transformation itself is implemented as a simproc in the preprocessor of the code generator. [Brian Huffman's AFP entry formalises stream fusion in HOLCF for the domain of lazy lists to prove the GHC compiler rewrite rules correct. In contrast, this work enables Isabelle's code generator to perform stream fusion itself. To that end, it covers both finite and coinductive lists from the HOL library and the Coinductive entry. The fusible list functions require specification and proof principles different from Huffman's.]
notify = mail@andreaslochbihler.de
[Case_Labeling]
title = Generating Cases from Labeled Subgoals
author = Lars Noschinski
date = 20150721
topic = Tools, Computer science/Programming languages/Misc
abstract =
Isabelle/Isar provides named cases to structure proofs. This article
contains an implementation of a proof method casify, which can
be used to easily extend proof tools with support for named cases. Such
a proof tool must produce labeled subgoals, which are then interpreted
by casify.
As examples, this work contains verification condition generators
producing named cases for three languages: The Hoare language from
HOL/Library, a monadic language for computations with failure
(inspired by the AutoCorres tool), and a language of conditional
expressions. These VCGs are demonstrated by a number of example programs.
notify = noschinl@gmail.com
[DPTSATSolver]
title = A Fast SAT Solver for Isabelle in Standard ML
topic = Tools
author = Armin Heller <>
date = 20091209
abstract = This contribution contains a fast SAT solver for Isabelle written in Standard ML. By loading the theory DPT_SAT_Solver, the SAT solver installs itself (under the name ``dptsat'') and certain Isabelle tools like Refute will start using it automatically. This is a port of the DPT (Decision Procedure Toolkit) SAT Solver written in OCaml.
notify = jasmin.blanchette@gmail.com
[Rep_Fin_Groups]
title = Representations of Finite Groups
topic = Mathematics/Algebra
author = Jeremy Sylvestre
date = 20150812
abstract = We provide a formal framework for the theory of representations of finite groups, as modules over the group ring. Along the way, we develop the general theory of groups (relying on the group_add class for the basics), modules, and vector spaces, to the extent required for theory of group representations. We then provide formal proofs of several important introductory theorems in the subject, including Maschke's theorem, Schur's lemma, and Frobenius reciprocity. We also prove that every irreducible representation is isomorphic to a submodule of the group ring, leading to the fact that for a finite group there are only finitely many isomorphism classes of irreducible representations. In all of this, no restriction is made on the characteristic of the ring or field of scalars until the definition of a group representation, and then the only restriction made is that the characteristic must not divide the order of the group.
notify = jsylvest@ualberta.ca
[Noninterference_Inductive_Unwinding]
title = The Inductive Unwinding Theorem for CSP Noninterference Security
topic = Computer science/Security
author = Pasquale Noce
date = 20150818
abstract =
The necessary and sufficient condition for CSP noninterference security stated by the Ipurge Unwinding Theorem is expressed in terms of a pair of event lists varying over the set of process traces. This does not render it suitable for the subsequent application of rule induction in the case of a process defined inductively, since rule induction may rather be applied to a single variable ranging over an inductively defined set.
Starting from the Ipurge Unwinding Theorem, this paper derives a necessary and sufficient condition for CSP noninterference security that involves a single event list varying over the set of process traces, and is thus suitable for rule induction; hence its name, Inductive Unwinding Theorem. Similarly to the Ipurge Unwinding Theorem, the new theorem only requires to consider individual accepted and refused events for each process trace, and applies to the general case of a possibly intransitive noninterference policy. Specific variants of this theorem are additionally proven for deterministic processes and trace set processes.
notify = pasquale.noce.lavoro@gmail.com
[Password_Authentication_Protocol]
title = Verification of a DiffieHellman Passwordbased Authentication Protocol by Extending the Inductive Method
author = Pasquale Noce
topic = Computer science/Security
date = 20170103
notify = pasquale.noce.lavoro@gmail.com
abstract =
This paper constructs a formal model of a DiffieHellman
passwordbased authentication protocol between a user and a smart
card, and proves its security. The protocol provides for the dispatch
of the user's password to the smart card on a secure messaging
channel established by means of Password Authenticated Connection
Establishment (PACE), where the mapping method being used is Chip
Authentication Mapping. By applying and suitably extending
Paulson's Inductive Method, this paper proves that the protocol
establishes trustworthy secure messaging channels, preserves the
secrecy of users' passwords, and provides an effective mutual
authentication service. What is more, these security properties turn
out to hold independently of the secrecy of the PACE authentication
key.
[Jordan_Normal_Form]
title = Matrices, Jordan Normal Forms, and Spectral Radius Theory
topic = Mathematics/Algebra
author = René Thiemann , Akihisa Yamada
contributors = Alexander Bentkamp
date = 20150821
abstract =
Matrix interpretations are useful as measure functions in termination proving. In order to use these interpretations also for complexity analysis, the growth rate of matrix powers has to examined. Here, we formalized a central result of spectral radius theory, namely that the growth rate is polynomially bounded if and only if the spectral radius of a matrix is at most one.
To formally prove this result we first studied the growth rates of matrices in Jordan normal form, and prove the result that every complex matrix has a Jordan normal form using a constructive prove via Schur decomposition.
The whole development is based on a new abstract type for matrices, which is also executable by a suitable setup of the code generator. It completely subsumes our former AFPentry on executable matrices, and its main advantage is its close connection to the HMArepresentation which allowed us to easily adapt existing proofs on determinants.
All the results have been applied to improve CeTA, our certifier to validate termination and complexity proof certificates.
extrahistory =
Change history:
[20160107]: Added Schurdecomposition, GramSchmidt orthogonalization, uniqueness of Jordan normal forms
[20180417]: Integrated lemmas from deeplearning AFPentry of Alexander Bentkamp
notify = rene.thiemann@uibk.ac.at, ayamada@trs.cm.is.nagoyau.ac.jp
[LTL_to_DRA]
title = Converting Linear Temporal Logic to Deterministic (Generalized) Rabin Automata
topic = Computer science/Automata and formal languages
author = Salomon Sickert
date = 20150904
abstract = Recently, Javier Esparza and Jan Kretinsky proposed a new method directly translating linear temporal logic (LTL) formulas to deterministic (generalized) Rabin automata. Compared to the existing approaches of constructing a nondeterministic Buechiautomaton in the first step and then applying a determinization procedure (e.g. some variant of Safra's construction) in a second step, this new approach preservers a relation between the formula and the states of the resulting automaton. While the old approach produced a monolithic structure, the new method is compositional. Furthermore, in some cases the resulting automata are much smaller than the automata generated by existing approaches. In order to ensure the correctness of the construction, this entry contains a complete formalisation and verification of the translation. Furthermore from this basis executable code is generated.
extrahistory =
Change history:
[20150923]: Enable code export for the eager unfolding optimisation and reduce running time of the generated tool. Moreover, add support for the mlton SML compiler.
[20160324]: Make use of the LTL entry and include the simplifier.
notify = sickert@in.tum.de
[Timed_Automata]
title = Timed Automata
author = Simon Wimmer
date = 20160308
topic = Computer science/Automata and formal languages
abstract =
Timed automata are a widely used formalism for modeling realtime
systems, which is employed in a class of successful model checkers
such as UPPAAL [LPY97], HyTech [HHWt97] or Kronos [Yov97]. This work
formalizes the theory for the subclass of diagonalfree timed
automata, which is sufficient to model many interesting problems. We
first define the basic concepts and semantics of diagonalfree timed
automata. Based on this, we prove two types of decidability results
for the language emptiness problem. The first is the classic result
of Alur and Dill [AD90, AD94], which uses a finite partitioning of
the state space into socalled `regions`. Our second result focuses
on an approach based on `Difference Bound Matrices (DBMs)`, which is
practically used by model checkers. We prove the correctness of the
basic forward analysis operations on DBMs. One of these operations is
the FloydWarshall algorithm for the allpairs shortest paths problem.
To obtain a finite search space, a widening operation has to be used
for this kind of analysis. We use Patricia Bouyer's [Bou04] approach
to prove that this widening operation is correct in the sense that
DBMbased forward analysis in combination with the widening operation
also decides language emptiness. The interesting property of this
proof is that the first decidability result is reused to obtain the
second one.
notify = wimmers@in.tum.de
[Parity_Game]
title = Positional Determinacy of Parity Games
author = Christoph Dittmann
date = 20151102
topic = Mathematics/Games and economics, Mathematics/Graph theory
abstract =
We present a formalization of parity games (a twoplayer game on
directed graphs) and a proof of their positional determinacy in
Isabelle/HOL. This proof works for both finite and infinite games.
notify =
[Ergodic_Theory]
title = Ergodic Theory
author = Sebastien Gouezel
date = 20151201
topic = Mathematics/Probability theory
abstract = Ergodic theory is the branch of mathematics that studies the behaviour of measure preserving transformations, in finite or infinite measure. It interacts both with probability theory (mainly through measure theory) and with geometry as a lot of interesting examples are from geometric origin. We implement the first definitions and theorems of ergodic theory, including notably Poicaré recurrence theorem for finite measure preserving systems (together with the notion of conservativity in general), induced maps, Kac's theorem, Birkhoff theorem (arguably the most important theorem in ergodic theory), and variations around it such as conservativity of the corresponding skew product, or Atkinson lemma.
notify = sebastien.gouezel@univrennes1.fr, hoelzl@in.tum.de
[Latin_Square]
title = Latin Square
author = Alexander Bentkamp
date = 20151202
topic = Mathematics/Combinatorics
abstract =
A Latin Square is a n x n table filled with integers from 1 to n where each number appears exactly once in each row and each column. A Latin Rectangle is a partially filled n x n table with r filled rows and nr empty rows, such that each number appears at most once in each row and each column. The main result of this theory is that any Latin Rectangle can be completed to a Latin Square.
notify = bentkamp@gmail.com
[Deep_Learning]
title = Expressiveness of Deep Learning
author = Alexander Bentkamp