Files in this item



application/pdfHOASandStrongNormalization.pdf (380kB)
(no description provided)PDF


Title:HOAS and Strong Normalization -- an exercise in HOAS --
Author(s):Popescu, Andrei
Subject(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.
Issue Date:2009-05-11
Genre:Technical Report
Publication Status:unpublished
Date Available in IDEALS:2009-05-11

This item appears in the following Collection(s)

Item Statistics