Lecture: Compilers: CompCert

Date: 3/1/17

Reading

• Required reading: Formal verification of a realistic compiler, Xavier Leroy, CACM, 2008.
• Optional reading: A formally verified compiler back-end, Xavier Leroy, Journal of Automated Reasoning, 2009.
• Optional reading: Compositional CompCert, Gordon Stewart, Lennart Beringer, Santiago Cuellar, Andrew W. Appel, POPL, 2015.