@inproceedings{e040ebf5bd16482482fd1ccc19c9fbea,
title = "Strong normalization for system F by HOAS on top of FOAS",
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.",
keywords = "General-purpose framework, Higher-order abstract syntax, Isabelle/HOL, System F",
author = "Andrei Popescu and Gunter, \{Elsa L.\} and Osborn, \{Christopher J.\}",
year = "2010",
doi = "10.1109/LICS.2010.48",
language = "English (US)",
isbn = "9780769541143",
series = "Proceedings - Symposium on Logic in Computer Science",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "31--40",
booktitle = "Proceedings - 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010",
address = "United States",
note = "25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010 ; Conference date: 11-07-2010 Through 14-07-2010",
}