“[Abstract]. This paper describes a verfied compiler for PreScheme, the implementation language for the vlisp run-time system. The compiler and proof were divided into three parts: A transformational front end that translates source text into a core language, a syntax-directed compiler that translates the core language into combinator-based treemanipulation language, and a linearizer that translates combinator code into code for an abstract stored-program machine with linear memory for both data and code. This factorization enabled dierent proof techniques to be used for the dierent phases of the compiler, and also allowed the generation of good code. Finally, the whole process was made possible by carefully dening the semantics of vlisp PreScheme rather than just adopting Scheme’s. We believe that the architecture of the compiler and its correctness proof can easily be applied to compilers for languages other than PreScheme.”
PreScheme is the system that Scheme48 (s48.org) uses to “boostrap” the compiler and runtime. It’s lower-level than Scheme, but still has many of the same features you’d want in a Scheme-like language. This paper talks about using a verified compiler for PreScheme in the “verified lisp” project at NEC. I’m hacking my longer talk on PLT, Types, & appsec, and remembered this paper from long ago when I was first looking at preScheme (say ~2006).