Université de Paris 7

The team is working on the proofs-as-programs paradigm from the viewpoint of programming as well as from the viewpoint of mathematics. We are also working on the development of proof assitant systems.

The Af2 proof assistant system.

The Af2 proof assistant is a tool for the interactive development of proofs in second or higher order logic, designed and implemented by Christophe Raffalli. It could be used to develop formal mathematics and optionally to extract correct programs from proofs.

The system is designed to make easier the interactive development of formal proofs:

- The basic tactics give a direct access to natural deduction.

- Equational reasoning (automatic or using a "rewrite" tactic) is provided.

- The system has an automatic tactic to solve easy parts of the proof. This tactic is based on a higher-order semi-unification algorithm and the blind iteration of the basic tactics. This is why it can be understood by the user.

- The basic tactics can be extended to provide specific introduction and elimination rules for a given connective. This allows to hide the fact that object may have a complex definition by using directly the natural derived rules.

- The left rules of the sequent calculus may also be used and are also extensible.

- These new rules may be used by the automatic tactics, which can therefore be programmed by the user in an intuitive way to be as efficient as possible when dealing with newly introduces notions.

- A module system allows you to reuse previous proofs.

- You can easily extract a LaTeX paper from your proofs (the English text of the paper is not automatically generated, only formulas are).

A first version of the software is now available by ftp. Some changes in the system are planed to facilitate proof constructions, but the main remaining work is the development of a large and coherent library of basic mathematical results. We will then be able to really evaluate the system on a large scale.

Refinements of the proofs-as-programs paradigm.

In his forthcoming PhD thesis, Philippe Curmin developed marking algorithms for proofs in first and second order logic. They allow to eliminate redondant code in the extracted programs, and also to optimize the intermediate computations. The correctness of the generated programs is proved via a notion of realazibility.

He also proposed a system of derivation of recursive equations from proofs, and proved the corresponding correctness result.

Proofs as imperative programs.

An important subset of imperative instructions was interpreted in classical second order predicate calculus by J.L. Krivine (assignment, input, for and while loops, control instructions, subroutines, ...). Verification of typing in system F is done at compile-time. Under weak head reduction, the lambda-term will exactly simulate the run of the imperative source. This translation could give birth to a methodology for optimization and proof of imperative programs by extending the type system to predicate calculus.

Programs extracted from of mathematical theorems

J.L. Krivine has found a formal proof of the completeness theorem for predicate calculus and shown that this theorem is provable in intuitionistic logic. Quite surprisingly, any lambda-term associated with such a proof behaves like an interactive debugger with the usual security mechanism for system calls [Kri96b]. He is now working on formal proofs of the Gödel second incompleteness theorem.

J.L. Krivine gives in [Kri97] a set of logical rules for deriving a proof in Zermelo-Fraenkel set theory. They allow to extract a program (written in $\lambda$-calculus extended with the usual control operator Call/cc) from any classical proof in this theory. Normalization is no longer true, but the $\lambda$-terms obtained in this way are shown to be solvable.

Papers.

[Cur97] Ph. Curmin, PhD Thesis, in preparation.

[Kri96a] J.L. Krivine. About classical logic and imperative programming. Ann. of Math. and Art. Intell. 16 (1996) p. 405-414.

[Kri96b] J.L. Krivine. Une preuve formelle et intuitionniste du théorème de complétude de la logique classique. Bull. Symb. Logic., Vol. 2, 4 (Déc 1996), p. 405-421.

[Kri97] J.L. Krivine. Realizability in Zermelo-Fraenkel set theory. In preparation.