I was until recently a phd student at Pareo (a very united team) under the direction of Frederic Blanqui and Claude Kirchner, on the subject: Termination of Higher Order Rewrite Rules. I now am a PostDoc at the Proval INRIA team, working on improving the alt-ergo automatic theorem prover.
This is my homepage.
My contact adress is (\ x y z t → email@example.com)cody roux lri fr. Beta-normalise for real adress.
I am defending my thesis at 10:30AM on the 14th at Loria, room C005
The manuscript can be found here.
I have taught an introductory algorithmics class on the Ocaml language.
One can find an excellent online source book at http://caml.inria.fr/pub/docs/oreilly-book/html/index.html, also available as a pdf.
I have many interests, most of them concerning the foundations of computer science, more specifically type theory, and its logical foundations. My current research concerns systems of the Barendregt cube, namely the simply typed lambda calculus, system F, and the Calculus of Constructions, to which we add constructors and functions defined by (higher order) rewrite rules. The termination of these systems is difficult to prove in general (though this has been done for an extention of the calculus of constructions using recursors, the Calculus of Inductive Constructions), and I am studying a technique that uses size annotations to prove termination of the general system.
It is of interest that these techniques seem to be at the center of much activity in the fields of theorem proving and proofs of programs. We can cite in particular the techniques of semantic labelling (recently generalised to the higher order by Makoto Hamana), which seem to very closely correspond to the notion of size annotation, which suggests a number of possible generalizations of the notion of size annotation. Some of the results from this observation have been published (see list of publications).
Currently I am implementing a termination checker for the language Dedukti. The point of interest is that one can use the pre-existing dependent types to naturally add, in an “explicit” way, the constructions needed to check termination.
In the process I have noticed that the technique of size-based termination can easily accommodate the termination technique known as the size-change principle as conjectured in the PhD work of David Wahlstedt. This is work in progress.
I have also noticed that it is possible to express a form of the dependency pair technique (see e.g. Arts & Giesl) using these type-based termination techniques. It had already been observed that the size-change principle could readily be unified with the dependency pair method, so it is not entirely surprising that we may “bridge the gap” and extend this to the higher order situation. The criterion rests on a kind of refinement type already studied for ML style programs; however this “typed-based dependency pair” approach seems to be quite novel in the extension of these termination techniques to higher order rewriting.
Finally I am interested by all things mathematic, with particular emphasis on algebra. My holy grail would be to understand the statement and proofs of the Weil conjectures.
A small paper on coercions in type theory, which gives the main results of my master's thesis and published in the 2008 JFLA conference (french).
A paper which details the connections between semantic labelling and size based termination, by Frederic Blanqui and myself (published in CSL '09).
We use refinement types to express an approximation of the dependency graph as used in the dependency pair technique, and then apply usual computability techniques to show that if the graph is without cycles, then the system is strongly normalizing. Submitted to LPAR '10.
Fooling around in Coq: It is easy to define a version of Normalisation by Evaluation for the simply typed lambda calculus, using the (quite efficient) evaluation of Coq (as a programming language). This is quite elegant, in that it adopts the point of view of Coq as a universe in which functions exist (and are defined). Mathieu Boesflug rightly notes that there is a mistake in my development, namely that fresh names can not be given by simple induction on the types. I will get around to correcting this as soon as possible. Also note that very similar work has been carried out by Francois Garillot.
It is well known that there is no simple Set-theoretic model of Girard and Reynold's System F, as the impredicativity of System F would make set-theory inconsistent. However there is a simple Type-theoretic model of system-F in the Calculus of Inductive Constructions with Universes, which is unsurprising, considering that system-F is a subsystem of that system. This construction can be likened to the construction of a model of Zermelo's set-theory Z whithin Zermelo-Fraenkel set-theory ZF. We give this construction in Coq.
Here is the proof of correctness of the type system of a very simple language with pattern matching with respect to its operational semantics. Note that the evaluator for that language can be simply written in Coq, as it is not Turing Complete. Observe also that the proof is quite short and (somewhat) intuitive, and that there is no need to have any special treatment of bound variables, as the evaluator and typing judgement agree on the treatment of these variables, namely that a variable “hides” a previously declared variable of the same name. This introduces disequality judgements in the (object level) typing derivations which are nevertheless quite easy to deal with. A somewhat similar treatment, which relates Hoare-style semantics and operational semantics can be found here in a very beautiful development by Yves Bertot.
Size annotations by Frederic Blanqui
Type Checking in the CACSA