## Files in this item

FilesDescriptionFormat

application/pdf

HOASonTopOfFOAS.pdf (182kB)
(no description provided)PDF

## Description

 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
﻿