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

Contents

The exercises is divided into the following parts:

Schedule

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