Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Seventh Annual IEEE Symposium on

Logic in Computer Science (LICS 1992)

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}
  }
   

Last modified: 2017-04-0512:37
Andrzej Murawski