Compiler verification in LF
- 2 January 2003
- proceedings article
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 407-418
- https://doi.org/10.1109/lics.1992.185552
Abstract
We sketch a methodology for the verication of com- piler 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 program- ming language to a variant of the Categorical Abstract Machine (CAM).Keywords
This publication has 16 references indexed in Scilit:
- Natural semanticsPublished by Springer Nature ,2005
- Elf: a language for logic definition and verified metaprogrammingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- A framework for defining logicsJournal of the ACM, 1993
- An algorithm for testing conversion in type theoryPublished by Cambridge University Press (CUP) ,1991
- Operational semantics in a natural deduction settingPublished by Cambridge University Press (CUP) ,1991
- Staging transformations for abstract machinesPublished by Association for Computing Machinery (ACM) ,1991
- From operational semantics to abstract machines: preliminary resultsPublished by Association for Computing Machinery (ACM) ,1990
- Two-level semantics and code generationTheoretical Computer Science, 1988
- The categorical abstract machineScience of Computer Programming, 1987
- A simple applicative language: mini-MLPublished by Association for Computing Machinery (ACM) ,1986