Compiler Verification in LF

We sketch a methodology for the verification of compiler correctness based on the LF Logical Framework as realized within the Elf programming language. We have applied this technique to specify, implement, and verify a compiler from a simple functional programguage to a variant of the Categorical Abstract Machine (CAM).

• Type: Conference
• Year: 1992
• Where: LICS
• Authors: John Hannan, Frank Pfenning
• Keywords: Automated Reasoning, Compiler Correctness, Elf Programming Language, LF Logical Framework, LICS 1992