A rewriting view of simple typing

DOI10.2168/LMCS-9(1:4)2013MaRDI QIDQ4913767zbMATH OpenOpenAlexFDO

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

Publication date 9 April 2013

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1211.0865

zbMATH Keywords

confluencesimple type theorysimply typed lambda-calculusterm rewritingterm-rewritingtype safety

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Grammars and rewriting systems (68Q42)

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.

Recommendations

• The simply typed rewriting calculus
• Towards a proof theory of rewriting: The simply typed \(2\lambda\)-calculus
• Type Preservation as a Confluence Problem
• Approximation and normalization results for typeable term rewriting systems
• scientific article; zbMATH DE number 1692906

Cited in

(5)

• Simply-typed underdeterminism
• Labelings for decreasing diagrams
• scientific article; zbMATH DE number 1722665 (Why is no real title available?)
• Finding small counterexamples for abstract rewriting properties
• First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification

Describes a project that uses

Uses Software

• Automath

This page was built for publication: A rewriting view of simple typing

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4913767)