Stump, Aaron and Kimmell, Garrin and Zantema, Hans and Omar, Ruba El Haj - A Rewriting View of Simple Typing

lmcs:936 - Logical Methods in Computer Science, February 27, 2013, Volume 9, Issue 1
A Rewriting View of Simple Typing

Authors: Stump, Aaron and Kimmell, Garrin and Zantema, Hans and Omar, Ruba El Haj

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.


Source : oai:arXiv.org:1211.0865
DOI : 10.2168/LMCS-9(1:4)2013
Volume: Volume 9, Issue 1
Published on: February 27, 2013
Submitted on: October 28, 2011
Keywords: Computer Science - Programming Languages,D.3.1


Share

Consultation statistics

This page has been seen 66 times.
This article's PDF has been downloaded 43 times.