Files in this item



application/pdfHOASonTopOfFOAS.pdf (182kB)
(no description provided)PDF


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
Publication Status:published or submitted for publication
Peer Reviewed:is peer reviewed
Date Available in IDEALS:2010-05-02

This item appears in the following Collection(s)

Item Statistics