Because compilers are trusted components of almost every computer system, it is important to have trustworthy proofs of their correctness. A new method of proving compilers correct using higher- order abstract assembly language has been developed recently. This project is to study how to extend such proofs to more realistic compilers. Mechanical support for the proof process will allow the resulting proofs to be more trustworthy by supplying independent verification of the human prover's work. Three main areas of activities in this project include: (1) the use of mechanical theorem- provers to support compiler correctness proofs, (2) the extension of such proofs to optimizing compilers, and (3) a cooperative development of a verified compiler for Scheme.
