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
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)
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