This course is a continuation of "Software foundations in Coq" and it offers a hands-on introduction to compiler certification in Coq. The course comprises two parts: a seminar at which students present both classical and most recent papers on compiler certification, and a group project aiming at developing (parts of) a certified compiler for a functional language with algebraic effects.
- Teacher: Dariusz Biernacki
- Teacher: Piotr Polesiuk