Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems

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.

Research activities
  Formalisation of (Specification and Programming) Languages in Proof Assistants

Participants
VOISIN Frédéric
WOLFF Burkhart
LONGUET Delphine


More information : http://paral-itp.lri.fr/