The Community for Technology Leaders
Logic in Computer Science, Symposium on (2010)
Edinburgh, United Kingdom
July 11, 2010 to July 14, 2010
ISSN: 1043-6871
ISBN: 978-0-7695-4114-3
pp: 31-40
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.
100 ms
(Ver 3.3 (11022016))