Speaker
Description
The teaching of programming language theory has a long track record at ELTE Faculty of Informatics. Traditionally, formal semantics and type systems of programming languages, similarly to other theory-oriented subjects, were taught with the pen-and-paper method. However, modern proof assistants call for replacing this old-fashioned way of teaching with novel and interactive methods that bring deeper understanding, provide a better learning experience and build technical skills in applying formal methods. From 2019 on we implemented this paradigm change in multiple programming language theory subjects for the benefit of both the students and the instructors. In this talk, we present the main challenges of bringing machine-checked proofs into the practice classes and share our experiences from the past five years of teaching the Formal semantics course.
