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

lmcs:936 - Logical Methods in Computer Science, February 27, 2013, Volume 9, Issue 1 - https://doi.org/10.2168/LMCS-9(1:4)2013
A Rewriting View of Simple TypingArticle

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

    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.


    Volume: Volume 9, Issue 1
    Published on: February 27, 2013
    Imported on: October 28, 2011
    Keywords: Computer Science - Programming Languages,D.3.1
    Funding:
      Source : OpenAIRE Graph
    • SHF:Large:Collaborative Research: TRELLYS: Community-Based Design and Implementation of a Dependently Typed Programming Language; Funder: National Science Foundation; Code: 0910510

    2 Documents citing this article

    Consultation statistics

    This page has been seen 1200 times.
    This article's PDF has been downloaded 306 times.