Strong normalization for System F by HOAS on top of FOAS

Popescu, Andrei; Gunter, Elsa L.; Osborn, Christopher J.

Permalink

https://hdl.handle.net/2142/15451 Copy

Description

Title

Strong normalization for System F by HOAS on top of FOAS

Author(s)

• Popescu, Andrei
• Gunter, Elsa L.
• Osborn, Christopher J.

Issue Date

2010

Keyword(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.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/15451

Owning Collections