License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2015.143
URN: urn:nbn:de:0030-drops-51949
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5194/
Go to the corresponding LIPIcs Volume Portal

Endrullis, Jörg ; Hansen, Helle Hvid ; Hendriks, Dimitri ; Polonsky, Andrew ; Silva, Alexandra

A Coinductive Framework for Infinitary Rewriting and Equational Reasoning

pdf-format:
14.pdf (0.5 MB)

Abstract

We present a coinductive framework for defining infinitary analogues of equational reasoning and rewriting in a uniform way. The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence. This makes the framework especially suitable for formalizations in theorem provers.

BibTeX - Entry

@InProceedings{endrullis_et_al:LIPIcs:2015:5194,
  author =	{J{\"o}rg Endrullis and Helle Hvid Hansen and Dimitri Hendriks and Andrew Polonsky and Alexandra Silva},
  title =	{{A Coinductive Framework for Infinitary Rewriting and Equational Reasoning}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{143--159},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Maribel Fern{\'a}ndez},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5194},
  URN =		{urn:nbn:de:0030-drops-51949},
  doi =		{10.4230/LIPIcs.RTA.2015.143},
  annote =	{Keywords: infinitary rewriting, coinduction}
}

Keywords: infinitary rewriting, coinduction
Collection: 26th International Conference on Rewriting Techniques and Applications (RTA 2015)
Issue Date: 2015
Date of publication: 18.06.2015

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