Papers and Talks
Submitted
Least and greatest fixed points in linear logic
Extended and revised version of the earlier papers, including a new, direct proof of normalization. Submitted to ToCL in October 2009, available on arxiv/corr.
Published
On the proof theory of regular fixed points
Model-checking and proof-theory, finite automata and regular formulas, multi-simulation and simultaneous induction, cyclic proofs. Accepted at TABLEAUX'09, February 2009. This paper (PDF) corresponds to Chapter 5 of my PhD.
On the Expressivity of Minimal Generic Quantification
On the interaction of minimal generic quantification and fixed points. Published in the proceedings of LFMTP 2008, extended version at HAL, slides here. April 2008.
De la webradio lambda à la λ-webradio
Joint work with Samuel Mimram, published in the proceedings of JFLA 2008. Get the PDF of the paper and slides, and go try the system, it's free software.
Least and greatest fixed points in linear logic
Focusing for logics supporting (co)induction. Joint work with Dale Miller, published in the proceedings of LPAR 2007. Get the paper (PDF), and the extended version (PDF). See also the slides of the presentation at LPAR, or a former and longer talk at PPS.
The Bedwyr system for model checking over syntactic expressions
Joint work with Andrew Gacek, Dale Miller, Gopalan Nadathur and Alwen Tiu. Published in the proceedings of CADE'07. Get the paper, or the slides of the presentations I gave at CADE'07, at the ICMS in May 2007 (Workshop on Abstraction, Substitution and Naming in CS), or at INRIA Rocquencourt (long talk in Sept 2007, in french and with new details). And of course, get Bedwyr!
Notes and reports
A linear approach to the proof-theory of least and greatest fixed points
Thèse de doctorat de l'école Polytechnique, 9 décembre 2008.
Focused Inductive Theorem Proving
About the application of focusing proof system for fixed point logics to (co)inductive theorem proving in the intuitionistic logic μLJ (PDF). This has been implemented in our framework Tac.
Logique linéaire et algèbres de processus
My master's thesis on linear logic and process calculi is available in french. This work was presented at Geocal'06 (PDF in english).
Interactive proof development for CAL
Summer 2004, I worked in Kyôto at an interactive proof development mode in CAL, the local logical framework: report.
Useless code elimination for π-calculus
I mostly studied Naoki Kobayashi's paper on the subject. Sorry, everything is in french. Rapport, présentation, sources.
Failure detectors for asynchronous distributed systems
Many common problems are no more solvable in a realistic distributed computing model, that is when failures are possible and everything is asynchronous. Failure detectors were introduced as a mean to compare the problems anyway. After a review of a few common problems I focused on leader election. It was a work during summer 2003, at the LaRIA in Amiens. Report in english, presentation in french, sources.
