A Rewriting View of Simple Typing

TL;DR

This paper demonstrates how a rewriting perspective on simple typing can simplify proofs of key properties like preservation, progress, and normalization, and how automated tools can assist in these proofs.

Contribution

It introduces a rewriting-based framework for simple type theory, enabling new proofs and automation of meta-theoretic results.

Findings

Rewriting view simplifies proofs of preservation and progress.

Automated tools assist in meta-theoretic proof automation.

Normalization proof adapted to the rewriting approach.

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.