Paper: Compiler verification in LF (at LICS 1992)

Authors: John Hannan Frank Pfenning

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)

BibTeX

  @InProceedings{HannanPfenning-Compilerverificatio,
    author = 	 {John Hannan and Frank Pfenning},
    title = 	 {Compiler verification in LF},
    booktitle =  {Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science (LICS 1992)},
    year =	 {1992},
    month =	 {June}, 
    pages =      {407--418},
    location =   {Santa Cruz, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }