A rewriting view of simple typing

A. Stump, H. Zantema, G. Kimmell, R. El Haj Omar

Research output: Contribution to journalArticleAcademicpeer-review

3 Citations (Scopus)
67 Downloads (Pure)

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.
Original languageEnglish
Pages (from-to)4/1-29
JournalLogical Methods in Computer Science
Volume9
Issue number1
DOIs
Publication statusPublished - 2013

Fingerprint Dive into the research topics of 'A rewriting view of simple typing'. Together they form a unique fingerprint.

Cite this