2026-07-20T10:41:57Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3134 2024-03-06T10:33:52Z ddc:004 open_access

Type Preservation as a Confluence Problem Stump, Aaron Kimmell, Garrin El Haj Omar, Roba Term rewriting Type Safety Confluence This paper begins with recent work by Kuan, MacQueen, and Findler, which shows how standard type systems, such as the simply typed lambda calculus, can be viewed as abstract reduction systems operating on terms. The central idea is to think of the process of typing a term as the computation of an abstract value for that term. The standard metatheoretic property of type preservation can then be seen as a confluence problem involving the concrete and abstract operational semantics, viewed as abstract reduction systems (ARSs). In this paper, we build on the work of Kuan et al. by showing show how modern ARS theory, in particular the theory of decreasing diagrams, can be used to establish type preservation via confluence. We illustrate this idea through several examples of solving such problems using decreasing diagrams. We also consider how automated tools for analysis of term-rewriting systems can be applied in testing type Schloss Dagstuhl – Leibniz-Zentrum für Informatik Aaron Stump and Garrin Kimmell and Roba El Haj Omar 2011 Is Part Of LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2011.345 urn:nbn:de:0030-drops-31343 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.345 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode