RTA
2005
Springer
14 years 4 months ago
2005
Springer
We consider the relation of the dual calculus of Wadler (2003) to the λµ-calculus of Parigot (1992). We give translations from the λµ-calculus into the dual calculus and back a...
RTA
2005
Springer
14 years 4 months ago
2005
Springer
Proofs of equalities may be built from assumptions using proof rules for reflexivity, symmetry, and transitivity. Reflexivity is an axiom proving x=x for any x; symmetry is a 1-p...
RTA
2005
Springer
14 years 4 months ago
2005
Springer
RTA
2005
Springer
14 years 4 months ago
2005
Springer
Abstract. Partial-inversion compilers generate programs which compute some unknown inputs of given programs from a given output and the rest of inputs whose values are already give...
RTA
2005
Springer
14 years 4 months ago
2005
Springer
Many applications of congruence closure nowadays require the ability of recovering, among the thousands of input equations, the small subset that caused the equivalence of a given ...
RTA
2005
Springer
14 years 4 months ago
2005
Springer
Abstract. This paper is a contribution to the long standing open problem of uniform termination of Semi-Thue Systems that consist of one rule s → t. McNaughton previously showed ...
RTA
2005
Springer
14 years 4 months ago
2005
Springer
Cryptographic protocols are small programs which involve a high level of concurrency and which are difficult to analyze by hand. The most successful methods to verify such protocol...
RTA
2005
Springer
14 years 4 months ago
2005
Springer
We present a new method for proving termination of term rewriting systems automatically. It is a generalization of the match bound method for string rewriting. To prove that a term...
RTA
2005
Springer
14 years 4 months ago
2005
Springer
RTA
2005
Springer
14 years 4 months ago
2005
Springer
Abstract. This paper shows that the suitable orderings for proving innermost termination are characterized by the innermost parallel monotonicity, IP-monotonicity for short. This p...