Before lecture, read the paper assigned below, and submit two items
to the submission website
- Submit your own question about the paper (e.g., what you find most
confusing about the paper or the paper's general context/problem), before
lecture (i.e., 1pm). You cannot use the question below. To the extent
possible, during lecture we will try to answer questions submitted
- Submit your answer for the question below, before the beginning of the lecture.
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?
Seminal result in the field.
Both the artifact and the techniques are used in many subsequent papers.
Good to know that this is possible with current verification tools.
What to learn from this paper?
What does it mean to write a correct compiler? What is the spec of a compiler?
Useful technique of translation validation.
Answer this question
Are there properties that you might want from a compiler that are not
captured by definition 2?