Coinductive foundations of infinitary rewriting and infinitary equational logic

DOI10.23638/LMCS-14(1:3)2018zbMATH Open1459.68089arXiv1706.00677MaRDI QIDQ4600775FDOQ4600775

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

Publication date: 12 January 2018

Full work available at URL: https://arxiv.org/abs/1706.00677

Recommendations

• A coinductive framework for infinitary rewriting and equational reasoning
• scientific article; zbMATH DE number 6678680
• Infinitary rewriting: foundations revisited
• Infinitary rewriting: closure operators, equivalences and models
• Proof Terms for Infinitary Rewriting

zbMATH Keywords

coinductioninfinitary rewritinginfinitary equational reasoning

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Logic in computer science (03B70) Equational logic, Mal'tsev conditions (08B05)

Cites Work

• Completely iterative algebras and completely iterative monads
• Term Rewriting and All That
• Title not available (Why is that?)
• An introduction to (co)algebra and (co)induction
• Confluence of the coinductive \(\lambda\)-calculus
• Rewrite, rewrite, rewrite, rewrite, rewrite, \dots
• Transfinite reductions in orthogonal term rewriting systems
• Local termination: theory and practice
• Infinitary normalization
• Complexity of Fractran and Productivity
• PROVING PRODUCTIVITY IN INFINITE DATA STRUCTURES
• Lazy productivity via termination
• Normalization of Infinite Terms
• Circular coinduction in Coq using bisimulation-up-to techniques
• Applications of infinitary lambda calculus
• Highlights in infinitary rewriting and lambda calculus
• Title not available (Why is that?)
• A coinductive confluence proof for infinitary lambda-calculus
• Least upper bounds on the size of confluence and Church-Rosser diagrams in term rewriting and \(\lambda\)-calculus
• Proof Terms for Infinitary Rewriting
• A coinductive framework for infinitary rewriting and equational reasoning
• The minimalist MOVE operation in a deductive perspective
• Infinitary rewriting: closure operators, equivalences and models
• On confluence and residuals in Cauchy convergent transfinite rewriting
• Proving Infinitary Normalization
• Abstract models of transfinite reductions
• Partial order infinitary term rewriting and Böhm trees
• Title not available (Why is that?)
• Infinitary term graph rewriting is simple, sound and complete
• Infinitary term rewriting for weakly orthogonal systems: properties and counterexamples

Cited In (8)

• Coequational logic for finitary functors
• A coinductive framework for infinitary rewriting and equational reasoning
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Non-well-founded deduction for induction and coinduction
• Title not available (Why is that?)
• A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed-points

This page was built for publication: Coinductive foundations of infinitary rewriting and infinitary equational logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4600775)