Sciweavers

RTA
2010
Springer
13 years 2 months ago
The Undecidability of Type Related Problems in Type-free Style System F
We consider here a number of variations on the System F, that are predicative second-order systems whose terms are intermediate between the Curry style and Church style. The terms ...
Ken-etsu Fujita, Aleksy Schubert
RTA
2010
Springer
13 years 2 months ago
Polynomial Interpretations over the Reals do not Subsume Polynomial Interpretations over the Integers
Polynomial interpretations are a useful technique for proving termination of term rewrite systems. They come in various flavors: polynomial interpretations with real, rational and...
Friedrich Neurauter, Aart Middeldorp
RTA
2010
Springer
13 years 6 months ago
Underspecified computation of normal forms
We consider the problem of computing, out of a set C of trees and a rewrite system R, those trees in C that cannot be rewritten into a tree in C. We solve this problem for sets of ...
Alexander Koller, Stefan Thater
RTA
2010
Springer
13 years 7 months ago
Automated Termination Analysis of Java Bytecode by Term Rewriting
We present an automated approach to prove termination of Java Bytecode (JBC) programs by automatically transforming them to term rewrite systems (TRSs). In this way, the numerous t...
Carsten Otto, Marc Brockschmidt, Christian von Ess...
RTA
2010
Springer
13 years 8 months ago
Automated Confluence Proof by Decreasing Diagrams based on Rule-Labelling
Decreasing diagrams technique (van Oostrom, 1994) is a technique that can be widely applied to prove confluence of rewrite systems. To directly apply the decreasing diagrams techn...
Takahito Aoto
RTA
2010
Springer
13 years 8 months ago
Computing Critical Pairs in 2-Dimensional Rewriting Systems
Rewriting systems on words are very useful in the study of monoids. In good cases, they give finite presentations of the monoids, allowing their manipulation by a computer. Even b...
Samuel Mimram
RTA
2010
Springer
13 years 8 months ago
Infinitary Rewriting: Foundations Revisited
Infinitary Term Rewriting allows to express infinitary terms and infinitary reductions that converge to them. As their notion of transfinite reduction in general, and as binary...
Stefan Kahrs
RTA
2010
Springer
13 years 8 months ago
Polynomially Bounded Matrix Interpretations
Matrix interpretations can be used to bound the derivational complexity of rewrite systems. We present a criterion that completely characterizes matrix interpretations that are pol...
Johannes Waldmann
RTA
2010
Springer
13 years 8 months ago
A Proof Calculus Which Reduces Syntactic Bureaucracy
In usual proof systems, like the sequent calculus, only a very limited way of combining proofs is available through the tree structure. We present in this paper a logicindependent ...
Alessio Guglielmi, Tom Gundersen, Michel Parigot
RTA
2010
Springer
13 years 8 months ago
Closing the Gap Between Runtime Complexity and Polytime Computability
In earlier work, we have shown that for confluent term rewrite systems (TRSs for short), innermost polynomial runtime complexity induces polytime computability of the functions de...
Martin Avanzini, Georg Moser