Strong normalization for System F by HOAS on top of FOAS

Conference paper

Popescu, A., Gunter, E. and Osborn, C. 2010. Strong normalization for System F by HOAS on top of FOAS. 25th Annual IEEE Symposium on Logic in Computer Science (LICS). Edinburgh, United Kingdom 11 - 14 Jul 2010 Institute of Electrical and Electronics Engineers. pp. 31-40
TypeConference paper
TitleStrong normalization for System F by HOAS on top of FOAS
AuthorsPopescu, A., Gunter, E. and Osborn, C.
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.

KeywordsHigher-Order Abstract Syntax; System F; General-Purpose Framework; Isabelle/HOL
Research GroupFoundations of Computing group
Conference25th Annual IEEE Symposium on Logic in Computer Science (LICS)
Page range31-40
ISSN1043-6871
ISBN
Hardcover9781424475889
PublisherInstitute of Electrical and Electronics Engineers
Publication dates
Print13 Sep 2010
Publication process dates
Deposited23 Apr 2015
Accepted01 Mar 2010
Output statusPublished
Accepted author manuscript
Copyright Statement

© 2010 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.

Additional information

Online ISBN:9781424475896

Web address (URL)http://dx.doi.org/10.1109/LICS.2010.48
LanguageEnglish
Book title2010 25th Annual IEEE Symposium on Logic in Computer Science (LICS)
Permalink -

https://repository.mdx.ac.uk/item/85120

Log in to edit

Download files

Accepted author manuscript
LICS2010.pdf

  • 14
    total views
  • 4
    total downloads
  • 0
    views this month
  • 0
    downloads this month

Export as