Lectures & tutorials

  • Summer School on Metaprogramming (Dagstuhl, 2019)
    I gave two lectures in the 2nd summer school on Metaprogramming. There were two interactive demos that you can go over and process in the F* interactive mode. One goes over the various types of quoting and program generation. The other implements a mini type-class resolution system.

  • Metaprogramming (University of Cambridge, 2018)
    I gave a lecture in the metaprogramming class, introducing our metaprogramming framework in F* and its applications ranging from tactics, DSLs to code generation. PPTX

  • Summer School on Formal Techniques (SRI, 2018)
    Nik Swamy and I gave a two-part lecture about program verification in F* and its application to the Low* toolchain. PDF, live demo, exercise 1, exercise 2

  • PLDI Tutorial (2018)
    I gave a Low* programming tutorial at PLDI. PDF

  • MPRI (2017)
    I gave a lecture at the “Cryptographic protocols formal and computational proofs” MPRI course about pure, stateful, and low-level programming and verification in F*.
    PDF, Exercise 1, (answers), Exercise 2 (answers, memory safety) (answers, functional spec)

Junior Seminar (2011-2013)

With Mathieu Feuillet and Emanuele Leoncini, I kept the Junior Seminar running at Rocquencourt for two years. As of 2018, the seminar was still running!

Teaching assistantship (2010-2014)

  • 2013-2014 I worked on the online algorithms course from École Polytechnique, on Coursera.
  • 2011-2013 I was a teaching assistant for INF431 (algorithms) and « Modal Web » (Web programming) at École Polytechnique
  • 2010-2011 I was a teaching assistant for INF311 (introduction to algorithms) at École Polytechnique