SIL(ID:3519/sil003)

Stack Intermediate Language 


Stack Intermediate Language - permits the compilation of ComLisp so that parameter passing may be implemented by a stack technique.


Structures:
Related languages
ComLisp => SIL   Target language for
SIL => Cint   Target language for

References:
  • Axel Dold, Vincent Vialard "A Mechanically Verified Compiling Specification for a Lisp Compiler" view details External link: online Abstract: 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.
    ps
          in Proceedings of the 21st LAFL Conference view details