. . . . .
. . . . .
Interactive Proof Development for Everybody
Welcome to the Home Page
The purpose of the PIDE-Project is to create a Prover IDE framework that brings Interactive Theorem Proof Assistants truly to the rest of us. Our ultimate goal is an IDE that makes interactive theorem proving (ITP) amenable both to high-school education as well as power users in theorem proving, and that makes theorem provers as easy to install as, say, LibreOffice under Mac OS X, and as common to use as, say, a Computer Algebra System. Furthermore, we want to exploit the full potential of ITP Systems such as Isabelle, Coq or HOL as implementation basis for Formal Methods Tools.
High-Level Design Goals at a Glance
- Prover Independence ("Genericity")
in the tradition of Proof General that works for Isabelle, Coq, ..., but based on completely new technologies.
- Platform Independence
PIDE implementations should work uniformly on Linux, Mac OS X, Windows.
- Support for Asynchronous Proof Processing
We are living in a world with cheap multi-core processors nowadays. ITPs with their increasing demand of computer power will exploit this trend. For ITP-GUIs, this means new challenges for the representation of no longer linear proof documents and their processing.
- Extensibility for Domain-Specific Theorem Proving
Some ITP systems can be used to "implement" formal methods tools, in particular via shallow embeddings and reasonable mechanical support on top of them. PIDE will provide an plug-in infra-structure that allows for domain-specific viewing and editing components.
- There are some slides by Makarius Wenzel on general concepts behind PIDE from 2007 and 2008.
- Slides on designing the prover/interface communication for asynchronous proof processing can be found here. The paper also discusses the integration of provers with linear processing models.
- Holger Gast: Towards a Modular Extensible Isabelle Interface. Emerging Trends Track of TPHOLs 2009. PDF
- Makarius Wenzel: Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit]. In C. Sacerdoti Coen and D. Aspinall, editors, User Interfaces for Theorem Provers (UITP 2010), FLOC 2010 Satellite Workshop, Edinburgh, Scotland, July 2010. To appear in ENTCS. PDF
See Isabelle/jEdit as part of the official Isabelle release http://isabelle.in.tum.de/download.html
Some members of the PIDE-Taskforce are:
- Achim Brucker, SAP Research Karlsruhe, Germany, http://www.brucker.ch/.
- Holger Gast, Uni-Tübingen, Germany, http://www-pu.informatik.uni-tuebingen.de/users/gast/.
- Makarius Wenzel, Univ. Paris-Sud, LRI, France, http://www.lri.fr/~wenzel/.
- Burkhart Wolff, Univ. Paris-Sud, LRI, CNRS, France, http://www.lri.fr/~wolff/.