Supervision
Kaustuv Chaudhuri, chargé de recherche, équipe Parsifal, Inria Saclay Île-de-France &
LIX/École Polytechnique
Contact: kaustuv.chaudhuri@inria.fr
Description
All current interactive proof-assistants have an interaction language consisting of a combination of a formal proof language to describe the proofs and a command language to give instructions to the proof-assistant. Unfortunately, there is no uniformity in these languages across different systems.
This internship will investigate alternative proof construction methods that avoid linguistic differences and limitations by avoiding proof languages entirely. Rather, proofs will be built by directly manipulating the structure of the theorems and lemmas using the mouse or touch screens and such natural user-interface actions as pointing, selecting, and dragging-and-dropping.
A useful analogy is the difference between interactive text-adventure games such as Zork or Adventure, where one uses language both to understand the current gameplay context through prompts and descriptions and to instruct an interpreter to perform the actions for the player, and interactive 3-D games where the player can simply obseve the gameplay context and can express their actions by manipulating the representations of objects using a range of input devices and metaphors.
Despite the additional freedom that direct manipulation techniques may provide, we still want all the guarantees of formal proofs. In other words, the user should not be allowed to make unsound manipulations, nor should the interactive system prevent the user from proving true theorems. This requires a fair bit of sophistication in the internal representation of formal proofs.
We use a deep inference calculus known as the calculus of structures which has many of the ingredients required for such representations. The crucial feature of deep inference systems is the ability to perform infrence steps inside a formula. We have built a prototype system called Profound that can build proofs in first-order linear logic by a simple interaction metaphor called linking, which results from dragging and dropping subformulas of a given theorem.
This internship is concerned with bridging the gap between the Profound system and current interactive theorem provers. Specifically, Profound will generate a proof object in a variant of deep inference, and this will then need to be translated into a formal proof document in an existing system. For the purposes of this internship, we will target the two systems Coq and Isabelle/HOL.
The ideal end-product of this internship will be a plugin to both systems that will launch Profound to build the proof, which will then be transformed into Coq and Isar proof scripts to be checked by the respective systems.
Candidate Profile and Background
The ideal internship candidate will be familiar with proof theory, automated theorem proving, and with programming in OCaml. Knowledge of HTML5, Javascript, or WebGL will be a big plus, but is not required.
For MPRI candidates, modules 2.1, 2.5, 2.7.1, and 2.7.2 are useful prerequisites, but only 2.1 is strictly required.
Continuing on to a Ph.D. is both possible and encouraged. Deep inference is full of interesting problems with direct application to interactive theorem proving and proof certificates.
Some Relevant Publications
The following publications give a background and indicate the kind of work performed in this research effort.
- K. Chaudhuri, Subformula Linking as an Interaction Method, Conference on Interactive Theorem Proving (ITP-04), France. LNCS 7998, pp. 386–401. July 2013.
- K. Chaudhuri, N. Guenot, and L. Straßburger. The Focused Calculus of Structures. Computer Science Logic (CSL-20), Bergen, Norway. LIPICS v.12, pp. 159–173. September 2011.
- Y. Bertot, The CtCoq system: Design and architecture. Formal Aspects of Computing, /11(3): 225–243. September 1999
- K. Chaudhuri, Compact Proof Certificates for Linear Logic Certified Programs and Proofs (CPP-02), Kyoto, Japan. LNCS 7679, pp. 208–233. December 2012.