Papers and Talks
PhD thesis
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.
Journals
Least and greatest fixed points in linear logic
Extended and revised version of the earlier papers, including a new, direct proof of normalization. Accepted in Sept 2010 for publication in the ACM Transactions on Computational Logic, available on arxiv/corr.
Conferences
Liquidsoap: a High-Level Programming Language for Multimedia Streaming
Design principles of Liquidsoap, including the two main novelties of version 1.0, namely heterogeneous stream contents and clocks. Joint work with Romain Beauxis and Samuel Mimram, accepted at SOFSEM'11.
A meta-programming approach to realizing dependently typed logic programming
Redundancy elimination in dependently typed lambda calculus (LF) and its application to implementing efficient proof search for LF by translating to λProlog. Joint work with Zach Snow and Gopalan Nadathur, accepted at PPDP'10. A companion workshop paper, focusing more on the LF results, has been presented at PSTT'10.
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. This paper (PDF) is joint work with Zach Snow and Dale Miller, and has been accepted at IJCAR'10. This has been implemented in Tac.
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. Also see some code using the notion of multisimulation to produce ML functions as proofs of inclusions.
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!
Workshops
An overview of focusing for least and greatest fixed points in intuitionistic logic
Bringing that work outside of the linear setting, with some new observations, presented at PSTT'10.
Notes and reports
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.