Lecture preparation

Before lecture, read the paper assigned below, and submit two items to the submission website:

Also keep in mind that you will need to write a paper summary for your choice of papers throughout the semester.


Read the paper Formal verification of a realistic compiler by Xavier Leroy, and a note on CompCert's terminology.

Why are we reading this paper?

What to learn from this paper?

Answer this question

Are there properties that you might want from a compiler that are not captured by definition 2?