Credible Compilers
Author(s)
Rinard, Martin C.![Thumbnail](/bitstream/handle/1721.1/149889/MIT-LCS-TR-776.pdf.jpg?sequence=3&isAllowed=y)
DownloadMIT-LCS-TR-776.pdf (2.675Mb)
Metadata
Show full item recordAbstract
This paper presents a new concept in compiler correctness: instead of proving that the compiler performs all of its transformations correctly, the compiler generates a proof that the transformed program correctly implements the input program. A simple pro
Date issued
1999-03Series/Report no.
MIT-LCS-TR-776