License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2011.345
URN: urn:nbn:de:0030-drops-31343
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2011/3134/
Go to the corresponding LIPIcs Volume Portal

Stump, Aaron ; Kimmell, Garrin ; El Haj Omar, Roba

Type Preservation as a Confluence Problem

pdf-format:
27.pdf (0.5 MB)

Abstract

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

BibTeX - Entry

@InProceedings{stump_et_al:LIPIcs:2011:3134,
  author =	{Aaron Stump and Garrin Kimmell and Roba El Haj Omar},
  title =	{{Type Preservation as a Confluence Problem}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{345--360},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9 },
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Manfred Schmidt-Schau{\ss}},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/3134},
  URN =		{urn:nbn:de:0030-drops-31343},
  doi =		{10.4230/LIPIcs.RTA.2011.345},
  annote =	{Keywords: Term rewriting, Type Safety, Confluence}
}

Keywords: Term rewriting, Type Safety, Confluence
Collection: 22nd International Conference on Rewriting Techniques and Applications (RTA'11)
Issue Date: 2011
Date of publication: 26.04.2011

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI