# Publications on Infinitary rewriting

## 2018

- Coinductive Foundations of Infinitary Rewriting and Infinitary Equational LogicJörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra SilvaLogical Methods in Computer Science , 14 (1) (2018)paper
# Summary

We present a coinductive framework for defining and reasoning about the infinitary analogues of equational logic and term rewriting in a uniform, coinductive way.

The framework lends itself to an elegant and concise definition of the infinitary rewrite relation \( \to^\infty \) in terms of the single step relation \( \to \): \[ {\to^\infty} \,=\, \mu R. \nu S. ( \to \cup \mathrel{\overline{R}} )^* \mathrel{;} \overline{S} \] Here \( \mu \) and \( \nu \) are the least and greatest fixed-point operators, respectively, and \[ \overline{R} \,=\, \{\, (\, f(s_1,\ldots,s_n),\, \,f(t_1,\ldots,t_n) \,) \mid f \in \Sigma,\, s_1\! \mathrel{R} t_1,\ldots,s_n\! \mathrel{R} t_n \,\} \cup \text{Id} \] 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 suitable for formalizations in theorem provers. To wit, we provide the first formalization of the compression lemma in Coq.

This paper is an extended version of A Coinductive Framework for Infinitary Rewriting and Equational Reasoning (RTA 2015). We build on ideas in Infinitary Rewriting Coinductively (TYPES 2012) giving a coinductive perspective on infinitary lambda calculus. We extend these ideas to rewrite sequences beyond length omega by mixing induction and coinduction (least and greatest fixed-points).

# Bibtex

@article{infintary:rewriting:coinductive:2018, author = {Endrullis, J\"{o}rg and Hansen, Helle Hvid and Hendriks, Dimitri and Polonsky, Andrew and Silva, Alexandra}, title = {{Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic}}, journal = {Logical Methods in Computer Science}, volume = {14}, number = {1}, year = {2018}, doi = {10.23638/LMCS-14(1:3)2018}, keywords = {rewriting, infinitary rewriting, coinduction}, type = {journal} }

# Digital Object Identifier

10.23638/LMCS-14(1:3)2018

## 2017

- Clocked Lambda CalculusJörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew PolonskyMathematical Structures in Computer Science , 27 (5) , pp. 782–806 (2017)paper
# Summary

We introduce the

*clocked lambda calculus*, an extension of the classical lambda calculus with a unary symbol \( \tau \) that serves as a witness of \( \beta \)-steps. This calculus consists of the following two rules: \[ \begin{aligned} (\lambda x.M) N &\to \tau( M[x = N] ) \\ \tau(M)N &\to \tau(MN) \end{aligned} \] The clocked lambda-calculus is infinitary strongly normalizing, infinitary confluent, and the unique infinitary normal forms constitute enriched Böhm trees (more precisely, Lévy-Longo trees), which we call*clocked Böhm trees*. We show that clocked Böhm trees are suitable for discriminating a rich class of lambda terms having the same Böhm trees.See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.

# Bibtex

@article{clocked:lambda:calculus:2017, author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem and Polonsky, Andrew}, title = {{Clocked Lambda Calculus}}, journal = {Mathematical Structures in Computer Science}, volume = {27}, number = {5}, pages = {782--806}, year = {2017}, doi = {10.1017/S0960129515000389}, keywords = {rewriting, infinitary rewriting, lambda calculus}, type = {journal} }

# Digital Object Identifier

10.1017/S0960129515000389

## 2015

- A Coinductive Framework for Infinitary Rewriting and Equational ReasoningJörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra SilvaIn: Proc. Conf. on Rewriting Techniques and Applications (RTA 2015), pp. 143–159, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)paper
# Summary

We present a coinductive framework for defining and reasoning about the infinitary analogues of equational logic and term rewriting in a uniform, coinductive way.

The framework lends itself to an elegant and concise definition of the infinitary rewrite relation \( \to^\infty \) in terms of the single step relation \( \to \): \[ {\to^\infty} \,=\, \mu R. \nu S. ( \to \cup \mathrel{\overline{R}} )^* \mathrel{;} \overline{S} \] Here \( \mu \) and \( \nu \) are the least and greatest fixed-point operators, respectively, and \[ \overline{R} \,=\, \{\, (\, f(s_1,\ldots,s_n),\, \,f(t_1,\ldots,t_n) \,) \mid f \in \Sigma,\, s_1\! \mathrel{R} t_1,\ldots,s_n\! \mathrel{R} t_n \,\} \cup \text{Id} \] 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 suitable for formalizations in theorem provers.

We refer to Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic (LMCS 2018) for an extended journal version of this paper.

We build on ideas in Infinitary Rewriting Coinductively (TYPES 2012) giving a coinductive perspective on infinitary lambda calculus. We extend these ideas to rewrite sequences beyond length omega by mixing induction and coinduction (least and greatest fixed-points).

# Bibtex

@inproceedings{infintary:rewriting:coinductive:2015, author = {Endrullis, J\"{o}rg and Hansen, Helle Hvid and Hendriks, Dimitri and Polonsky, Andrew and Silva, Alexandra}, title = {{A Coinductive Framework for Infinitary Rewriting and Equational Reasoning}}, booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA 2015)}, volume = {36}, pages = {143--159}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}, series = {LIPIcs}, year = {2015}, doi = {10.4230/LIPIcs.RTA.2015.143}, keywords = {rewriting, infinitary rewriting, coinduction}, type = {conference} }

# Digital Object Identifier

10.4230/LIPIcs.RTA.2015.143

## 2014

- Discriminating Lambda-Terms Using Clocked Boehm TreesJörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew PolonskyLogical Methods in Computer Science , 10 (2) (2014)paper
# Summary

As observed by Intrigila, there are hardly techniques available in the lambda calculus to prove that two lambda terms are not \( \beta \)-convertible. Techniques employing the usual Böhm trees are inadequate when we deal with terms having the same Böhm tree. This is the case in particular for fixed-point combinators, as they all have the same Böhm tree.

Another interesting equation, whose consideration was suggested by Scott, is BY = BYS, an equation valid in the classical model \( P \omega \) of lambda calculus, and hence valid with respect to Böhm tree-equality, but nevertheless the terms are \( \beta \)-inconvertible.

To prove such beta-inconvertibilities, we refine the concept of Böhm trees: we introduce

*clocked Böhm trees's*with annotations that convey information of the tempo in which the Böhm trees are produced. Böhm trees are thus enriched with an intrinsic clock behaviour, leading to a refined discrimination method for lambda terms. An analogous approach pertains to Levy-Longo trees and Berarducci trees.We illustrate applicability of our refined Böhm trees at the following examples:

- We show how to \( \beta \)-discriminate a large number of fixed-point combinators.
- We answer a question of Gordon Plotkin:
*Is there a fixed point combinator \( Y \) such that \[ Y ( \lambda z. f zz ) =_\beta Y ( \lambda x. Y ( \lambda y. f xy )) \]*

*atomic clocks*.This paper is an extended version of

*Modular Construction of Fixed Point Combinators and Clocked Böhm Trees*(LICS 2010).See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.

# Bibtex

@article{lambda:clocks:2014, author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem and Polonsky, Andrew}, title = {{Discriminating Lambda-Terms Using Clocked Boehm Trees}}, journal = {Logical Methods in Computer Science}, volume = {10}, number = {2}, year = {2014}, doi = {10.2168/LMCS-10(2:4)2014}, keywords = {rewriting, infinitary rewriting, lambda calculus}, type = {journal} }

# Digital Object Identifier

10.2168/LMCS-10(2:4)2014

- Infinitary Term Rewriting for Weakly Orthogonal Systems: Properties and CounterexamplesJörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, and Vincent van OostromLogical Methods in Computer Science , 10 (2:7) , pp. 1–33 (2014)paper
# Bibtex

@article{infinitary:weakly:orthogonal:2014, author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri and Klop, Jan Willem and van~Oostrom, Vincent}, title = {{Infinitary Term Rewriting for Weakly Orthogonal Systems: Properties and Counterexamples}}, journal = {Logical Methods in Computer Science}, volume = {10}, number = {2:7}, pages = {1--33}, year = {2014}, doi = {10.2168/LMCS-10(2:7)2014}, keywords = {rewriting, infinitary rewriting, lambda calculus}, type = {journal} }

# Digital Object Identifier

10.2168/LMCS-10(2:7)2014

## 2013

- Clocks for Functional ProgramsJörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew PolonskyIn: The Beauty of Functional Code - Essays Dedicated to Rinus Plasmeijer on the Occasion of His 61st Birthday, pp. 97–126, Springer (2013)paper
# Summary

The contribution of this paper is twofold.

First, we derive a complete characterization of all

*simply-typed***fixed-point combinator (fpc) generators**using*Barendregt's Inhabitation Machines*. A fpc generator is a lambda term \( G \) such that \( Y G \) is a fpc whenever \( Y \) is. The term \( \delta = \lambda xy. y(xy) \), also known as Smullyan's Owl, is a famous fpc generator. For instance, Turing's fpc \( Y_1 \) can be obtaind from Curry's fpc \( Y_0 \) by postfixing \( \delta \): \[ Y_1 = Y_0 \delta \]Second, we present a conjecture that vastly generalises Richard Statman's question on the existance of double fixed-point combinators. Statman asked whether there is a fixed-point combinator \( Y \) such that \( Y =_\beta Y \delta \). This question remains open as the proof by Benedetto Intrigila contains a gap. We have the following conjecture about the relation of the \( \mu \)-opertator and fixed-point combinators:

ConjectureWe conjecture that for any fixed-point combinator \( Y \) and simply-typed \( \lambda\mu \)-terms \( s,t \) it holds that \[ s =_{ \beta \mu } t \iff s_Y =_{ \beta } t_Y \] where \(s_Y, t_Y\) are the*untyped*lambda terms obtained from \(s,t\), respectively, by replacing all occurrences of \( \mu \)-operators with the fixed-point combinator \( Y \).See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.

# Bibtex

@inproceedings{lambda:clocks:functional:programs:2013, author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem and Polonsky, Andrew}, title = {{Clocks for Functional Programs}}, booktitle = {The Beauty of Functional Code - Essays Dedicated to Rinus Plasmeijer on the Occasion of His 61st Birthday}, pages = {97--126}, year = {2013}, doi = {10.1007/978-3-642-40355-2\_8}, series = {LNCS}, volume = {8106}, publisher = {Springer}, keywords = {rewriting, infinitary rewriting, lambda calculus}, type = {journal} }

# Digital Object Identifier

10.1007/978-3-642-40355-2_8

## 2012

- Highlights in Infinitary Rewriting and Lambda CalculusJörg Endrullis, Dimitri Hendriks, and Jan Willem KlopTheoretical Computer Science , 464 , pp. 48–71 (2012)paper
# Bibtex

@article{infinitary:highlights:2012, author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem}, title = {{Highlights in Infinitary Rewriting and Lambda Calculus}}, journal = {Theoretical Computer Science}, volume = {464}, pages = {48--71}, year = {2012}, doi = {10.1016/j.tcs.2012.08.018}, keywords = {rewriting, infinitary rewriting, lambda calculus}, type = {journal} }

# Digital Object Identifier

10.1016/j.tcs.2012.08.018

## 2011

- Lazy Productivity via TerminationJörg Endrullis, and Dimitri HendriksTheoretical Computer Science , 412 (28) , pp. 3203–3225 (2011)paper
# Bibtex

@article{productivity:termination:2011, author = {Endrullis, J\"{o}rg and Hendriks, Dimitri}, title = {{Lazy Productivity via Termination}}, journal = {Theoretical Computer Science}, volume = {412}, number = {28}, pages = {3203--3225}, year = {2011}, doi = {10.1016/j.tcs.2011.03.024}, keywords = {rewriting, infinitary rewriting, productivity, termination}, type = {journal} }

# Digital Object Identifier

10.1016/j.tcs.2011.03.024

- Proving Equality of Streams AutomaticallyHans Zantema, and Jörg EndrullisIn: Proc. Conf. on Rewriting Techniques and Applications (RTA 2011), pp. 393–408, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)paper
# Bibtex

@inproceedings{streams:equality:2011, author = {Zantema, Hans and Endrullis, J\"{o}rg}, title = {{Proving Equality of Streams Automatically}}, booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2011)}, volume = {10}, pages = {393--408}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}, series = {LIPIcs}, year = {2011}, doi = {10.4230/LIPIcs.RTA.2011.393}, keywords = {rewriting, infinitary rewriting, streams}, type = {conference} }

# Digital Object Identifier

10.4230/LIPIcs.RTA.2011.393

- Infinitary Rewriting CoinductivelyJörg Endrullis, and Andrew PolonskyIn: Proc. Conf. on Types for Proofs and Programs (TYPES 2012), pp. 16–27, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)paper
# Summary

We provide a coinductive definition of strongly convergent reductions between infinite lambda terms. This approach avoids the notions of ordinals and metric convergence which have appeared in the earlier definitions of the concept. As an illustration, we prove the existence part of the infinitary standardization theorem. The proof is fully formalized in Coq using coinductive types.

The paper concludes with a characterization of infinite lambda terms which reduce to themselves in a single beta step.

The papers

extend the idea in this paper to reductions of length beyond omega.The extension to reduction lengths beyond omega requires mixing of induction and coinduction. Therefore the simpler setup presented in the current paper (

*Infinitary Rewriting Coinductively*) is preferrable whenever there is no need for reductions longer than omega. This concerns for instance rewrite systems having the compression property, such as lambda calculus and left-linear term rewriting systems (with finite left-hand sides).# Bibtex

@inproceedings{infintary:lambda:coinductive:2011, author = {Endrullis, J\"{o}rg and Polonsky, Andrew}, title = {{Infinitary Rewriting Coinductively}}, booktitle = {Proc.\ Conf.\ on Types for Proofs and Programs (TYPES~2012)}, volume = {19}, pages = {16--27}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}, series = {LIPIcs}, year = {2011}, doi = {10.4230/LIPIcs.TYPES.2011.16}, keywords = {rewriting, infinitary rewriting, coinduction}, type = {conference} }

# Digital Object Identifier

10.4230/LIPIcs.TYPES.2011.16

## 2010

- Productivity of Stream DefinitionsJörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Ariya Isihara, and Jan Willem KlopTheoretical Computer Science , 411 (4-5) , pp. 765–782 (2010)paper
# Summary

We give an algorithm for deciding productivity of a large and natural class of recursive stream definitions. A stream definition is called `productive' if it can be evaluated continually in such a way that a uniquely determined stream in constructor normal form is obtained as the limit. Whereas productivity is undecidable for stream definitions in general, we show that it can be decided for `pure' stream definitions. For every pure stream definition the process of its evaluation can be modelled by the dataflow of abstract stream elements, called `pebbles', in a finite `pebbleflow net(work)'. And the production of a pebbleflow net associated with a pure stream definition, that is, the amount of pebbles the net is able to produce at its output port, can be calculated by reducing nets to trivial nets.

This paper is an extended version of Productivity of Stream Definitions (2007) (FCT 2007).

See research for an overview of my research on productivity.

# Bibtex

@article{productivity:streams:2010, author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri and Isihara, Ariya and Klop, Jan Willem}, title = {{Productivity of Stream Definitions}}, journal = {Theoretical Computer Science}, volume = {411}, number = {4-5}, pages = {765--782}, year = {2010}, doi = {10.1016/j.tcs.2009.10.014}, keywords = {rewriting, infinitary rewriting, productivity}, type = {journal} }

# Digital Object Identifier

10.1016/j.tcs.2009.10.014

- Modular Construction of Fixed Point Combinators and Clocked Böhm TreesJörg Endrullis, Dimitri Hendriks, and Jan Willem KlopIn: Proc. Symp. on Logic in Computer Science (LICS 2010), pp. 111–119, IEEE Computer Society (2010)paper
# Summary

One of the best-known methods for discriminating lambda terms with respect to \( \beta \)-convertibility is due to Corrado Böhm. Roughly speaking, the

*Böhm tree*of a lambda term is its infinite normal form. If lambda terms have distinct Böhm trees, then they are not \( \beta \)-convertible. But what if their Böhm trees coincide? For example, all fixed-point combinators have the same Böhm tree, namely \[ \lambda x. x(x(x(\ldots))) \]We refine Böhm trees with a

*clock*that records how many head reduction steps have been used to rewrite each subterm to head normal form. We show that*clocked Böhm trees*are suitable for discriminating a rich class of lambda terms (in particular many fixed-point combinators) having the same Böhm trees.We refer to

*Discriminating Lambda-Terms Using Clocked Boehm Trees*(LMCS 2014) for an extended journal version of this paper. In the extended version we improve the precision of the clocks to*atomic clocks*and we answer a question of Gordon Plotkin, showing that the method can be used beyond simple terms.# Bibtex

@inproceedings{lambda:clocks:2010, author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem}, title = {{Modular Construction of Fixed Point Combinators and Clocked B\"{o}hm Trees}}, booktitle = {Proc.\ Symp.\ on Logic in Computer Science (LICS~2010)}, pages = {111--119}, publisher = {{IEEE} Computer Society}, year = {2010}, doi = {10.1109/LICS.2010.8}, keywords = {rewriting, infinitary rewriting, lambda calculus}, type = {conference} }

# Digital Object Identifier

10.1109/LICS.2010.8

- Unique Normal Forms in Infinitary Weakly Orthogonal RewritingJörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, and Vincent van OostromIn: Proc. Conf. on Rewriting Techniques and Applications (RTA 2010), pp. 85–102, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2010)paper
# Bibtex

@inproceedings{infinitary:weakly:orthogonal:unique:normal:forms:2010, author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri and Klop, Jan Willem and van~Oostrom, Vincent}, title = {{Unique Normal Forms in Infinitary Weakly Orthogonal Rewriting}}, booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2010)}, volume = {6}, pages = {85--102}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}, series = {LIPIcs}, year = {2010}, doi = {10.4230/LIPIcs.RTA.2010.85}, keywords = {rewriting, infinitary rewriting, lambda calculus}, type = {conference} }

# Digital Object Identifier

10.4230/LIPIcs.RTA.2010.85

## 2008

- Data-Oblivious Stream ProductivityJörg Endrullis, Clemens Grabmayer, and Dimitri HendriksIn: Proc. Conf. on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2008), pp. 79–96, Springer (2008)paper
# Summary

We are concerned with demonstrating productivity of specifications of infinite streams of data, based on orthogonal rewrite rules. In general, this property is undecidable, but for restricted formats computable sufficient conditions can be obtained. The usual analysis, also adopted here, disregards the identity of data, thus leading to approaches that we call data-oblivious. We present a method that is provably optimal among all such data-oblivious approaches. This means that in order to improve on our algorithm one has to proceed in a data-aware fashion.

See research for an overview of my research on productivity.

# Bibtex

@inproceedings{productivity:data:oblivious:2008, author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri}, title = {{Data-Oblivious Stream Productivity}}, booktitle = {Proc.\ Conf.\ on Logic for Programming Artificial Intelligence and Reasoning (LPAR~2008)}, number = {5330}, pages = {79--96}, publisher = {Springer}, series = {LNCS}, year = {2008}, doi = {10.1007/978-3-540-89439-1\_6}, keywords = {rewriting, infinitary rewriting, productivity}, type = {conference} }

# Digital Object Identifier

10.1007/978-3-540-89439-1_6

- Proving Infinitary NormalizationJörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, and Roel C. de VrijerIn: Proc. Conf. on Types for Proofs and Programs (TYPES 2008), pp. 64–82, Springer (2008)paper
# Bibtex

@inproceedings{infinitary:normalization:2009, author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri and Klop, Jan Willem and de~Vrijer, Roel C.}, title = {{Proving Infinitary Normalization}}, booktitle = {Proc.\ Conf.\ on Types for Proofs and Programs (TYPES~2008)}, volume = {5497}, pages = {64--82}, publisher = {Springer}, series = {LNCS}, year = {2008}, doi = {10.1007/978-3-642-02444-3\_5}, keywords = {rewriting, infinitary rewriting, automata}, type = {conference} }

# Digital Object Identifier

10.1007/978-3-642-02444-3_5

## 2007

- Productivity of Stream DefinitionsJörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Ariya Isihara, and Jan Willem KlopIn: Proc. Symp. on Fundamentals of Computation Theory (FCT 2007), pp. 274–287, Springer (2007)paper
# Summary

We give an algorithm for deciding productivity of a large and natural class of recursive stream definitions. A stream definition is called `productive' if it can be evaluated continually in such a way that a uniquely determined stream in constructor normal form is obtained as the limit. Whereas productivity is undecidable for stream definitions in general, we show that it can be decided for `pure' stream definitions. For every pure stream definition the process of its evaluation can be modelled by the dataflow of abstract stream elements, called `pebbles', in a finite `pebbleflow net(work)'. And the production of a pebbleflow net associated with a pure stream definition, that is, the amount of pebbles the net is able to produce at its output port, can be calculated by reducing nets to trivial nets.

An extended journal version of this paper is available from Productivity of Stream Definitions (TCS 2010).

See research for an overview of my research on productivity.

# Bibtex

@inproceedings{productivity:streams:2007, author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri and Isihara, Ariya and Klop, Jan Willem}, title = {{Productivity of Stream Definitions}}, booktitle = {Proc.\ Symp.\ on Fundamentals of Computation Theory (FCT~2007)}, number = {4639}, pages = {274--287}, publisher = {Springer}, series = {LNCS}, year = {2007}, doi = {10.1007/978-3-540-74240-1\_24}, keywords = {rewriting, infinitary rewriting, productivity}, type = {conference} }

# Digital Object Identifier

10.1007/978-3-540-74240-1_24

- Root Stabilisation Using Dependency PairsJörg Endrullis, and Jeroen KetemaIn: Proc. Workshop on Termination (WST 2007), pp. 17–21 (2007)paper
# Bibtex

@inproceedings{termination:root:2007, author = {Endrullis, J\"{o}rg and Ketema, Jeroen}, title = {{Root Stabilisation Using Dependency Pairs}}, booktitle = {Proc.\ Workshop on Termination (WST~2007)}, pages = {17--21}, year = {2007}, keywords = {rewriting, infinitary rewriting, termination}, type = {workshop} }