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: https://drops.dagstuhl.de/opus/volltexte/2015/5194/
Endrullis, Jörg ; Hansen, Helle Hvid ; Hendriks, Dimitri ; Polonsky, Andrew ; Silva, Alexandra
A Coinductive Framework for Infinitary Rewriting and Equational Reasoning
| pdf-format: |
|
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 | |
| Seminar: | 26th International Conference on Rewriting Techniques and Applications (RTA 2015) | |
| Issue date: | 2015 | |
| Date of publication: | 18.06.2015 |
