HOAS and Strong Normalization -- an exercise in HOAS --

Popescu, Andrei

Permalink

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

Description

Title

HOAS and Strong Normalization -- an exercise in HOAS --

Author(s)

Popescu, Andrei

Issue Date

2009-05-11

Keyword(s)

• Higher Order Abstract Syntax
• System F
• Strong Normalization

Abstract

We develop some Higher-Order Abstract Syntax (HOAS) concepts and proof principles as a collection of definitions and propositions on top of the original syntax with bindings. Our approach brings together hassle-free (i.e., binding- and substitution-free) manipulation of the objects on the one hand, and inductive reasoning about the same objects on the other. We present our approach by providing adequate representations of the untyped lambda-calculus, its beta-reduction and its Curry-style System F typing. The HOAS induction and recursion principles extracted from the encoding are illustrated by employing them in tandem to naturally (re)discover a proof of strong normalization for typable terms in System F.

Type of Resource

text

Permalink

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

Owning Collections