Talks

• Proofs-as-programs for programmers (ThEdu, Nancy, 2024) pdf
• Say it intensionally (ECNU, 2024) pdf
• Small inversion for smaller inversions (TYPES, 2022) pdf
• Smaller inversions and Unleashed Recursion in Coq (several places, 2021) pdf
• Probabilistic Testing Semantics in Coq (Catuscia Palamidessi Festschrift, 2019) pdf
• Handcrafted Small Inversions Made Operational on Operational Semantics (ITP'2013, Rennes, jul. 2013) pdf
• Designing a CPU model: from a pseudo-formal document to fast code (Rapido'2011, Heraklion, Jan. 2011) pdf
• On defining McCarthy f91 in CIC (TYPES'2008, Torino, mar. 2008) pdf, with a coq development (to come).
• Apero-reflexion (JFLA, Aix-les-Bains, jan. 2007) pdf (in french), with a coq demo.
• Proving termination using dependent types: the case of xor-terms (common session TFP+TYPES, Nottingham, april 2006). pdf.
• Defending the Bank with a Proof Assistant (WITS, Vienna, march 2006). pdf.
• Proof pearl: From concrete to functional unparsing (TPHOLs, sept 2004). advi.
• A formalisation of the join-calculus in type theory (IWFMS'04, Nanjing). pdf, advi.