Cint(ID:3518/cin002)
Cint - c-like machine-independant code
- Country: de
- Began: 2001
- Sammet:MLT
Cint is a machine-independant c-like language. Takes the S-Expressions from ComLisp via SIL as integers only, and translates them to TASM (transputer assembly)
Related languages
C |
=> |
Cint | |
Influence |
SIL |
=> |
Cint | |
Target language for |
TASM |
=> |
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
|