Communications at conferences

A constructive proof of the axiom of dependent choice, compatible with classical logic (pdf) [LICS, June 2012]
An intuitionistic logic that proves Markov's principle (pdf) [LICS, June 2010]
An approach to call-by-name delimited continuations (pdf) [POPL, January 2008]

Other talks

Talk on the Calculus of Inductive Constructions in sequent calculus form (pdf) [July 2010]
Synthetic talk on the Calculus of Inductive Constructions (ps, pdf) [September 2009]
Introductory talk on call-by-name delimited continuations (pdf, advi) [July 2007]
Talk on the dualité of computation (pdf) [PRELUDE, January 2008]
Talk on the duality of computation (pdf, advi) [HOR '06]
Talk on games, sequent calculus and abstract machines (ps) [APPSEM '01]
Introductory talk on the computational content of completeness and reducibility proofs (pdf) [September 2014]
Introductory talk on cubical type theory with definitional univalence (pdf) [LHC '19]