**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.**

**Computational content of true mathematical theorems.**

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 where

**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
-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.