Towards a broad spectrum proof certificate

Encadrement :

Description du sujet

Various computer systems produce proofs of logical statements. Many of these systems are also capable of outputing certain evidence or ``proof certificates'' that they have successfully proved a theorem. Unfortunately, most of the artifacts that are produced are of limited use. For example, many interactive theorem provers use ``proof scripts'' as evidence that they have been steered to a final proof. Such scripts can be replayed but they seldom have meaning within any other computation system and their validity many not even survive a change in the prover's version number.

This state-of-the-art is unfortunate for at least two reasons. First, there is a great deal of foundational work available regarding the structuring of proofs and about their ``universal'' character. Second, there is growing evidence that there are setting where proofs could be used to help guarantee the correctness and security of computer systems. An example of this is the so-called proof-carrying code paradigm (Wikipedia, U. Princeton, UC Berkeley).

Recent research within the Parsifal team and elsewhere has shown that a wide range of proof systems studied by proof theorists, theorem proving reseachers, and those building model checkers can be represented within one, high-level and declarative system. The evidence is that a rather simple description of, say, classical logic inference rules can be given to which one can specific different parameters (such as ``polarizations'' and ``permeabilities'') and then automatically account for a range of proof systems for classical logic. Proof systems that are know to be handled by such a scheme include sequent calculus, natural deduction, tableaux, free deduction, Hilbert-style proofs, and tabled deduction (in the setting, say, of model checking). The paper [NM09] provides the theoretical background for most of these claims using a linear logic setting for specification while the technical report [SH09] does the same using an intuitionistic setting. The paper [MN07] provides a similar background for describing tables in model checkers as proofs.

The goal of this internship is to take that theoretical background and propose ways to develop it into an architecture for a broad-spectrum of proof systems. This work can be developed into at least two directions: only one of these directions need to be pursued.

1. The specification of proof certificates described above is declarative and, as a result, a rich calculus of computing on proof certificates should be possible. For example, it should be possible to locally transform one kind of proof format to another, to extract information from a proof, or to interact with proofs (in the sense of a game), all in a number of formats. A theoretical framework that allows for a rich collection of operations on proofs is to be designed.
2. Design a concrete proposal for proof formats that can be tested and prototyped. A high-level language implementation of the proposal (in, say, an ML dialect or λProlog) should be considered and its feasibility with a number of proof formats and proof producers should be tested. Many aspects of computing with proofs can easily involve exponential time and/or space: thus, understanding what is feasible with a broad-based proof certificates need to better understood. Several research-oriented questions should be tied to such prototype considerations.

It should be possible to continue this work as a PhD student.

Bibliography

1. [NM09] Vivek Nigam and Dale Miller, A framework for proof systems. Accepted to the Journal of Automated Reasoning. Draft dated 22 Dec 2009: (pdf)

2. [LM09] Focusing and Polarization in Linear, Intuitionistic, and Classical Logic by Chuck Liang and Dale Miller. Theoretical Computer Science, 410(46), pp. 4747-4768 (2009) (doi, pdf). This paper is an extended version of a CSL07 paper.

3. [SH09] Anders Starcke Henriksen. Using LJF as a Framework for Proof Systems. Technical Report, University of Copenhagen, 2009.
   [http ]

4. [MN07] Incorporating tables into proofs by Dale Miller and Vivek Nigam. CSL'07: Computer Science Logic, J. Duparc and T. A. Henzinger, editors, LNCS 4646, pages 466-480. Springer-Verlag. (pdf).