• Distinguished Lecture, NUS Computer Science Research Week, January 2024. Online

  • HCSS Keynote, May 2023. Online

  • Aeneas: Rust verification by functional translation PPTX. This covers the new Rust verification toolchain developed with my student Son Ho. See Son’s presentation at ICFP, or this talk given at an internal seminar. Variations of this talk given at Galois (Oct 2022), NESVD (Nov 2022), Azure, Academia Sinica (Taiwan, Apr 2023), Kobayashi Lab (Tokyo, Mar 2023), and more.

  • Formal Computational Law PPTX. This covers my whole formal computational law agenda, including: Catala, Lean, LFOs, etc. Talk given at: Microsoft Research Summit (2022), Online Logic Seminar (SIU, 2022), World AI & IOT Congress (2021, keynote), AISEC’21 workshop, internal presentations, etc.

  • The Noise verified protocol compiler PPTX. This describes the S&P’22 work, wherein a single meta-programmed compiler takes a DSL description of a Noise protocol and produces 49 verified low-level implementations complete with security proof in the symbolic model. Presented by Son Ho at S&P, and by myself through various internal seminars.

  • The EverCrypt verified library, Mini-Symposium on Security and Privacy at the Edge, UCSD, 2019. PPTX. I also presented EverCrypt at: the Cambridge Computer Lab (2019), New England Systems Verification Days (2018), NYU (2019), IDA CCS (2020), Boston University (2020), the SOIL initiative (2020)

  • Building and deploying verified components in the HTTPS ecosystem. This is the latest and most updated version of a talk given at: the Cambridge Computer Lab, MIT, the Celtique team (INRIA Rennes). PPTX

  • Verified Embedded Low-Level Programming in F*, ICFP’17. PDF

  • Secure compilation from F* to C using the KreMLin compiler, Models and Tools for Security Analysis and Proofs (MTP), 2017. PDF This is an improved version of talk previously given at the ML Workshop (2016) and the Secure Compilation Meeting (POPL’17 workshop).

  • Young Researcher Panel Session, Programming Languages Mentoring Workshop (PLMW), 2017. Website

  • GSP: a memory model for distributed systems (invited), Journées Francophones du Logiciel Applicatif (JFLA), 2016. PDF Talk also given at Gallium (INRIA Paris) and Celtique (INRIA Rennes).

  • The BBC micro:bit and TouchDevelop (keynote), Programming for Mobile and Touch (PROMOTO) 2015. PPTX Talk also given at the Workshop on Programming Languages Technology for Massive Open Online Courses (PLOOC), 2015.

  • Translating from TouchDevelop to C++11 (short presentation), cppcon (the c++ conference), 2015. PPTX

  • Mezzo, the language of the future PhD defense, September 2014. PDF

  • The design of Mezzo, a new programming language ICFP’13. PDF I gave variations of “the Mezzo talk” at: INRIA (Rocquencourt, 2011), the PPS lab (Paris, 2012), the Proval team (Saclay, 2012), Texas A&M university (Texas, USA, 2012), Google (New York, USA, 2012), the Computer Lab (Cambridge, UK, 2013), INRIA (Rennes, Celtique Team, 2014), Microsoft Research (Redmond, USA, 2014), Microsoft C++ team (Redmond, USA, 2015), as well as all the other locations mentioned above (IFL, ICFP, ML, FSFMA, and finally my PhD defense). Dr. Pottier also gave several more Mezzo talks!

  • Why design a new programming language? FSFMA’13. PDF

  • What is type-checking? INRIA Junior Seminar, June 2013. PDF, Video

  • An introduction to Mezzo (short). ML’12. PDF, YouTube