Articles et Exposés
Thèse de doctorat
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.
Revues
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.
Conférences
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.
Rapports et notes
Une introduction à la théorie de la démonstration
À l'occasion du séminaire thésard du LIX j'ai essayé d'expliquer un peu ce qu'est la théorie de la démonstration et ce que je fais dans ma thèse, pour l'instant.
Logique linéaire et algèbres de processus
J'ai réalisé mon stage de 2ème année de Master avec Dale Miller. Dans mon rapport je mets en évidence une connection forte entre la logique linéaire et de nombreux calculs concurrents. J'ai présenté ce travail à Geocal'06 (hiver 2006) (PDF en anglais).
Mode interactif pour CAL
Été 2004, j'ai travaillé à Kyôto sur l'ajout d'un mode de développement interactif de preuves dans CAL, le logical framework local: rapport.
Élimination de code inutile dans le π-calcul
Exposé dans le cadre du cours de DEA "Mobilité" à l'ENS Lyon. Rapport, présentation, sources.
Détecteurs de pannes et systèmes asynchrones distribués
Sur la difficulté théorique de faire des choses ensemble en réseau quand les pannes sont possibles, spécifiquement l'élection de leader. Travail effectué au LaRIA à Amiens pour mon stage de MIM1 (Licence, 2003). Rapport, présentation, sources.
Construction explicite d'une solution approchée au problème de rétropropagation
Une courte réponse théorique sur les réseaux de neurones : pourquoi met-on toujours trois couches ?
Transcription graphème-phonème
Pour mon TIPE, j'ai étudié une technique possible de transcription (traduction d'une écriture en sa prononciation). Le compte-rendu ou une note avec des compléments, et les sources C++.