Logic in Computer Science (LICS 1992)

Paper: Compiler verification in LF (at LICS 1992)

Authors: Hannan, J. Pfenning, F.

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 = 	 {Hannan, J. and Pfenning, F.},
    title = 	 {Compiler verification in LF},
    booktitle =  {Proceedings of the Seventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1992},
    year =	 1992,
    editor =	 {Andre Scedrov},
    month =	 {June}, 
    pages =      {407--418},
    location =   {Santa Cruz, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }