Paris 7 site: scientific report

Paris 7 team studies most of the aspects of the correspondance between proofs and programs. This work can be classified along the following lines:

- Computational interpretations of classical logic

- Computational content of true mathematical theorems

- Use of Curry-Howard correspondance to prove the correctness of imperative programs.

- Game semantics for classical linear logic

- Type systems for computer languages

- Development of the AF2 proof assistant

Computational interpretations of classical logic.

M. Parigot introduces in [10] a computional interpretation of classical logic, called $\lambda\mu$-calculus which has been widely studied. In [11], he gives two proofs of strong normalisation for second order typed $\lambda\mu$-calculus. The first one is an adaptation of the method of reducibility candidates introduced by J.Y. Girard for second order typed $\lambda$-calculus; the extension to the classical case requires in particular a simplification of the notion of reducibility candidate. The second one is a reduction to the intuitionistic case, using a kind of cps translation.

In [5], V. Danos, J.B. Joinet and H.D Schellinx, packed a comprehensive study of sequent calculi for classical logic, most notably LKT, LKQ and LKTQ, that one could embed in linear logic. In [6] V. Danos attaches a sound and intuitive continuation calculus to LKQ, yielding a `Curry-Howard' configuration. Plugging in a standard embedding of natural deduction in sequent calculus, one retrieves a Plotkin-like continuation passing style compilation of call-by-value lambda-calculus with control. In collaboration with a student, Charles Harris, he is now trying to set up a mixed call-by-value/call-by-name CPS compilation starting from LKTQ.

In a recent forthcoming work, C. Raffalli proposes a method to extract a program from a proof in mixed second order logic. It is clear now that classical logic corresponds to control operators like Felleisen Call-CC, but it is not clear how to get an exceptions mechanism similar to ML's one. C. Raffalli uses three level of logic in the system: classical, intuitionnistic and non-algorithmic, Combining the three levels, one can get exactly the program ones wants (like a search in a list using exceptions) from a simple equationnal specification which do not mention exceptions.

Computational content of true mathematical theorems.

J.L. krivine studied the correspondance between proofs and programs in the framework of second order classical logic and Zermelo-Frænkel Set Theory. This correspondance associates the notion of theorem to that of specification. But the problem of finding the specification associated to a given mathematical theorem is highly non trivial and is solved yet only in a few number of particular cases.

In the framework of second order classical logic, J.L. Krivine solved the problem in [7] for the completness theorem of predicate calculus. This theorem appears surpisingly as the specification of an interactive disassembler program, with a security mechanism against the handling mistakes of the programmer.

The most general framework to set up this kind of problem is clearly Set Theory. But one has first to realize axioms of this theory, in the framework of classical logic. The main difficulty comes from the extensionality axiom: J.L. Krivine shows in [9] how to overcome this difficulty, using a method directly inspired from the forcing method of P. Cohen (cf. [8]).

This framework being established, one can set up the problem of finding the spefication associated to any mathematical theorem. Partial result have been obtained for Cantor and Cantor-Bernstein theorems.

V. Danos and C. Aubouy, are pursuing another line of research: they study the proof-theory of projective and affine geometry in the hope of finding an extension of Curry-Howard correspondence in a real mathematical theory, as opposed to a purely logical one. Preliminary studies of the work of Matthias Baasz and Norbert Preining show that a relatively tractable cut-elimination theorem can be proved.

C. Raffalli studied the following question: what are the properties shared by all the proofs of a given theorem? In [12] he generalizes Krivine's theorem about storage operators to all types (not only for-all positive types), giving a property of all programs extracted from the proof of a theorem of the shape $D^* \rightarrow \neg\neg D$ where D^* is the Godel translation of the formula D. In [13], he shows that all the proofs of the completeness theorem for minimal logic translates an higher-order representation of simply typed lambda-terms to a Debruijn representation of a term with the same type. Moreover, there exists one proof which does not change the term. This seems impossible for the completeness theorem of classical logic (treated by J.L. Krivine) or for the full intuitionnistic logic (with disjunction or existential).

Use of Curry-Howard correspondance to prove the correctness of imperative programs.

The correspondance between proofs and programs (also called Curry-Howard correspondance) can be used to prove the correctness of programs. Relating the Hoare Logic to the systems of typed $\lambda$-calculus, J.L. Krivine obtained results for imperative programming languages such as C. The methodology is the following: one associates to a program a formula of classical second order logic (or set theory), built from the source of the program. This formula specifies the behaviour of the program, as it is written. One has then to prove that the original specification is a consequence of this formula. The paper containing these results is in preparation.

Game semantics for classical linear logic.

In [1], P. Baillot, V. Danos, T. Ehrhard and L. Regnier introduced the first games semantics for classical linear logic, with a new approach to the central topic of representing composition of strategies, which is consistent with the symmetries of linear logic. It was investigated further in [2] how that semantics could relate to static denotational semantics. A careful construction of a polarized version of relational semantics for linear logic gives a neat factorization theorem, which to my knowledge is the first of its kind, by which one sees that the lax functor that maps games to sets exactly relates the two semantics. Further refinements of those polarized relations, due to Paul-André Mellies, show strong links with Thomas Ehrhard's hypercoherence semantics.

As to bridging the gap with operational semantics, in [3], it is proved that interaction between definable strategies can be computed directly by simple environment machines, thus giving good founding to the intuitive claim that games semantics represents syntactical objects by their set of computation traces in all contexts.

V. Danos, is working now, in collaboration with Russel Harmer, on an extension of games semantics to model functional or imperative computations extended with a random instruction. So far, they proved that in their setting of probabilistic strategies, the coin strategy that returns true or false with equal chances, is universal, that is any probabilistic strategy can be factorized as a deterministic one composed with the coin.

Type systems for computer languages.

In [14] and [15], C. Raffalli studied how the system F-eta (an extension of Girard's system F), which is undecidable, can be used as a type system in a real programming language. There are two possible approaches. In [14] he uses an incomplete algorithm which always terminates and never backtrack. In this case one gets clear error messages and one can always add enough type information in the program to have it type-checked. In [15] he describes an optimized and efficient complete algorithm. This algorithm works very well (and fast) for small polymorphic programs. However, as the algorithm do backtrack, it is not clear how to get nice error messages and an interactive type-checker working like a debugger would be necessary to make this practical for larger programs.

Development of the AF2 proof assistant.

Since the end of his phd, C. Raffalli is developing the AF2 proof assistant [16], whose aim is to be as user friendly as possible and so to need a minimal learning time. The current version is quite functional and is used for teaching in Paris VII and in the University of Savoie. P. Roziere developed libraires and examples for this system.