2021 
“On the logical structure of choice and bar induction principles”,
in collaboration with Nuria Brede,
to appear in the proceedings of LICS '21 (illustrated summary)
(erratum,
pdf including erratum).

2020 
“A calculus of expandable stores”,
in collaboration with Étienne Miquey,
proceedings of LICS '20
© IEEE
(bibtex).

2018 
“Realizability Interpretation and Normalization of Typed CallbyNeed lambdacalculus with Control”,
in collaboration with Étienne Miquey,
proceedings of FoSSaCS '18
(bibtex).

2016  
2014 
“A dependentlytyped construction of
semisimplicial types”,
Mathematical Structures in Computer Science, 2015
(erratum)
(bibtex)
(the formalisation in Coq).

2012 
“A constructive proof of the axiom of dependent choice, compatible with classical logic”,
proceedings of LICS '12
© IEEE
(bibtex)
(erratum,
pdf including erratum)
(talk at LICS '12)
(the proof in Coq).
“Classical callbyneed sequent calculi: The unity of semantic artifacts”,
in collaboration with Zena Ariola, Paul Downen, Keiko Nakata and Alexis Saurin,
proceedings of FLOPS '12
© SpringerVerlag
(bibtex).

2011 
“Pure Type Systems conversion is always typable”,
in collaboration with Vincent Siles,
appeared in the Journal of Functional Programming, 2011
(bibtex).
“Classical CallbyNeed and Duality”,
in collaboration with Zena Ariola and Alexis Saurin,
proceedings of TLCA '11
(bibtex).

2010 
“An intuitionistic logic that proves Markov's principle”,
proceedings of LICS '10
© IEEE
(typos)
(bibtex entry)
(talk at LICS '10).
“Equality is typable in SemiFull Pure Type Systems”,
in collaboration with Vincent Siles,
proceedings of LICS '10
© IEEE
(bibtex).
“Kripke models for Classical Logic”,
in collaboration with Danko Ilik and Gyesik Lee,
appeared in the Special Issue on “Classical Logic and Computation”,
Annals of Pure and Applied Logic, 2010
(bibtex).
“λcalculus and Λcalculus: a Capital Difference”,
in collaboration with Alexis Saurin, manuscript, 2010.

2009 
“An operational account of callbyvalue minimal and classical lambdacalculus in "natural deduction" form”,
in collaboration with Stéphane Zimmermann,
Proceedings of TLCA '09, LNCS 5608
© SpringerVerlag
(errata included)
(bibtex).
“Forcingbased cutelimination for Gentzenstyle intuitionistic sequent calculus”,
in collaboration with Gyesik Lee, WOLLIC '09
(bibtex).

2008 
“A new elimination rule for the Calculus of Inductive Constructions”,
in collaboration with Bruno Barras, Pierre Corbineau, Benjamin
Grégoire and Jorge Luis Sacchini,
TYPES '08, selected papers, LNCS 5497
(bibtex).
“An approach to callbyname delimited continuations”,
in collaboration with Silvia Ghilezan, Proceedings of POPL '08
(© ACM  posted here by permission of ACM for your personal use  not for redistribution)
(errata)
(bibtex)
(talk at POPL '08).
“Control Reduction Theories: the Benefit of Structural Substitution”,
in collaboration with Zena Ariola, Journal of Functional Programming, 2008
(bibtex).

2007 
“A TypeTheoretic Foundation of Delimited Continuations”,
with Zena Ariola et Amr Sabry,
HigherOrder and Symbolic Computation, 2007 ©
SpringerVerlag
(bibtex).
This paper is a full and improved version of “A TypeTheoretic Foundation of Continuations and Prompts”. 
2005 
“On the Degeneracy of SigmaTypes in Presence of
Computational Classical Logic”,
Proceedings of TLCA '05, LNCS 3461
(erratum)
(bibtex)
© SpringerVerlag
(the typed degeneracy proof in
Coq's old syntax).

2004 
“A TypeTheoretic Foundation of Continuations and Prompts”,
Proceedings of ICFP '04 © by the
Association for Computing Machinery,
Inc (erratum) (bibtex).

2003 
“Minimal classical logic and control operators”,
with Zena Ariola, Proceedings of ICALP '03, LNCS 2719 ©
SpringerVerlag
(erratum)
(bibtex)
(talk in Active dvi format or pdf). A journal version with Amr Sabry
entitled "A ProofTheoretic Foundation of Abortive Continuations"
appeared in the HigherOrder and Symbolic Computation journal.

2001 
“Explicit Substitutions and Reducibility”,
Journal of Logic and Computation, Vol
11(3), pp 429449, 2001 ©
Oxford University Press (the weakening lemma proof in here is wrong... more about it)
(bibtex).

2000 
“The duality of computation”,
with PierreLouis Curien,
Proceedings of ICFP '00 ©
ACM (get also the errata or
ps version that includes the errata,
pdf)
(bibtex).
Later talk to WoLP '04 in advi
(install Active dvi) or ps. The notes
corresponding to the invited talk at HOR '06
(bibtex).

1998 
“Computing with Abstract Böhm Trees”, with
PierreLouis Curien, Proceedings of FLOPS'98
(bibtex).

1997 
“Games and weakhead reduction for Classical PCF”,
Proceedings of TLCA'97 , LNCS 1210
(bibtex).

1996 
“Game semantics and abstract machines”,
with Vincent Danos and
Laurent Regnier, Proceedings of LICS'96
(bibtex).
“Une caractérisation des stratégies indépendantes
de l'histoire à partir des stratégies innocentes”, manuscript, 1996.

1995 
“Notes sur les lambdasigmacalculs”,
manuscript, 1995.

1994 
“A lambdacalculus structure isomorphic to sequent calculus
structure”, Proceedings of CSL'94
(bibtex).
“A lambdacalculus structure isomorphic to sequent calculus structure”, extended version for full classical predicate calculus, draft, 1994 .
“Atranslation and looping combinators in Pure Type
Systems”,
with Thierry Coquand, Journal of Functional
Programming , Volume 4, 1994
(bibtex).
“Some remarks on Novikoff's calculus”,
with Thierry Coquand, manuscript, 1994.

1993 
“Weak reduction in sequent calculus”,
manuscript, 1993, French version integrated in chapter 6 of my PhD thesis.
“Weak cutelimination and the
gametheoretic approach of provability”, manuscript (11 pages),
1993, French version integrated in chapter 6 of my PhD thesis.

1989 
“The twolist algorithm for the knapsack problem on a FPS T20”,
with Afonso Ferreira and Michel Cosnard, short communication,
Parallel Computing , Volume 9, North Holland, 1989
(no electronic version).

Hab. 
“C'est maintenant qu'on calcule: au
cœur de la dualité”, habilitation thesis, 2005.
Cf specific page.

PhD 
“Séquents qu'on calcule: de
l'interprétation du calcul des séquents comme calcul de lambdatermes
et comme calcul de stratégies gagnantes”, PhD thesis, 1995
(errata)
(bibtex).

Mast. 
“Formalisation du théorème de SchröderBernstein
dans le calcul des constructions”,
mémoire de DEA, 1988.

2017 
“Coq, assistant de preuve”,
with Sandrine Blazy and Pierre Castéran, Techniques de l'ingénieur, 2017
