Teaching

• Intro to Logic (2024)
• Programs and Interactive Proofs (2025)
• Languages and Machines (2025)

All the information is available on the BrightSpace. See also the Education section on the FC webpage.

If you are a student and you are interested in doing a project (be it a short project or a thesis) related to one of mine research topics, please don’t hesitate to contact me.

See here for a list of previous student projects offered from our group.

• Languages and Machines (2024)
• Intro to Logic (2023), Models and Semantics of Computation (2023)
• Program Correctness, 2021, 2022
  Why3, Why3 tutorial

• Type Theory and Coq, 2019/2020
  In the final part of the course we look at MetaCoq/TemplateCoq. See also a recent overview of MetaCoq.
• Co-TA for Type Theory and Coq, 2018/2019.
  The topic for the last part of the course is guarded type theory.
• TA for Type Theory and Coq, 2017/2018.
  In the final part of the course we will be looking at continuation passing style and CPS transformations.
• TA for Type Theory and Coq, 2016/2017.
  In the final part of the course we looked into logical relations. Extra materials: Contextual equivalence proof for logical relations, example proofs in the Abadi-Plotkin logic. UPDATE: there is now an even more comprehensive introduction to logical relations by Lau Skorstengaard: arXiv:1907.11133.
• TA for Berekenbaarheid (Computability), 2016, 2018.
  Extra materials: some exercises on reductions and Rice’s theorem.