Guillaume Gillard

 I have defended my PHD thesis on the 25th of June 2001. This page is dedicated to the researches I have done at INRIA Sophia Antipolis from 1997 to 2001. If you want to know more about my present activities have a look at my resume (in French) there.

  Mon Curriculum Vitae actualisé (Novembre 2002) est disponible en HTML (CV de Guillaume Gillard).

  I have prepared a PhD with Joelle Despeyroux within the Certilab research group. My research interests concern the encoding of binders of programming languages inside the coq system. Given a binder we use a first layer de Bruijn constructor and we derive a new function that we will use for encoding the real life binder. This new function (function as constructor) re-introduce the binded variable name (from λ.0 to λx.x) and we prove that its behavior in our Logical Framework is the same than the behavior of the binder in real life. With this kind of encoding we show that we can have the same induction schemes than those used on paper (alpha-equivalence is given for free).

Keywords:

Formal methods, specifications, proofs, Coq, calculi, programming languages, concurrent and object oriented language, alpha conversion and alpha equivalence.

 A resumed presentation (in French) of my research and teaching activities from 1997 to 2000 is available there (PostScript format).

 A presentation of my implementation, in the Coq system, of an concurrent object oriented calculus (syntax, reduction rules and typing) is available here (.dvi) -copyright-.This paper has been presented at the CADE-17 conference.

 A more detailed presentations of the method we used can be found in here (.dvi).This paper (draft, unpublished) only deals with the encoding of the syntax, we only mention the semantics rules as a future subject of studies.

 My PhD thesis: Formalization of concurrent and object languages up to alpha-conversion. Final version (25 June 2001) in French.

• The Coq code of the implementation of the conc-sigma-calculus is there. This encoding include the syntax of this calculus, its transition relation, a very simple typing system and the Subject Reduction Theorem.
• The coq code of my encoding of a typed monadic pi-calculus using the same method for formalizing binder is also available there . In this development, difficulties arise in formalizing the labelled transition relation. A detailed presentation of this work is given in my PHD.