A major recent scientific achievement in programming languages research is the development of the first realistic verified C compiler CompCert: a compiler that comes with a computer-verified rigorous correctness proof. In this course, we study basic concepts of verified compilers: both conceptually (what does it mean for a compiler to be correct) and practically (how does one build such a proof in practice). To do this, we first teach the basics of the main tool in this field: dependently-typed programming languages (in our case Agda). In addition to provably correct compilers, we also look at provably secure compilers. This course is taught in a hands-on way, with students learning to program and prove in Agda and studying and extending important compiler passes. Evaluation is done through a course project (with an oral defence) in which students apply the concepts and techniques learned. Functional Programming is a prerequisite for this course, but this course starts a bit later in the semester, so both courses can be followed in parallel.
Dependently typed programming en computer-verified proving in Agda
Inductive data types with parameters and indices
Dependent pattern matching
The identity type
Negation
Proofs by induction
Verified and secure compilation: a selection of compiler passes are studied, for example:
Register allocation
Call lowering
Stack spilling
Closure conversion
These compiler passes are formalised and studied abstractly and/or in Agda, studying verified and secure compilation properties and proofs.
Classes will be taught in a mixed, interactive model. A typical class consists of both teacher explanations and exercises for students in Agda. The first few classes will be more hands-on, exercise-sesssion-like, in order to get students up to speed with Agda. Later classes will contain a bit more advanced material, where a bit more of the implementation will be done in group.
Prof. Dominique Devriese.
Course material consists of the following, made available online through the online course system.
This course is a 2-semester course. Classes will start in approx. the 5th or 6th week of the 1st semester and continue until approx. the 4th or 5th week of the second semester. The project assignment will probably be given at the end of the 1st or beginning of the 2nd semester.
The evaluation consists for 100% of a course project in which the students formalise and prove concepts and proofs in Agda, related to verified and/or secure compilation. The students defend the project orally with the teacher during the exam period. During this defence, their understanding of the concepts taught in this course and their programming and proving skills in Agda will be tested, based on their solution of the course project. The exam is entirely aimed at testing understanding of the material and ability to work with Agda and the code seen in class, rather than testing knowledge of literal definitions and such.