Journal article
A REWRITING VIEW OF SIMPLE TYPING
Logical methods in computer science, Vol.9(1), pp.4/1-29
01/01/2013
DOI: 10.2168/LMCS-9(1:04)2013
Abstract
This paper shows how a recently developed view of typing as small-step abstract reduction, due to Kuan, MacQueen, and Findler, can be used to recast the development of simple type theory from a rewriting perspective. We show how standard meta-theoretic results can be proved in a completely new way, using the rewriting view of simple typing. These meta-theoretic results include standard type preservation and progress properties for simply typed lambda calculus, as well as generalized versions where typing is taken to include both abstract and concrete reduction. We show how automated analysis tools developed in the term-rewriting community can be used to help automate the proofs for this meta-theory. Finally, we show how to adapt a standard proof of normalization of simply typed lambda calculus, for the rewriting approach to typing.
Details
- Title: Subtitle
- A REWRITING VIEW OF SIMPLE TYPING
- Creators
- Aaron Stump - Univ Iowa, Iowa City, IA 52242 USAHans Zantema - TU Eindhoven, Dept Comp Sci, Eindhoven, NetherlandsGarrin Kimmell - Univ Iowa, Iowa City, IA 52242 USARuba El Haj Omar - Univ Iowa, Iowa City, IA 52242 USA
- Resource Type
- Journal article
- Publication Details
- Logical methods in computer science, Vol.9(1), pp.4/1-29
- Publisher
- Logical Methods Computer Science E V
- DOI
- 10.2168/LMCS-9(1:04)2013
- ISSN
- 1860-5974
- eISSN
- 1860-5974
- Number of pages
- 29
- Grant note
- CCF-0910510 / U.S. National Science Foundation; National Science Foundation (NSF)
- Language
- English
- Date published
- 01/01/2013
- Academic Unit
- Computer Science
- Record Identifier
- 9984259498702771
Metrics
9 Record Views