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.

People using Isabelle at Cambridge

• Wenda Li
• Peter Sewell
• Nik Sultana

Former team members

• Giampaolo Bella
• Michael Compton
• Jean Martina
• Jia Meng
• Susmit Sarkar
• Rok Strniša
• Christian Urban
• John Wickerson
• Yichi Zhang

Isabelle-Related Research Grants at Cambridge

• Automatic Proof Procedures for Polynomials and Special Functions (ended 2014). Primarily about MetiTarski, this project has also stimulated work into real algebraic geometry and on proving bounding properties of certain special functions.
• Automated Formal Proofs for Polynomial and Transcendental Problems (ended 2009)
• Automation for Interactive Proof (ended 2007)
  Methods for linking interactive and automatic proof tools. This project produced Sledgehammer!
• Compositional Reasoning about Concurrent Programs (ended 2003)
  The UNITY formalism and theories of composition.
• Verifying E-Commerce Protocols (ended 2003)
  The verification of major security protocols, such as SET and the certified e-mail protocol.

Isabelle archives (mailing list, papers, past releases) are available!

Thanks to the EPSRC and ESPRIT for financial support.

Last modified Tuesday, 22 September, 2015