HOA
1993
13 years 9 months ago
1993
This paper studies termination properties of rewrite systems that are typeable using intersection types. It introduces a notion of partial type assignment on Curryfied Term Rewri...
RTA
1997
Springer
13 years 9 months ago
1997
Springer
Abstract. We investigate conditions under which con uence and or termination are preserved for constructor-sharing and hierarchical combinations of rewrite systems, one of which is...
17
Voted
PPDP
2001
Springer
13 years 9 months ago
2001
Springer
We define a transformation from a left-linear constructor-based conditional rewrite system into an overlapping inductively sequential rewrite system. This transformation is sound...
CADE
2001
Springer
13 years 9 months ago
2001
Springer
The dependency pair method of Arts and Giesl is the most powerful technique for proving termination of term rewrite systems automatically. We show that the method can be improved b...
RTA
2007
Springer
13 years 11 months ago
2007
Springer
The use of automata techniques to prove the termination of string rewrite systems and left-linear term rewrite systems is advocated by Geser et al. in a recent sequence of papers. ...
PPDP
2007
Springer
13 years 11 months ago
2007
Springer
Non-confluent and non-terminating rewrite systems are interesting from the point of view of programming. In particular, existing functional logic languages use such kind of rewri...
RTA
2009
Springer
13 years 11 months ago
2009
Springer
Abstract. We show how polynomial path orders can be employed efficiently in conjunction with weak innermost dependency pairs to automatically certify the polynomial runtime comple...
FROCOS
2009
Springer
13 years 11 months ago
2009
Springer
Deduction modulo consists in applying the inference rules of a deductive system modulo a rewrite system over terms and formulæ. This is equivalent to proving within a so-called co...