Introducing Certified Compilation in Education by a Functional Language Approach

Per Lindgren
(Luleå University of Technology)
Marcus Lindner
(Luleå University of Technology)
Nils Fitinghoff
(Luleå University of Technology)

Classes on compiler technology are commonly found in Computer Science curricula, covering aspects of parsing, semantic analysis, intermediate transformations and target code generation. This paper reports on introducing certified compilation techniques through a functional language approach in an introductory course on Compiler Construction. Targeting students with little or no experience in formal methods, the proof process is highly automated using the Why3 framework. Underlying logic, semantic modelling and proofs are introduced along with exercises and assignments leading up to a formally verified compiler for a simplistic imperative language.

This paper covers the motivation, course design, tool selection, and teaching methods, together with evaluations and suggested improvements from the perspectives of both students and teachers.

In Peter Achten and Heather Miller: Proceedings Seventh International Workshop on Trends in Functional Programming in Education (TFPIE 2018), Chalmers University, Gothenburg, Sweden, 14th June 2018, Electronic Proceedings in Theoretical Computer Science 295, pp. 65–78.
Published: 18th June 2019.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: