ANR Paral-ITP Project Home Page

Summary:

Interactive theorem proving is a technology of fundamental importance for mathematics and computer-science. It is based on expressive logical foundations and implemented in a highly trustable way. Applications include huge mathematical proofs and semi-automated verifications of complex software systems. Interactive development of larger and larger proofs increases the demand for computing power, which means explicit parallelism on current multicore hardware.

The architecture of contemporary interactive provers such as Coq, Isabelle or the HOL family goes back to the influential LCF system (from 1979), which has pioneered key principles like correctness by construction for primitive inferences and definitions, free programmability in userspace via ML, and toplevel command interaction. Both Coq and Isabelle have elaborated the prover architecture over the years, driven by the demands of sophisticated proof procedures, derived specification principles, large theory libraries etc. Despite this success, the operational model of interactive proof checking is largely limited by sequential ML evaluation and the sequential read-eval-print loop, as inherited from LCF.

The proposed project intends to overcome the sequential model both for Coq and Isabelle, to make the resources of multi-core hardware available for even larger proof developments. Beyond traditional processing of proof scripts as sequence of proof commands, and batchloading of theory modules, there is a large space of possibilities and challenges for pervasive parallelism. This affects many layers of each prover system: basic computational structures, inference kernel, tactical programming, proof command language, and interactive front-ends. Some of these aspects need to be addressed for Coq and Isabelle in slightly different ways, to accommodate different approaches in either system tradition. These substantial extensions of the operational aspects of interactive theorem proving shall retain the trustability of LCF-style proving at the very core.

Once that both Coq and Isabelle have been elevated to a parallel prover architecture, they shall be connected to a uniform document model that integrates parallel and asynchronous evaluation processes with notions of history and change management, over the rich structure of formal content. This can then serve as a basis for an editor document model in direct user interaction, and background library management with continuous proof checking, in the style of modern IDEs like Eclipse or Netbeans. Ultimately, both Coq and Isabelle will become more powerful and more accessible. The general document model and front-end technology will accommodate end-users and builders of add-on tools for either prover. Thus the achievements of decades of research into formal modelling and theorem proving will become more easily accessible for the construction of highly trustworthy software systems.

Project Partners:

LRI: Burkhart Wolff (coordinator),

Makarius Wenzel, Delphine Longuet,
Frédéric Voisin, Pierre Courtieu, Olivier Pons.

INRIA Rocquencourt:

Hugo Herbelin, Yann Régis-Gianas, Matthieu Sozeau, Damien Doligez

INRIA Saclay:

Bruno Barras, Germain Faure, Assia Mahboubi.

The Kick-off Meeting :