Christophe Raffalli's home page

Research interests

Geometry

I also started to work on algebraic geometry.

In [Raf22], 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 $ℝ^{n}$

I also programmed GlSurf, a software to triangulate, visualized and animate implicit surfaces. This work (using a new kind of "marching cube" algorithm) is related in [Raf03a].

I am currently extending this work to an exact algorithm for solving real algebraic system in any dimension, provided the system is smooth (without critical points). The algorithm is implemented an works in already in some non trivial case. The paper [Raf23] gives a proof for the codimension 1 and a conjecture for the general case.

My main research topics are application of proof theory. It can be divided in four subtopics:

Type systems for computer languages

In [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 proof

Using 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 [Raf02c], I show how we can extract from a proof of " $\forall x, \exists y, 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 proof

One 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^{*} \to \neg \neg 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 assistant

Since 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].