We report on an ongoing effort in mechanically proving correct a compiling specification for a bootstrap compiler from ComLisp (a subset of ANSI Common Lisp sufficiently expressive to serve as a compiler implementation language) to binary Transputer code using the PVS system. The compilation is carried out in four steps through a series of intermediate languages. This paper focuses on the first phase, namely, the compilation of ComLisp to the stack-intermediate language SIL, where parameter passing is implemented by a stack technique. The context of this work is the joint research effort Verifix aiming at developing methods for the construction of correct compilers for realistic programming languages. Keywords: interactive theorem proving, formal specification and verification, compiler verification.

 

Online Copy

Slightly expanded version available as Postscript (223 KB)

BibTeX Entry

@InProceedings{Dold:01:verification,
  author =       {Axel Dold and Vincent Vialard},
  title =        {A Mechanically Verified Compiling Specification for
                  a Lisp Compiler},
  booktitle =    {FST TCS 2001: Foundations of Software Technology and
                  Theoretical Computer Sience},
  pages =        {144-155},
  year =         2001,
  editor =       {Ramesh Hariharan and Madhavan Mukund and V. Vinay},
  volume =       2245,
  series =       lncs,
  publisher =    springer
}