Research Interests Programming Languages, Logic and Type Theory, Logical Frameworks, Automated Deduction, Trustworthy Computing (see also Publications, Students & Co-authors) Projects Logosphere A Formal Digital Library Triple Type Refinement in Programming Languages ConCert Language Technology for Trustless Software Dissemination Twelf Logical and Meta-Logical Frameworks SeLF Distributed System Security via Logical Frameworks Manifest Security Logics and Languages for Manifestly Secure Systems Prospero Integrating Types and Specifications
Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. Isabelle is developed at University of Cambridge (Larry Paulson) and Technische Universität München (Tobias Nipkow). See the Isabelle overview for a brief introduction. Now available: Isabelle2008 Some notable improvements: * HOL: significant speedup of Metis prover; proper support for multithreading. * HOL: new version of primrec command supporting type-inference and local theory targets. * HOL: improved support for termination proofs of recursive function definitions. * New local theory targets for class instantiation and overloading. * Support for named dynamic lists of theorems.
HOL4 is the latest version of the HOL interactive proof assistant for higher order logic: a programming environment in which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems (users may have to prove the hard theorems themselves!) An oracle mechanism gives access to external programs such as SAT and BDD engines. HOL 4 is particularly suitable as a platform for implementing combinations of deduction, execution and property checking. several widely used versions of the HOL system: 1. HOL88 from Cambridge; 2. HOL90 from Calgary and Bell Labs; 3. HOL98 from Cambridge, Glasgow and Utah. HOL 4 is the successor to these. Its development was partly supported by the PROSPER project. HOL 4 is based on HOL98 and incorporates ideas and tools from HOL Light. The ProofPower system is another implementation of HOL.