Strong normalization for system F by HOAS on top of FOAS

Andrei Popescu, Elsa L. Gunter, Christopher J. Osborn

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

Abstract

We present a point of view concerning HOAS (Higher-Order Abstract Syntax) and an extensive exercise in HOAS along this point of view. The point of view is that HOAS can be soundly and fruitfully regarded as a definitional extension on top of FOAS (First-Order Abstract Syntax). As such, HOAS is not only an encoding technique, but also a higher-order view of a first-order reality. A rich collection of concepts and proof principles is developed inside the standard mathematical universe to give technical life to this point of view. The exercise consists of a new proof of Strong Normalization for System F. The concepts and results presented here have been formalized in the theorem prover Isabelle/HOL.

Original languageEnglish (US)
Title of host publicationProceedings - 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages31-40
Number of pages10
ISBN (Print)9780769541143
DOIs
StatePublished - 2010
Event25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010 - Edinburgh, United Kingdom
Duration: Jul 11 2010Jul 14 2010

Publication series

NameProceedings - Symposium on Logic in Computer Science
ISSN (Print)1043-6871

Other

Other25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010
Country/TerritoryUnited Kingdom
CityEdinburgh
Period7/11/107/14/10

Keywords

  • General-purpose framework
  • Higher-order abstract syntax
  • Isabelle/HOL
  • System F

ASJC Scopus subject areas

  • Software
  • Mathematics(all)

Fingerprint

Dive into the research topics of 'Strong normalization for system F by HOAS on top of FOAS'. Together they form a unique fingerprint.

Cite this