Compiler verification in LF

John Joseph Hannan, Frank Pfenning

Research output: Chapter in Book/Report/Conference proceedingConference contribution

42 Scopus citations

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).

Original languageEnglish (US)
Title of host publicationProceedings - Symposium on Logic in Computer Science
PublisherPubl by IEEE
Pages407-418
Number of pages12
ISBN (Print)0818627352
Publication statusPublished - Jun 1992
EventProceedings of the 7th Annual IEEE Symposium on Logic in Computer Science - Santa Cruz, CA, USA
Duration: Jun 22 1992Jun 25 1992

Other

OtherProceedings of the 7th Annual IEEE Symposium on Logic in Computer Science
CitySanta Cruz, CA, USA
Period6/22/926/25/92

    Fingerprint

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Cite this

Hannan, J. J., & Pfenning, F. (1992). Compiler verification in LF. In Proceedings - Symposium on Logic in Computer Science (pp. 407-418). Publ by IEEE.