Logic in Computer Science, Symposium on (2010)
Edinburgh, United Kingdom
July 11, 2010 to July 14, 2010
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2010.48
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.
Higher-Order Abstract Syntax, System F, Isabelle/HOL
E. L. Gunter, C. J. Osborn and A. Popescu, "Strong Normalization for System F by HOAS on Top of FOAS," Logic in Computer Science, Symposium on(LICS), Edinburgh, United Kingdom, 2010, pp. 31-40.