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) (slight
update presented at the University of Padova, September 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)