Type systems for computer languagesIn [Raf99a] and [Raf98b] I study 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 [Raf98b] I use an incomplete algorithm which always terminates and never backtrack. Then you get clear error messages and you can always add enough type information in your program to have it type-checked.
- In [Raf99a] I describe 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.
Extraction of programs from proofUsing Curry-Howard isomorphism, one can extract programs from proofs. However, for a given program is not not always easy or even possible to get a proof to extract it from. In [Raf03b] and [Raf02b], I introduce system ST; a complete system for purely functional programming (the pure lambda-calculus): any program can be extracted from a proof. Frédéric Ruyer's phd, which I am supervising, will explore the practical application of system ST.
Another related topic is the algorithmic content of classical proofs (proof using the law of excluded middle). It is clear now that classical logic corresponds to control operators like Felleisen Call-CC. Nevertheless, classical proofs do not give a real program (for instance a proof of the existence of an uncomputable object such as the minimum element in a set of natural numbers). Moreover, even when a classical proof gives a algorithm, one do not always understand how it works. In [Raf0c], I show how we can extract from a proof of "for all x there exists y s.t. S(x,y)" an algorithm computing y from x if S is decidable. I also explain how this program works: in short, this is an interaction between the proof of the given statement and the decidability proof of S. This interaction testes a sequence of possible value for y and always stops with a correct result.
Algorithmic contents of mathematical proofOne can also study the relation between proofs and programs in the other direction : what program corresponds to a given proof in mathematics. Or better : what are the properties shared by all the proofs of a given theorem.
In [Raf98a], we give a generalization of Krivine's theorem about storage operators to all types (not only for-all positive types). Here we give a property of all programs extracted from the proof of a theorem of the shape (D* -> not not D) where D* is the Godel translation of the formula D.
In [Raf98c], we show 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, we show that there exists one proof which do not change the term. This seems impossible for the completeness theorem of classical logic (treated by Krivine) of for the full intuitionnistic logic (with disjunction or existential). This gives a concrete argument to say that a semantic is trivial: it corresponds to programs doing some trivial computing.
Implementation of a proof assistantSince the end of my phd, I have been working on the PhoX proof assistant. One of its principle 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 with first to fifth year students in math and fourth year students in computer sciences (to prove programs). We worker to make PhoX easier and faster to learn for student. These experiments are related in [Raf02a] and [Raf01c].
GeometryI also started to work on algebraic geometry.
In [Raf01b], with Frédéric Mangolte, we solved a problem he needed to end the proof of one of its theorem: to find a necessary condition for the existence of an hyperplan tangent to n convex set of R^n.
Web site I am in charge
Last update: Friday 9 June 2006