Lecture preparation
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
beforehand.
- 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.
Assignment
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?
