Introduction

Researchers are applying Isabelle to a broad range of problems. Further work has been presented at the 2007 Isabelle Workshop and at many conferences, such as FME, CADE and TPHOLs.

»[Isabelle]« means the material is included in the Isabelle distribution

This page is based upon information supplied by the researchers themselves. Comments and corrections are welcome at {webmaster} AT [isabelle.in.tum.de].

Formalized Mathematics

Simon Ambler and Roy Crole have used a deep encoding of syntax based on de Bruijn indices to formalize the operational semantics of a small functional programming language. This has enabled standard concepts of program equivalence to be presented uniformly through inductive and coinductive definitions. It is proved formally that applicative bisimulation is a congruence, and that it coincides with Morris-style contextual equivalence. A preliminary report is available as compressed postscript.

Jesús Aransay, Clemens Ballarin, and Julio Rubio work on formalisations in the domain of Algebraic Topology. The computer algebra systems EAT and Kenzo have been used to compute algebraic objects whose correctness hat not been, up to date (2003), confirmed or refuted by other theoretical or mechanical methods. The goal currently pursued is to obtain a mechanical proof of the Basic Perturbation Lemma, which is the theoretical basis for EAT and Kenzo, in Isabelle. An ulterior goal is the validation of algorithms implementing the Basic Perturbation Lemma. See Aransay's PhD thesis "Mechanized Reasoning in Homological Algebra", Universidad de La Rioja, 2006.

Jeremy Avigad, David Gray, and Adam Kramer are working to develop number theory in Isabelle. They have formalized Gauss' law of quadratic reciprocity and the prime number theorem. The latter development includes many useful contributions, such as a formalization of O-notation.

Pierre Castéran and Davy Rouillard are working on the CClair project. It intends to be a generic tool for proof and simulation activity on various classes of transitions systems. At this time, it uses HOL logic (with Paulson's lazy lists).

Louise Dennis is using Isabelle/HOL to prove theorems involving coinduction, guiding the proof with proof plans generated by CLaM rather than user interaction. Her method finds bisimulations automatically.

Jacques Fleuriot has mechanized the ultrapower construction of the hyperreals from Nonstandard Analysis (NSA) in Isabelle. Concepts from NSA and geometry theorem proving have been combined and applied to the mechanization of Propositions from Newton's Principia for his PhD thesis. This includes the famous Proposition Kepleriana. The framework has also been used to mechanize real analysis using nonstandard techniques.

Jacob Frost has mechanized Milner & Tofte's coinduction example in both HOL and ZF. [Isabelle]

Krzysztof Grabczewski has mechanized the first two chapters of Equivalents of the Axiom of Choice by Rubin and Rubin, in ZF. [Isabelle]

Slawomir Kolodynski is building a library of formalized mathematics within ZF. It has theorems about group theory, rings, general topology and an unfinished construction of real numbers as classes of integer almost homomorphisms.

Tobias Nipkow has proved the Church-Rosser Theorem for the lambda-calculus using a novel formalization, covering both the beta and the eta rules. [Isabelle]

Tobias Nipkow has mechanized the first 100 pages of Winskel's The Formal Semantics of Programming Languages, in HOL. This project extends the work of Lötzbeyer and Sandner. [Isabelle]

Larry Paulson has found a concise formalization and proof of the Mutilated Chess Board problem, using an inductive definition. [Isabelle]

Ole Steen Rasmussen has proved the Church-Rosser Theorem, porting Gérard Huet's Coq proof. [Isabelle]

René Vestergaard and James Brotherston have mechanized a confluence proof for the lambda-calculus. As a first, all inductive reasoning is conducted over first-order abstract syntax with one-sorted variable names. Curiously, a formal version of Barendregt's Variable Convention is needed. Raw and real calculi, related via alpha-collapse, are studied and their confluence properties are proved equivalent as are their equational theories. The proof development is modular with parts of Nipkow's work. See their paper: "A formalized first-order confluence proof for the lambda-calculus using one-sorted variable names". Inf. Comput. 183(2): 212-244 (2003).

Baris Sertkaya has proved some fundamental results and the Basic Theorem of Formal Concept Analysis in Isabelle/HOL following the book Formal Concept Analysis by Ganter and Wille. His master's thesis gives documentation and the source code of the formalization.

In connection with the Church Project, Ian Westmacott, Robert Muller, and Joe Wells have developed a Tofte-Talpin style region inference system for terms in a polymorphic programming language based on rank-2 intersection types and which subsumes core ML. The inference system, including terms, types, source language semantics and target language (store) semantics are all formalized in Isabelle as is a relation of consistency between values and stores. A number of properties are mechanically proven, including a proof of translation soundness.

Logical Investigations

David Basin and Stefan Friedrich have investigated a combination of the weak second-order monadic logic of one successor (WS1S) with higher-order logic (HOL). A semantic embedding of WS1S in HOL provides a basis for a secure integration of the MONA system, a decision procedure for WS1S, as an oracle in Isabelle's HOL. They describe methods for reducing problems formalized in HOL to problems in the language of WS1S, and present applications to arithmetic reasoning and proving properties of parameterized sequential systems.

David Basin, Seán Matthews and Luca Viganò are applying Isabelle to study presentations and combinations of non-classical logics (via labelled deductive systems). They have implemented a wide variety of modal logics (including K, D, T, B, KD45, S4, S4.2 S5), as well as several relevance logics. Papers describing the work are available from Luca Viganò.

Jeremy Dawson and Rajeev Goré are using Isabelle to mechanize Belnap's Display Logic (Journal of Philosophical Logic, 11:375-417, 1982) and its various extensions. Display Logic is a general methodology for obtaining cut-free Gentzen systems for a huge class of hybrid substructural logics in one uniform setting. To date they have mechanized classical tense logic Kt and the logic of Relation Algebras. For more details, and papers, please contact Rajeev at {rpg} AT [arp.anu.edu.au].

Sidi Ould Ehmety has used Isabelle/ZF set theory to formalize the Object Calculus, which Abadi and Cardelli developed for describing basic concepts of object-oriented programming. In preliminary results, the basic object-calculus (the pure untyped sigma-calculus) has been formalized.

Matt Fairtlough, Mike Holcombe, Michael Mendler and Xiaochun Cheng are working on the project Lax Logic applied to Formal System Design. The "Lax" in "Lax Logic" indicates the looseness associated with the notion of correctness-up-to constraints. We are investigating the proof theory and model theory of Lax Logic and have constructed an automatic theorem prover for Lax Logic for use in generating correctness proofs for combinational circuits. Because proofs in Lax Logic are constructive, it is possible to extract data-dependent constraints from them. Lax Logic also promises to be more widely applicable to the formal verification of software and of other types of hardware, as well as to more general notions of constraints and abstractions in artificial intelligence.

Jacob Frost has built an Isabelle implementation of a logic for reasoning about functional programs with imperative allocation, assignment and allocation effects on memory cells. The logic is a variant of VTLoE (Variable Typed Logic of Effects). This modern operational logic allows a large number of program properties to be expressed and reasoned about using a powerful yet simple logical language. His paper, "An Operational Logic of Effects", appeared in the Australasian Theorem Symposium (CATS'96).

Dirk Van Heule is using Isabelle as a proof tool for the Partial Predicate Logic. PPC is a three-valued logic, useful for proofs about programs.

Seán Matthews has used Isabelle to implement Feferman's theory of finitary inductive definitions, FS0.

David von Oheimb has implemented a Relation-Algebraic Language and Logic (RALL) with partially automatic proof facilities in Isabelle/HOL. (Reference for Relation Algebra: G. Schmidt and Th. Ströhlein. Relations and Graphs. Springer, 1993.)

Program Development

Abdelwaheb Ayari has interpreted the deductive tableaux system of Manna and Waldinger in Isabelle/HOL (this work is joint with David Basin ). In the future he will investigate the termination of functional programs in Isabelle.

David Basin is applying Isabelle to program development. His work concerns deriving program development calculi in higher-order logic and using higher-order resolution to carry out "proofs-as-programs" style program synthesis. Logical Framework Based Program Development gives a high-level overview. A Higher-Order Interpretation of Deductive Tableau describes an application to functional program synthesis and Modeling a Hardware Synthesis Methodology in Isabelle describes an application to hardware synthesis. Finally, Program Development Schemata as Derived Rules looks at applications to program transformation.

Marek Bednarczyk and Tomasz Borzyszkowski have developing a pLSD (Logic for Software Development). Using the theorem prover turns specification, development and verification into logical activities. A compiler from a simple arithmetical language to a stack machine is proved correct. Also present is the Isabelle/HOL proof (in progress) of the soundness of pLSD. Reports available; see also the Isabelle User Workshop.

Martin Coen's work on interactive development of functional is Isabelle's the object-logic CCL (Classical Computational Logic). Details may be found in his thesis. [Isabelle]

Johan Glimming (fomerly Larsson) mechanized category theory in Isabelle/HOL, studied an encoding of ZF-like sets, and mechanized portions of the Bird-Meertens Formalism for program calculation. He also defined the category GAL of Galois connections and the category CPO of complete partial orders and continuous functions. The work was a MSc project at the University of Oxford. Thesis and code are available.

Kolyang, Thomas Santen and Burkhart Wolff have embedded program transformations like GlobalSearch and DivideAndConquer into Isabelle (paper available). Burkhart Wolff and Christoph Lüth have provided tool-encapsulation techniques and advanced graphical user interface technology to bridge the gap between the embeddings and a Transformation Tool like TAS (paper available).

Specification Languages

The project Implementing Constructive Z uses Isabelle to support a software development method linking the Z specification language with intuitionistic and constructive program development methods.

Achim D. Brucker and Burkhart Wolff developed a conservative embedding of the Object Constraint Language (OCL) in Isabelle/HOL, called HOL-OCL. HOL-OCL allows one to reason over UML/OCL specifications and builds the basis for both further tool support (e.g. automatic test case generation) and the study of OCL language features (e.g. development of proof calculi and refinement notions for OCL).

Søren Heilmann has developed Isabelle/DC, an encoding of the real-time interval logic Duration Calculus. The encoding is in a sequent style and employs SVC as a decision procedure for real arithmetic.

Harald Hiss and Georg Lausen have been developing a formal model of XML in Isabelle/HOL (for a project called DEAXS, which abbreviates: Deductive Environment for the Analysis of XML-Specifications).

Robert Sandner and Olaf Müller have embedded FOCUS, a specification and verification methodology, into Isabelle and applied it to the verification of the production cell. Their paper has appeared in TACAS '97.

Stephan Merz has implemented Leslie Lamport's Temporal Logic of Actions (TLA) in Isabelle/HOL. The encoding is based on a simple axiomatic approach to represent modal logics in Isabelle, based on higher-order types and the parameter mechanism to keep track of different worlds, which may be more generally useful. Documentation and sources available.

David von Oheimb and Sebastian Nanz have designed and implemented Interacting State Machines, a formalism and toolkit for system modeling and verification, connected with the CASE tool AutoFocus.

Larry Paulson has mechanized the UNITY language using Isabelle/HOL. Commands are represented by relations over states. A program comprises a set of initial states and set of commands. The approach is definitional, with UNITY specification primitives defined in terms of program semantics and their properties proved. (Paper available.)

Ole Steen Rasmussen has embedded the relational hardware description language Ruby in ZF.

David Spelt and Susan Even have worked on the verification of semantic properties of object-oriented databases. A front-end tool has been implemented in ML to translate class specifications to Isabelle/HOL. Isabelle has been used to verify e.g. consistency (i.e., a method respects a number of static integrity constraints) and compensation (i.e., one method undoes the effects of another). Spelt has submitted his master's thesis to the University of Twente, Netherlands.

Kolyang, Thomas Santen and Burkhart Wolff have developed (as part of the former UniForM Project and ESPRESS Project) a conservative embedding of Z in HOL, called HOL-Z. Steffen Helke, Thomas Neustruppy and Thomas Santen also use HOL-Z in the project ESPRESS as part of a toolbox to support validating specifications and testing based on formal specifications. Starting with HOL-Z 2.0, HOL-Z allows one to use Z specification in LaTeX format (also used by the Z type checker Zeta as input.

Haykal Tej and Burkhart Wolff have developed (as part of the former UniForM-Project) a conservative embedding of CSP (Concurrent Sequential Processes by Hoare and Roscoe). It allows interactive verifications in process systems, protocols and distributed algorithms over infinite alphabets. (see HOL-CSP).

Verification

Sara Kalvala and Valeria de Paiva have implemented Linear Logic and have an ongoing project for developing a verification methodology using Linear Logic.

Olaf Müller has modelled the meta theory of I/O automata in Isabelle/HOLCF. (See his paper in TAPSOFT '97.) He formalizes the communication histories of the automata by lazy lists in domain theory. He is also a co-author of the paper "Possibly Infinite Sequences: a comparative case study" in TPHOLs '97 (Springer LNCS 1275, pages 89-104. This paper compares his approach with other formalizations of finite and infinite sequences. As a further application of I/O automata, a version of the alternating bit protocol with unbounded buffers has been verified using a combination of model checking and Isabelle. [Isabelle]

Wolfgang Naraschewski and Markus Wenzel have written a paper dealing with verification of object-oriented programs using extensible records in Isabelle/HOL.

Tobias Nipkow has verified an abstract lexical analyzer generator turning regular expressions into automata.

Tobias Nipkow and Leonor Prensa Nieto have implemented the Owicki/Gries method for the Hoare-style verification of concurrent programs in Isabelle/HOL.

Tobias Nipkow and Konrad Slind have done a protocol verification using I/O Automata in Isabelle/HOL. [Isabelle]

Tobias Nipkow, Cornelia Pusch, David von Oheimb, Gerwin Klein, Leonor Prensa Nieto, Martin Strecker, Norbert Schirmer, and Martin Wildmoser have formalized large parts of the programming language Java and the Java Virtual Machine. For details see the home pages of projects Bali and VerifiCard @ Munich. [Isabelle]

Claire Quigley wants Just-In-Time compilers to make optimizations not currently possible, and to perform existing optimizations more efficiently, by proving that certain properties hold of Java bytecode programs. She will carry out these proofs using Cornelia Pusch's Isabelle implementation of the operational semantics of Java and possibly a Hoare-like logic based on these semantics.

Larry Paulson has developed a new approach to the verification of cryptographic protocols. The operational semantics of all agents in the network (including an active intruder) is modelled using a series of inductive definitions. [Isabelle]

Starting from an operational semantics for Prolog, Cornelia Pusch presents some refinement steps towards the Warren Abstract Machine (WAM). The correctness and completeness proofs for each step have been elaborated with the theorem prover Isabelle using the logic HOL. Her paper, "Verification of compiler correctness for the WAM", appears in TPHOLs 1996 (Springer LNCS 1125).

Simon Thompson and Steve Hill have used Isabelle to reason about functional programs written in Miranda. Paper available.

Christian Urban has verified a nominal unification algorithm, which solves equations between terms involving binding operations. This algorithm solves such an equation (provided it is solvable at all) by calculating a most general unifier that makes the equated terms alpha-equivalent.

Norbert Völker is using Isabelle/HOL to verify function blocks in the area of control applications.

Tjark Weber has used separation logic to define three Hoare logics (corresponding to different notions of correctness) for the simple While language extended with commands for heap access and modification. Properties of separating conjunction and separating implication are mechanically verified and used to prove soundness and relative completeness of all three Hoare logics. The whole development, including a formal proof of the Frame Rule, is carried out in Isabelle/HOL. His paper, "Towards mechanized program verification with separation logic" has appeared in J. Marcinkowski and A. Tarlecki (Eds.): CSL 2004. Springer LNCS 3210.

Gerwin Klein and Tobias Nipkow have verified a Java-Like Language (Jinja), Virtual Machine and Compiler. The formalization includes a big and a small step operational semantics for Jinja and a proof of their equivalence; a type system and a definite initialization 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. dataflow analyzer for the JVM; a correctness proof of the bytecode verifiers w.r.t. the type system; a compiler and a proof that it preserves semantics and well-typedness.

David Cock, Kai Engelhardt, Kevin Elphinstone, Jeremy Dawson, Gerwin Klein, Rafal Kolanski, Jia Meng, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood in the L4.verified project of NICTA are verifying the functional correctness of the seL4 microkernel in Isabelle/HOL. This includes a Hoare Logic proof on the C/assembler implementation of seL4.