Interactive Teaching of Programming Language Theory with a Proof Assistant

  • Péter Bereczky
  • István Donkó
  • Dániel Horpácsi ELTE
  • Ambrus Kaposi
  • Dávid János Németh
Keywords: formal semantics, type systems, proof assistant, Coq, interactive teaching


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 better learning experience and build technical skills in applying formal methods. The authors have launched practice classes for two programming language theory subjects and carefully developed course material based on executable and verifiable definitions formalised in the Coq proof assistant. In this paper, we share our experiences regarding the design and implementation of the new material, we outline the pros and cons of using a proof assistant in the courses, and we describe how the presented method may be adapted to other courses.

How to Cite
Bereczky, P., Donkó, I., Horpácsi, D., Kaposi, A., & Németh, D. J. (2020). Interactive Teaching of Programming Language Theory with a Proof Assistant. Central-European Journal of New Technologies in Research, Education and Practice, 2(1), 19-33.
Scientific Papers