This paper presents an approach to compiler correctness in which the compiler generates a proof that the transformed program correctly implements the input program. A simple proof checker can then verify that the program was compiled correctly. We call a compiler that produces such proofs a credible compiler, because it produces verifiable evidence that it is operating correctly. / Singapore-MIT Alliance (SMA)
| Identifer | oai:union.ndltd.org:MIT/oai:dspace.mit.edu:1721.1/3674 |
| Date | 01 1900 |
| Creators | Rinard, Martin C. |
| Source Sets | M.I.T. Theses and Dissertation |
| Language | en_US |
| Detected Language | English |
| Type | Article |
| Format | 177863 bytes, application/pdf |
| Relation | Computer Science (CS); |
Page generated in 0.0018 seconds