University of Illinois Urbana-Champaign

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

Popescu, Andrei

Content Files
HOASandStrongNormalization.pdf

Permalink

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

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
Date of Ingest
2009-05-11T22:27:04Z
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
Genre of Resource
Technical Report
Permalink
http://hdl.handle.net/2142/11752

Owning Collections

Research and Tech Reports - Computer Science PRIMARY