Cody Roux

About Me

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 → x.y@z.t)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.

Teaching

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.

Research Interests

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.

Stuff By Me

Types, logique et coercions implicites

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

On the relation between sized-types based termination and semantic labelling

A paper which details the connections between semantic labelling and size based termination, by Frederic Blanqui and myself (published in CSL '09).

Refinement types as higher order dependency pairs

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.

Simply Typed Normalisation by Evaluation

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.

Simple model of System F

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.

Correctness of Micro Tom

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.

Stuff by others

Concerning My PhD

Size annotations

Size annotations by Frederic Blanqui
Type Checking in the CACSA

By Blanqui and Colin Riba using presburger arithmetic annotations
Combining Typing and Size Constraints

By Andreas Abel
Typed Based Termination of Generic Programms

By Gilles Barthe and Benjamin Gregoire
Typed Based Termination in the CIC

Hongwei Xi with the very interesting ATS language.

Inference of annotations

Semantic labelling

Abstract interpretation/Domain theory

Everything on Patrick Cousot's page

Coquand/Spiwack

On Other Stuff

Thierry Coquand

Benjamin Werner

Alexandre Miquel

Gilles Dowek

Coq

Guiseppe Longo

Jean-Yves Girard

Etc.

codyroux.txt · Last modified: 2011/06/07 18:18 by rouxcody
Back to top
chimeric.de = chi`s home Creative Commons License Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0