Axel Dold, Vincent Vialard "A Mechanically Verified Compiling Specification for a Lisp Compiler"

(2001) Proceedings of the 21st LAFL Conference  

Languages mentioned Cint {2001} Cint - c-like machine-independant code ComLisp {1996} Common Lisp subset for dynamic compilation SIL {1998} Stack Intermediate Language