| Title: | Strong normalization for System F by HOAS on top of FOAS |
| Author(s): | Popescu, Andrei; Gunter, Elsa L.; Osborn, Christopher J. |
| Subject(s): | Higher-Order Abstract Syntax, Isabelle/HOL |
| 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 {\em definitional extension} on top of FOAS (First-Order Abstract Syntax).
As such, HOAS is not only an {\em encoding technique}, but also
a {\em 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.
HOAS makes our proof considerably more direct than previous proofs.
The concepts and results presented here have been formalized in the theorem prover
Isabelle/HOL. |
| Issue Date: | 2010 |
| Citation Info: | This is an extended version of a paper to be presented at LICS 2010. |
| Genre: | Technical Report |
| Type: | Text |
| Language: | English |
| URI: | http://hdl.handle.net/2142/15451 |
| Publication Status: | published or submitted for publication |
| Peer Reviewed: | is peer reviewed |
| Date Available in IDEALS: | 2010-05-02 |
HOASonTopOfFOAS.pdf (182kB)