Study of the Formal Verification of Compilers

This page describes an exercise on compiler verification based on the lecture given by Xavier Leroy at the DeepSpec Summer School in 2017. The goal is to get the students familiar with the basics concepts in compiler verification by doing the Coq project coming along with the lecture.

Course Materials


The exercises is divided into the following parts:


We plan to finish this exercise in two weekends. The schedule is as follows: