Isabelle at Cambridge

Isabelle at Cambridge

Isabelle is a generic theorem proving environment developed at Cambridge (Larry Paulson) and TU Munich (Tobias Nipkow). This is the local page of the Cambridge Isabelle group, which is part of the Automated Reasoning Group.

Use the sledgehammer!!!

The Team

People using Isabelle at Cambridge

• Jean Martina
• Tom Ridge
• Susmit Sarkar
• Peter Sewell
• Rok Strniša
• Nikolai Sultana
• Dave Turner
• Yichi Zhang

Recently departed team members

• Giampaolo Bella
• Michael Compton
• Jia Meng

Isabelle-Related Projects at Cambridge

• Automation for Interactive Proof (finished 2007)
  This project concerns methods for linking interactive and automatic proof tools.
• Compositional Reasoning about Concurrent Programs (finished 2003)
  This project concerns the UNITY formalism and theories of composition.
• Verifying E-Commerce Protocols (finished 2003)
  This project concerns the verification of major security protocols, such as SET and the certified e-mail protocol.

Isabelle Resources

• Instructions for running Isabelle 2002 under Windows 2000 (thanks to Norbert Völker)
• archives (mailing list, papers, past releases)

Alternative User Interfaces

• Isamode is an XEmacs interface that provides extensive menus and shortcuts for common Isabelle tactics. It is by David Aspinall, who is one of the main developers of the default interface (Proof General).
• From the University of Bremen: Burkhart Wolff's Contribution Page contains an experimental, easy to modify user interface for Isabelle. There is a collection of Isabelle theories (e.g. State-Monads).

Thanks to the EPSRC and ESPRIT for financial support.

Last modified Tuesday, 21 April, 2009