Title :
Compiler verification in LF
Author :
Hannan, John ; Pfenning, Frank
Author_Institution :
Dept. of Comput. Sci., Copenhagen Univ., Denmark
Abstract :
A methodology for the verification of compiler correctness based on the LF logical framework as realized within the Elf programming language is presented. This technique is used to specify, implement, and verify a compiler from a simple functional programming language to a variant of the Categorical Abstract Machine (CAM)
Keywords :
formal logic; program compilers; program verification; CAM; Categorical Abstract Machine; Elf programming language; LF logical framework; compiler correctness; functional programming language; verification; CADCAM; Computer aided manufacturing; Computer languages; Computer science; Mechanical factors; Program processors;
Conference_Titel :
Logic in Computer Science, 1992. LICS '92., Proceedings of the Seventh Annual IEEE Symposium on
Conference_Location :
Santa Cruz, CA
Print_ISBN :
0-8186-2735-2
DOI :
10.1109/LICS.1992.185552
