Intuitionistic reverse mathematics of completeness theorem with respect to Tarski semantics (pdf for Thierry Coquand's birthday workshop, August 2022; pdf for Chocola meeting, November 2022)

On the common logical structure of choice and bar induction axioms (pdf with errata, Proof Theory Virtual Seminar, June 2021) (extended talk at the University of Verona, covering Teichmüller-Tukey lemma and Berger's update induction, March 2024)

Introductory talk on cubical type theory with definitional univalence (pdf, LHC, October 2019)

Talk on the computational content of Henkin's proof of Gödel's completeness theorem (pdf, IMJ, December 2018, includes the proof with side effects)

Talk on a proof with side effects of Gödel's completeness theorem (recorded video, HIM, July 2018)

Talk on the reverse mathematics of Gödel's completeness theorem (pdf, HIM, July 2018)

Introductory talk on the computational content of completeness and reducibility proofs (pdf, PPS, September 2014)

A constructive proof of the axiom of dependent choice, compatible with classical logic (pdf, LICS, June 2012) (recorded video, HIM, August 2018)

An intuitionistic logic that proves Markov's principle (pdf, LICS, June 2010) (recorded video, HIM, July 2018)

Talk on the Calculus of Inductive Constructions in sequent calculus form (pdf, DTP, July 2010)

Synthetic talk on the Calculus of Inductive Constructions (ps, pdf, PPS, September 2009)

An approach to call-by-name delimited continuations (pdf, POPL, January 2008)

Introductory talk on call-by-name delimited continuations (pdf, advi, July 2007)

Talk on the duality of computation (pdf, advi, HOR '06) (pdf, PRELUDE, January 2008)

Talk on games, sequent calculus and abstract machines (ps, APPSEM '01)