2026-10-14T13:11:06Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5194 2024-03-06T09:36:02Z ddc:004 open_access

A Coinductive Framework for Infinitary Rewriting and Equational Reasoning Endrullis, Jörg Hansen, Helle Hvid Hendriks, Dimitri Polonsky, Andrew Silva, Alexandra infinitary rewriting coinduction 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jörg Endrullis and Helle Hvid Hansen and Dimitri Hendriks and Andrew Polonsky and Alexandra Silva 2015 Is Part Of LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2015.143 urn:nbn:de:0030-drops-51949 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.143 eng https://creativecommons.org/licenses/by/3.0/legalcode