Sciweavers

Share
FROCOS
2011
Springer
8 years 6 months ago
Harnessing First Order Termination Provers Using Higher Order Dependency Pairs
Many functional programs and higher order term rewrite systems contain, besides higher order rules, also a significant first order part. We discuss how an automatic termination p...
Carsten Fuhs, Cynthia Kop
RTA
2011
Springer
8 years 10 months ago
Maximal Completion
Given an equational system, completion procedures compute an equivalent and complete (terminating and confluent) term rewrite system. We present a very simple and efficient compl...
Dominik Klein, Nao Hirokawa
LPAR
2010
Springer
9 years 5 months ago
Infinite Families of Finite String Rewriting Systems and Their Confluence
We introduce parameterized rewrite systems for describing infinite families of finite string rewrite systems depending upon non-negative integer parameters, as well as ways to reas...
Jean-Pierre Jouannaud, Benjamin Monate
CORR
2008
Springer
148views Education» more  CORR 2008»
9 years 5 months ago
Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo
In deduction modulo, a theory is not represented by a set of axioms but by a congruence on propositions modulo which the inference rules of standard deductive systems--such as for ...
Guillaume Burel
TACS
1994
Springer
9 years 11 months ago
Syntactic Definitions of Undefined: On Defining the Undefined
In the A-calculus, there is a standard notion of what terms should be considered to be "undefined": the unsolvable terms. There are various equivalent characterisations o...
Zena M. Ariola, Richard Kennaway, Jan Willem Klop,...
ALP
1992
Springer
9 years 11 months ago
On the Relation Between Primitive Recursion, Schematization and Divergence
The paper presents a new schematization of in nite families of terms called the primal grammars, based on the notion of primitive recursive rewrite systems. This schematization is...
Miki Hermann
MFCS
1997
Springer
9 years 11 months ago
Simulation as a Correct Transformation of Rewrite Systems
Abstract. Kamperman and Walters proposed the notion of a simulation of one rewrite system by another one, whereby each term of the simulating rewrite system is related to a term in...
Wan Fokkink, Jaco van de Pol
CC
2001
Springer
177views System Software» more  CC 2001»
9 years 11 months ago
Imperative Program Transformation by Rewriting
Abstract. We present a method of specifying standard imperative program optimisations as a rewrite system. To achieve this we have extended the idea of matching sub-terms in expres...
David Lacey, Oege de Moor
CSL
2009
Springer
10 years 1 months ago
On the Relation between Sized-Types Based Termination and Semantic Labelling
We investigate the relationship between two independently developed termination techniques for rst and higher-order rewrite systems. On the one hand, sized-types based termination...
Frédéric Blanqui, Cody Roux
books