RTA
2010
Springer
13 years 8 months ago
2010
Springer
Data words and data trees appear in verification and XML processing. The term “data” means that positions of the word, or tree, are decorated with elements of an infinite set...
RTA
2010
Springer
13 years 8 months ago
2010
Springer
We revisit (un)soundness of transformations of conditional into unconditional rewrite systems. The focus here is on so-called unravelings, the most simple and natural kind of such ...
RTA
2010
Springer
13 years 8 months ago
2010
Springer
This paper shows the equivalence of applicative similarity and contextual approximation, and hence also of bisimilarity and contextual equivalence, in the deterministic call-by-nee...
RTA
2010
Springer
13 years 8 months ago
2010
Springer
We describe performance enhancements that have been added to mkbTT, a modern completion tool combining multi-completion with the use of termination tools.
RTA
2010
Springer
13 years 8 months ago
2010
Springer
For a general class of infinite data structures including streams, binary trees, and the combination of finite and infinite lists, we investigate a notion of productivity. This ...
RTA
2010
Springer
13 years 8 months ago
2010
Springer
Abstract. We extend first-order order-sorted unification by permitting regular expression sorts for variables and in the domains of function symbols. The set of basic sorts is ...
RTA
2010
Springer
13 years 8 months ago
2010
Springer
RTA
2010
Springer
13 years 8 months ago
2010
Springer
The K framework, based on rewriting logic semantics, provides a powerful logic for defining the semantics of programming languages. While most work in this area has focused on de...
RTA
2010
Springer
13 years 8 months ago
2010
Springer
Abstract. In this paper we present our formalization of two important termination techniques for term rewrite systems: the subterm criterion and the reduction pair processor in com...
RTA
2010
Springer
13 years 8 months ago
2010
Springer
We show that, contrary to the situation in first-order term rewriting, almost none of the usual properties of rewriting are modular for higher-order rewriting, irrespective of the...