In this module, we shall see basic principles of mechanised compilation and interpretation. After having recalled basic notions of programming language theory and semantics, we will implement interpreters (following operational semantics specifications) and compilers of a core imperative language in the Coq proof assistant. We shall then use the very same tool to certify our interpreters and compilers, hence giving machine-mechanised proofs of their correctness .
Certified interpretation and compilation of a core language for arithmetic; Practical introduction to Coq
What is Coq: the proposition-as-types correspondence
Operational Semantics of Imp (small-step, big-step, evaluation); operational-semantics based intepreter and its certification
A virtual machine-based compiler for Imp and its certification; simulation theorems between interpretation and compilation
(Time permitting) Static analysis and program logics for Imp; Hoare Logic, liveness analysis
Leroy's course on Mechanized Semantics (slides and code available here https://xavierleroy.org/CdF/2019-2020/ )
X. Leroy, Lecture notes on Mechanized Semantics. (https://xavierleroy.org/courses/Marktoberdorf-2009/notes.pdf)
A. Chilipala. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant (Chapter 2). (http://adam.chlipala.net/cpdt/cpdt.pdf)
Code and notes used in class