Interactive Teaching of Programming Language Theory with a Proof Assistant
  • Metaadatok
Tartalom: http://ojs.elte.hu/cejntrep/article/view/470
Archívum: CEJNTREP
Gyűjtemény: Scientific Papers
Cím:
Interactive Teaching of Programming Language Theory with a Proof Assistant
Létrehozó:
Bereczky, Péter
Donkó, István
Horpácsi, Dániel
Kaposi, Ambrus
Németh, Dávid János
Kiadó:
Eötvös Loránd University, Faculty of Informatics
Dátum:
2020-04-28
Tartalmi leírás:
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.
Nyelv:
angol
Típus:
info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion
Peer-reviewed Article
Formátum:
application/pdf
Azonosító:
10.36427/CEJNTREP.2.1.470
Forrás:
Central-European Journal of New Technologies in Research, Education and Practice; 2020: Volume 2, Number 1; 19-33
Central-European Journal of New Technologies in Research, Education and Practice; 2020: Volume 2, Number 1; 19-33
2676-9425
10.36427/CEJNTREP.2.1
Kapcsolat:
Létrehozó: