A Rewriting View of Simple Typing
Aaron Stump (University of Iowa), Garrin Kimmell (University of Iowa),, Hans Zantema (TU Eindhoven), Ruba El Haj Omar (University of Iowa)

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
