pith. sign in

arxiv: 2305.18250 · v4 · submitted 2023-05-29 · 💻 cs.LO · cs.PL

On Complexity Bounds and Confluence of Parallel Term Rewriting

Tha\"is Baudon , Carsten Fuhs , Laure Gonnord This is my paper

Pith reviewed 2026-05-24 08:57 UTC · model grok-4.3

classification 💻 cs.LO cs.PL
keywords term rewritingparallel complexityruntime complexityconfluencecomplexity boundsinnermost rewritingprogram analysisbounds
0
0 comments X

The pith

Automatic techniques derive upper and lower bounds on parallel complexity of term rewriting by reusing sequential methods.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper models parallel computation on inductive data structures via parallel-innermost term rewriting and introduces a runtime complexity measure that depends on the size of the starting term. It supplies automatic methods to compute both upper and lower bounds on this parallel complexity, allowing existing sequential complexity techniques to be applied with only minor adaptation. Lower-bound computation requires the parallel-innermost rewrite relation to be confluent, so the work also gives practical sufficient criteria for proving confluence automatically. The resulting methods were implemented in an existing analysis tool and checked against standard benchmarks.

Core claim

Parallel-innermost term rewriting models parallel computation on inductive data structures, with runtime complexity defined parametrically in the size of the start term. Automatic techniques derive upper and lower bounds on parallel complexity by direct reuse of sequential complexity methods, supported by effective sufficient criteria that establish confluence of the parallel-innermost rewrite relation.

What carries the argument

The parallel-innermost rewrite relation, which contracts all disjoint redexes in a single parallel step and thereby defines the parallel runtime measure.

If this is right

  • Upper bounds on parallel complexity are obtained by adapting existing sequential bound techniques.
  • Lower bounds become computable once the supplied criteria establish confluence.
  • Existing program analysis tools can be extended to the parallel setting with modest changes.
  • The approach yields usable bounds on numerous published benchmarks.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same confluence criteria could be tested on parallel rewrite systems outside the innermost strategy.
  • The derived bounds may guide resource allocation when programs operate on tree-shaped data in parallel hardware.
  • Combining the parallel bounds with existing sequential cost analyses could produce joint time-space estimates.

Load-bearing premise

Lower bounds on parallel complexity require that the parallel-innermost rewrite relation is confluent.

What would settle it

A concrete term rewriting system in which the parallel-innermost relation fails confluence yet the supplied criteria still certify confluence, producing an incorrect lower bound.

Figures

Figures reproduced from arXiv: 2305.18250 by Carsten Fuhs, Laure Gonnord, Tha\"is Baudon.

Figure 1
Figure 1. Figure 1: Tree size computation in OCaml In this particular example, the recursive calls size left and size right can be done in parallel. Building on previous work on parallel-innermost rewriting [8, 9] and first ideas about parallel complex￾ity [10], we propose a new notion of Parallel Dependency Tuples that captures such a behaviour, and methods to compute both upper and lower parallel complexity bounds. Bounds o… view at source ↗
Figure 2
Figure 2. Figure 2: Input file for Example 3.1 [PITH_FULL_IMAGE:figures/full_fig_p035_2.png] view at source ↗
read the original abstract

We revisit parallel-innermost term rewriting as a model of parallel computation on inductive data structures and provide a corresponding notion of runtime complexity parametric in the size of the start term. We propose automatic techniques to derive both upper and lower bounds on parallel complexity of rewriting that enable a direct reuse of existing techniques for sequential complexity. Our approach to find lower bounds requires confluence of the parallel-innermost rewrite relation, thus we also provide effective sufficient criteria for proving confluence. The applicability and the precision of the method are demonstrated by the relatively light effort in extending the program analysis tool AProVE and by experiments on numerous benchmarks from the literature.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper proposes automatic techniques to derive upper and lower bounds on the parallel complexity of parallel-innermost term rewriting, enabling direct reuse of existing sequential complexity analysis methods. Upper bounds reuse techniques without additional conditions, while lower bounds require confluence of the parallel-innermost rewrite relation; the authors supply effective sufficient criteria for this confluence. The approach is demonstrated via a light extension of the AProVE tool and experiments on literature benchmarks.

Significance. If the results hold, the work is significant for enabling reuse of mature sequential complexity tools in a parallel setting with minimal additional machinery, as evidenced by the AProVE extension and benchmark results. The provision of confluence criteria and the parametric runtime complexity notion are concrete strengths that support automated analysis of parallel computation on inductive data structures.

minor comments (2)
  1. [Abstract] The abstract states that the lower-bound technique 'requires confluence' and supplies 'effective sufficient criteria,' but does not indicate the frequency with which these criteria succeed on systems where sequential methods already apply; a short discussion or table quantifying this would strengthen the 'direct reuse' claim.
  2. Notation for the parallel complexity measure (parametric in start-term size) is introduced without an explicit comparison table to the sequential case; adding such a table would clarify the reuse mechanism.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of the paper, the recognition of its significance for reusing sequential complexity tools in the parallel setting, and the recommendation of minor revision. No major comments were provided in the report.

Circularity Check

0 steps flagged

No circularity; derivation reuses sequential techniques with independent confluence criteria

full rationale

The paper reuses existing sequential complexity analysis methods for upper bounds on parallel complexity without additional conditions. Lower bounds require confluence of the parallel-innermost relation, for which the authors supply separate sufficient criteria. No quoted step reduces a claimed prediction or bound to a fitted input, self-definition, or load-bearing self-citation chain; the central claims remain independent of the paper's own outputs. This is the common case of a self-contained extension against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Only abstract available; no free parameters, axioms, or invented entities can be identified beyond the stated requirement for confluence in lower bound analysis.

axioms (1)
  • domain assumption Confluence of the parallel-innermost rewrite relation is required to derive lower bounds on parallel complexity.
    Explicitly stated in the abstract as a prerequisite for the lower bound approach.

pith-pipeline@v0.9.0 · 5632 in / 1088 out tokens · 21816 ms · 2026-05-24T08:57:35.010514+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

67 extracted references · 67 canonical work pages · 1 internal anchor

  1. [1]

    On Complexity Bounds and Confluence of Parallel Term Rewriting

    Baudon T, Fuhs C, Gonnord L. On Complexity Bounds and Confluence of Parallel Term Rewriting, 2024. URL https://arxiv.org/abs/2305.18250

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  2. [2]

    Types for Complexity of Parallel Computation in Pi-Calculus

    Baillot P, Ghyselen A. Types for Complexity of Parallel Computation in Pi-Calculus. In: Yoshida N (ed.), Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, vo...

    work page doi:10.1007/978-3-030-72019-3_3 2021

  3. [4]

    A General Framework for Static Cost Analysis of Parallel Logic Programs

    Klemen M, L´opez-Garc´ıa P, Gallagher JP, Morales JF, Hermenegildo MV . A General Framework for Static Cost Analysis of Parallel Logic Programs. In: Gabbrielli M (ed.), Logic-Based Program Synthesis and Transformation - 29th International Symposium, LOPSTR 2019, Porto, Portugal, October 8-10, 2019, Revised Selected Papers, volume 12042 of Lecture Notes in...

    work page doi:10.1007/978-3-030-45260-5_2 2019

  4. [5]

    Parallel Cost Analysis

    Albert E, Correas J, Johnsen EB, Pun KI, Rom´an-D´ıez G. Parallel Cost Analysis. ACM Trans. Comput. Logic, 2018. 19(4):31:1–31:37. URL https://doi.org/10.1145/3274278. 162 T. Baudon et al. / On Complexity Bounds and Confluence of Parallel Term Rewriting

    work page doi:10.1145/3274278 2018

  5. [6]

    Automatic Static Cost Analysis for Parallel Programs

    Hoffmann J, Shao Z. Automatic Static Cost Analysis for Parallel Programs. In: Vitek J (ed.), Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18,

    work page 2015

  6. [7]

    Springer, 2015 pp

    Proceedings, volume 9032 of Lecture Notes in Computer Science. Springer, 2015 pp. 132–157. URL https://doi.org/10.1007/978-3-662-46669-8_6

    work page doi:10.1007/978-3-662-46669-8_6 2015

  7. [8]

    Parallel complexity analysis with temporal session types

    Das A, Hoffmann J, Pfenning F. Parallel complexity analysis with temporal session types. Proc. ACM Program. Lang., 2018. 2(ICFP):91:1–91:30. URL https://doi.org/10.1145/3236786

    work page doi:10.1145/3236786 2018

  8. [9]

    Correct and Optimal Implementations of Recursion in a Simple Programming Language

    Vuillemin J. Correct and Optimal Implementations of Recursion in a Simple Programming Language. J. Comput. Syst. Sci., 1974. 9(3):332–354. URL https://doi.org/10.1016/S0022-0000(74)80048-6

    work page doi:10.1016/s0022-0000(74)80048-6 1974

  9. [10]

    Orderings for Innermost Termination

    Fern´andez M, Godoy G, Rubio A. Orderings for Innermost Termination. In: Giesl J (ed.), Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings, volume 3467 of Lecture Notes in Computer Science. Springer, 2005 pp. 17–31. URL https://doi.org/ 10.1007/978-3-540-32033-3_3

    work page doi:10.1007/978-3-540-32033-3_3 2005

  10. [11]

    Estimation of Parallel Complexity with Rewriting Techniques

    Alias C, Fuhs C, Gonnord L. Estimation of Parallel Complexity with Rewriting Techniques. In: Proceedings of the 15th Workshop on Termination (WST 2016). 2016 pp. 2:1–2:5. URL https: //hal.archives-ouvertes.fr/hal-01345914

    work page 2016

  11. [12]

    Term Rewriting on GPUs

    van Eerd J, Groote JF, Hijma P, Martens J, Wijs A. Term Rewriting on GPUs. In: Hojjat H, Massink M (eds.), Fundamentals of Software Engineering - 9th International Conference, FSEN 2021, Virtual Event, May 19-21, 2021, Revised Selected Papers, volume 12818 of Lecture Notes in Computer Science. Springer, 2021 pp. 175–189. URL https://doi.org/10.1007/978-3-...

    work page doi:10.1007/978-3-030-89247-0_12 2021

  12. [13]

    Innermost many-sorted term rewriting on GPUs

    van Eerd J, Groote JF, Hijma P, Martens J, Osama M, Wijs A. Innermost many-sorted term rewriting on GPUs. Sci. Comput. Program., 2023. 225:102910. URL https://doi.org/10.1016/j.scico.2022. 102910

    work page doi:10.1016/j.scico.2022 2023

  13. [14]

    Analysing Parallel Complexity of Term Rewriting

    Baudon T, Fuhs C, Gonnord L. Analysing Parallel Complexity of Term Rewriting. In: Villanueva A (ed.), Logic-Based Program Synthesis and Transformation - 32nd International Symposium, LOPSTR 2022, Tbilisi, Georgia, September 21-23, 2022, Proceedings, volume 13474 ofLecture Notes in Computer Science. Springer, 2022 pp. 3–23. URL https://doi.org/10.1007/978-...

    work page doi:10.1007/978-3-031-16767-6_1 2022

  14. [15]

    Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs

    Noschinski L, Emmes F, Giesl J. Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs. J. Autom. Reason. , 2013. 51(1):27–56. URL https://doi.org/10.1007/ s10817-013-9277-6

    work page 2013

  15. [16]

    Canonical algebraic simplification in computational logic

    Lankford DS. Canonical algebraic simplification in computational logic. Technical Report ATP-25, University of Texas, 1975

    work page 1975

  16. [17]

    SAT Solving for Termination Analysis with Polynomial Interpretations

    Fuhs C, Giesl J, Middeldorp A, Schneider-Kamp P, Thiemann R, Zankl H. SAT Solving for Termination Analysis with Polynomial Interpretations. In: Marques-Silva J, Sakallah KA (eds.), Theory and Applications of Satisfiability Testing - SAT 2007, 10th International Conference, Lisbon, Portugal, May 28-31, 2007, Proceedings, volume 4501 of Lecture Notes in Com...

    work page doi:10.1007/978-3-540-72788-0_33 2007

  17. [18]

    SAT Modulo Linear Arithmetic for Solving Polynomial Constraints

    Borralleras C, Lucas S, Oliveras A, Rodr´ıguez-Carbonell E, Rubio A. SAT Modulo Linear Arithmetic for Solving Polynomial Constraints. J. Autom. Reason., 2012. 48(1):107–131. URL https://doi.org/10. 1007/s10817-010-9196-8 . T. Baudon et al. / On Complexity Bounds and Confluence of Parallel Term Rewriting 163

    work page 2012

  18. [19]

    Analyzing Program Termination and Complexity Automatically with AProVE

    Giesl J, Aschermann C, Brockschmidt M, Emmes F, Frohn F, Fuhs C, Hensel J, Otto C, Pl ¨ucker M, Schneider-Kamp P, Str¨oder T, Swiderski S, Thiemann R. Analyzing Program Termination and Complexity Automatically with AProVE. J. Autom. Reason., 2017. 58(1):3–31. Web interface and download: https:// aprove.informatik.rwth-aachen.de/, URL https://doi.org/10.10...

    work page doi:10.1007/s10817-016-9388-y 2017

  19. [20]

    TcT: Tyrolean Complexity Tool

    Avanzini M, Moser G, Schaper M. TcT: Tyrolean Complexity Tool. In: Chechik M, Raskin J (eds.), Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings...

    work page 2016

  20. [21]

    Term Rewriting with Logical Constraints

    Kop C, Nishida N. Term Rewriting with Logical Constraints. In: Fontaine P, Ringeissen C, Schmidt RA (eds.), Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Nancy, France, September 18-20, 2013. Proceedings, volume 8152 of Lecture Notes in Computer Science. Springer, 2013 pp. 343–358. URL https://doi.org/10.1007/978-3-642-40885-4_24

    work page doi:10.1007/978-3-642-40885-4_24 2013

  21. [22]

    Verifying Procedural Programs via Constrained Rewriting Induction

    Fuhs C, Kop C, Nishida N. Verifying Procedural Programs via Constrained Rewriting Induction. ACM Trans. Comput. Log., 2017. 18(2):14:1–14:50. URL https://doi.org/10.1145/3060143

    work page doi:10.1145/3060143 2017

  22. [23]

    Higher Order Termination

    Kop C. Higher Order Termination. Ph.D. thesis, VU Amsterdam, 2012

    work page 2012

  23. [24]

    Higher-Order LCTRSs and Their Termination

    Guo L, Kop C. Higher-Order LCTRSs and Their Termination. In: Weirich S (ed.), Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part II, volume 14577 of Lecture Note...

    work page doi:10.1007/978-3-031-57267-8_13 2024

  24. [25]

    Term rewriting and all that

    Baader F, Nipkow T. Term rewriting and all that. Cambridge Univ. Press, 1998. ISBN 978-0-521-45520-6

    work page 1998

  25. [26]

    Automated Complexity Analysis Based on the Dependency Pair Method

    Hirokawa N, Moser G. Automated Complexity Analysis Based on the Dependency Pair Method. In: Armando A, Baumgartner P, Dowek G (eds.), Automated Reasoning, 4th International Joint Conference, IJ- CAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, volume 5195 ofLecture Notes in Computer Science. Springer, 2008 pp. 364–379. URL https://doi.org/10....

    work page doi:10.1007/978-3-540-71070-7_32 2008

  26. [27]

    Automated Complexity Analysis Based on Context-Sensitive Rewriting

    Hirokawa N, Moser G. Automated Complexity Analysis Based on Context-Sensitive Rewriting. In: Dowek G (ed.), Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8560 of Lecture Notes in Computer Science . Springer, 20...

    work page doi:10.1007/978-3-319-08918-8_18 2014

  27. [28]

    A combination framework for complexity

    Avanzini M, Moser G. A combination framework for complexity. Information and Computation, 2016. 248:22–55. URL https://doi.org/10.1016/j.ic.2015.12.007

    work page doi:10.1016/j.ic.2015.12.007 2016

  28. [29]

    Complexity Analysis for Term Rewriting by Integer Transition Systems

    Naaf M, Frohn F, Brockschmidt M, Fuhs C, Giesl J. Complexity Analysis for Term Rewriting by Integer Transition Systems. In: Dixon C, Finger M (eds.), Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Bras ´ılia, Brazil, September 27-29, 2017, Proceedings, volume 10483 of Lecture Notes in Computer Science. Springer, 2017 pp. 132–1...

    work page 2017

  29. [30]

    Lower Bounds for Runtime Complexity of Term Rewriting

    Frohn F, Giesl J, Hensel J, Aschermann C, Str ¨oder T. Lower Bounds for Runtime Complexity of Term Rewriting. J. Autom. Reason. , 2017. 59(1):121–163. URL https://doi.org/10.1007/ s10817-016-9397-x . 164 T. Baudon et al. / On Complexity Bounds and Confluence of Parallel Term Rewriting

    work page 2017

  30. [31]

    Automated amortised resource analysis for term rewrite systems

    Moser G, Schneckenreither M. Automated amortised resource analysis for term rewrite systems. Sci. Comput. Program., 2020. 185. URL https://doi.org/10.1016/j.scico.2019.102306

    work page doi:10.1016/j.scico.2019.102306 2020

  31. [32]

    Termination of Term Rewriting Using Dependency Pairs

    Arts T, Giesl J. Termination of Term Rewriting Using Dependency Pairs. Theoretical Computer Science,

    work page

  32. [33]

    Testing Positiveness of Polynomials

    Hong H, Jakus D. Testing Positiveness of Polynomials. J. Autom. Reason., 1998. 21(1):23–38. URL https://doi.org/10.1023/A:1005983105493

    work page doi:10.1023/a:1005983105493 1998

  33. [34]

    Parallelism in Sequential Functional Languages

    Blelloch GE, Greiner J. Parallelism in Sequential Functional Languages. In: Williams J (ed.), Proceedings of the seventh international conference on Functional programming languages and computer architecture, FPCA 1995, La Jolla, California, USA, June 25-28, 1995. ACM, 1995 pp. 226–237. URL https: //doi.org/10.1145/224164.224210

    work page doi:10.1145/224164.224210 1995

  34. [35]

    Loops under Strategies

    Thiemann R, Sternagel C, Giesl J, Schneider-Kamp P. Loops under Strategies ... Continued. In: Kirchner H, Mu ˜noz CA (eds.), Proceedings International Workshop on Strategies in Rewriting, Proving, and Programming, IWS 2010, Edinburgh, UK, 9th July 2010, volume 44 of EPTCS. 2010 pp. 51–65. URL https://doi.org/10.4204/EPTCS.44.4

    work page doi:10.4204/eptcs.44.4 2010

  35. [36]

    Remarks on the full parallel innermost strategy, 2023

    van Oostrom V . Remarks on the full parallel innermost strategy, 2023. URLhttp://www.javakade.nl/ research/pdf/fpi.pdf

    work page 2023

  36. [37]

    Maximal Termination

    Fuhs C, Giesl J, Middeldorp A, Schneider-Kamp P, Thiemann R, Zankl H. Maximal Termination. In: V oronkov A (ed.), Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings, volume 5117 of Lecture Notes in Computer Science. Springer, 2008 pp. 110–125. URL https://doi.org/10.1007/978-3-...

    work page doi:10.1007/978-3-540-70590-1_8 2008

  37. [38]

    Communications of the ACM 21(7), pp

    Lamport L. Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM, 1978. 21(7):558–565. URL https://doi.org/10.1145/359545.359563

    work page doi:10.1145/359545.359563 1978

  38. [39]

    Termination Problems DataBase (TPDB)

    Wiki. Termination Problems DataBase (TPDB). http://termination-portal.org/wiki/TPDB

    work page

  39. [40]

    The Termination and Complexity Competition

    Giesl J, Rubio A, Sternagel C, Waldmann J, Yamada A. The Termination and Complexity Competition. In: Beyer D, Huisman M, Kordon F, Steffen B (eds.), Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III, volume 11429 of ...

    work page doi:10.1007/978-3-030-17502-3_10 2019

  40. [41]

    The International Termination Competition (TermComp)

    Wiki. The International Termination Competition (TermComp). http://termination-portal.org/ wiki/Termination_Competition

    work page

  41. [42]

    Context-sensitive Rewriting

    Lucas S. Context-sensitive Rewriting. ACM Comput. Surv., 2021. 53(4):78:1–78:36. URL https: //doi.org/10.1145/3397677

    work page doi:10.1145/3397677 2021

  42. [43]

    Resource Analysis of Complex Programs with Cost Equations

    Flores-Montoya A, H¨ahnle R. Resource Analysis of Complex Programs with Cost Equations. In: Garrigue J (ed.), Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Proceedings, volume 8858 of Lecture Notes in Computer Science. Springer, 2014 pp. 275–295. URL https://doi.org/10.1007/978-3-319-12736-1_15

    work page doi:10.1007/978-3-319-12736-1_15 2014

  43. [44]

    Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations

    Flores-Montoya A. Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations. In: Fitzgerald JS, Heitmeyer CL, Gnesi S, Philippou A (eds.), FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings, volume 9995 of Lecture Notes in Computer Science. 2016 pp. 254–273. URL https://doi.org/10...

    work page doi:10.1007/978-3-319-48989-6_16 2016

  44. [45]

    Type introduction for runtime complexity analysis

    Avanzini M, Felgenhauer B. Type introduction for runtime complexity analysis. In: WST ’14. 2014 pp. 1–5. Available from http://www.easychair.org/smart-program/VSL2014/WST-proceedings.pdf. T. Baudon et al. / On Complexity Bounds and Confluence of Parallel Term Rewriting 165

    work page 2014

  45. [46]

    Simple Word Problems in Universal Algebras

    Knuth DE, Bendix PB. Simple Word Problems in Universal Algebras. In: Leech J (ed.), Computational Problems in Abstract Algebra. Pergamon Press, 1970 pp. 263–297

    work page 1970

  46. [47]

    Tree-Manipulating Systems and Church-Rosser Theorems

    Rosen BK. Tree-Manipulating Systems and Church-Rosser Theorems. J. ACM, 1973. 20(1):160–187. URL https://doi.org/10.1145/321738.321750

    work page doi:10.1145/321738.321750 1973

  47. [48]

    Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems

    Huet GP. Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems. J. ACM, 1980. 27(4):797–821. URL https://doi.org/10.1145/322217.322230

    work page doi:10.1145/322217.322230 1980

  48. [49]

    The International Confluence Competition (CoCo)

    Community. The International Confluence Competition (CoCo). http://project-coco.uibk.ac.at/

    work page

  49. [50]

    On Confluence of Parallel-Innermost Term Rewriting

    Baudon T, Fuhs C, Gonnord L. On Confluence of Parallel-Innermost Term Rewriting. In: Winkler S, Rocha C (eds.), Proceedings of the 11th International Workshop on Confluence. 2022 pp. 31–36. URL http://cl-informatik.uibk.ac.at/iwc/2022/proceedings.pdf

    work page 2022

  50. [51]

    Termination and confluence: properties of structured rewrite systems

    Gramlich B. Termination and confluence: properties of structured rewrite systems. Ph.D. thesis, Kaiser- slautern University of Technology, Germany, 1996. URL https://d-nb.info/949807389

    work page arXiv 1996

  51. [52]

    StarExec: A Cross-Community Infrastructure for Logic Solving

    Stump A, Sutcliffe G, Tinelli C. StarExec: A Cross-Community Infrastructure for Logic Solving. In: Demri S, Kapur D, Weidenbach C (eds.), Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22,

    work page 2014

  52. [53]

    Springer, 2014 pp

    Proceedings, volume 8562 of Lecture Notes in Computer Science . Springer, 2014 pp. 367–373. https://www.starexec.org/, URL https://doi.org/10.1007/978-3-319-08587-6_28

    work page doi:10.1007/978-3-319-08587-6_28 2014

  53. [54]

    URL https://www.dcs.bbk.ac.uk/~carsten/eval/parallel_complexity_journal/

    work page

  54. [55]

    URL https://www

    TCT, version from the Termination and Complexity Competitions 2020 – 2022. URL https://www. starexec.org/starexec/secure/details/solver.jsp?id=29575

    work page 2020

  55. [56]

    Cops and CoCoWeb: Infrastructure for Confluence Tools

    Hirokawa N, Nagele J, Middeldorp A. Cops and CoCoWeb: Infrastructure for Confluence Tools. In: Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, volume 10900 of LNCS. Springer, 2018 pp. 346–353. See also: https://cops.uibk.ac.at/, URL ...

    work page 2018

  56. [57]

    Task-level analysis for a language with async/finish parallelism

    Albert E, Arenas P, Genaim S, Zanardini D. Task-level analysis for a language with async/finish parallelism. In: Vitek J, Sutter BD (eds.), Proceedings of the ACM SIGPLAN/SIGBED 2011 conference on Languages, compilers, and tools for embedded systems, LCTES 2011, Chicago, IL, USA, April 11-14, 2011. ACM, 2011 pp. 21–30. URL https://doi.org/10.1145/1967677.1967681

    work page doi:10.1145/1967677.1967681 2011

  57. [58]

    Cost analysis of object-oriented bytecode programs

    Albert E, Arenas P, Genaim S, Puebla G, Zanardini D. Cost analysis of object-oriented bytecode programs. Theor. Comput. Sci., 2012. 413(1):142–159. URL https://doi.org/10.1016/j.tcs.2011.07.009

    work page doi:10.1016/j.tcs.2011.07.009 2012

  58. [59]

    Resource Aware ML

    Hoffmann J, Aehlig K, Hofmann M. Resource Aware ML. In: Madhusudan P, Seshia SA (eds.), Computer Aided Verification - 24th International Conference, CA V 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, volume 7358 of Lecture Notes in Computer Science . Springer, 2012 pp. 781–786. URL https://doi.org/10.1007/978-3-642-31424-7_64

    work page doi:10.1007/978-3-642-31424-7_64 2012

  59. [60]

    Runtime Complexity Analysis of Logically Constrained Rewriting

    Winkler S, Moser G. Runtime Complexity Analysis of Logically Constrained Rewriting. In: Fern ´andez M (ed.), Logic-Based Program Synthesis and Transformation - 30th International Symposium, LOPSTR 2020, Bologna, Italy, September 7-9, 2020, Proceedings, volume 12561 of Lecture Notes in Computer Science. Springer, 2020 pp. 37–55. URL https://doi.org/10.1007...

    work page doi:10.1007/978-3-030-68446-4_2 2020

  60. [61]

    Termination Proofs and the Length of Derivations

    Hofbauer D, Lautemann C. Termination Proofs and the Length of Derivations. In: Dershowitz N (ed.), Rewriting Techniques and Applications, 3rd International Conference, RTA-89, Chapel Hill, North Carolina, USA, April 3-5, 1989, Proceedings, volume 355 of Lecture Notes in Computer Science. Springer, 1989 pp. 167–177. URL https://doi.org/10.1007/3-540-51081-8_107

    work page doi:10.1007/3-540-51081-8_107 1989

  61. [62]

    Compositional Confluence Criteria

    Shintani K, Hirokawa N. Compositional Confluence Criteria. In: Felty AP (ed.), 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022, August 2-5, 2022, Haifa, Israel, volume 228 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum f¨ur Informatik, 2022 pp. 28:1–28:19. URL https://doi.org/10.4230/LIPIcs.FSCD.2022.28

    work page doi:10.4230/lipics.fscd.2022.28 2022

  62. [63]

    Compositional Confluence Criteria

    Shintani K, Hirokawa N. Compositional Confluence Criteria. Log. Methods Comput. Sci., 2024. 20(1)

    work page 2024

  63. [64]

    Confluence Framework: Proving Confluence with CONFident

    Guti´errez R, V´ıtores M, Lucas S. Confluence Framework: Proving Confluence with CONFident. In: Vil- lanueva A (ed.), Logic-Based Program Synthesis and Transformation - 32nd International Symposium, LOP- STR 2022, Tbilisi, Georgia, September 21-23, 2022, Proceedings, volume 13474 of Lecture Notes in Com- puter Science. Springer, 2022 pp. 24–43. URL https:...

    work page doi:10.1007/978-3-031-16767-6_2 2022

  64. [65]

    Locally maximal common factors as a tool for efficient dynamic string algorithms

    Contejean E, Courtieu P, Forest J, Pons O, Urbain X. Automated Certified Proofs with CiME3. In: Schmidt-Schauß M (ed.), Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, May 30 - June 1, 2011, Novi Sad, Serbia, volume 10 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum f¨ur Informatik, 2011 pp. 21–30. URL ht...

    work page doi:10.4230/lipics 2011

  65. [66]

    CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates

    Blanqui F, Koprowski A. CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comput. Sci., 2011. 21(4):827–859. URL https://doi.org/10.1017/S0960129511000120

    work page doi:10.1017/s0960129511000120 2011

  66. [67]

    Certification of Termination Proofs Using CeTA

    Thiemann R, Sternagel C. Certification of Termination Proofs Using CeTA. In: Berghofer S, Nipkow T, Ur- ban C, Wenzel M (eds.), Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 ofLecture Notes in Computer Science. Springer, 2009 pp. 452–468. URL https://doi.or...

    work page doi:10.1007/978-3-642-03359-9_31 2009

  67. [68]

    Certifying Higher-Order Polynomial Interpretations

    van der Weide N, Vale D, Kop C. Certifying Higher-Order Polynomial Interpretations. In: Naumowicz A, Thiemann R (eds.), 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, volume 268 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum f ¨ur Informatik, 2023 pp. 30:1–30:20. URL https://doi.org/10....

    work page doi:10.4230/lipics.itp.2023.30 2023