The authors present an improved and more complex treatment of equational logic. Compared with previous works, this paper deals more simply with concepts like polymorphism, partiality, and dependent types.

Overall, the paper is good. Its strengths are its investigation of computational aspects of equational type logic within conditional term rewriting systems and of the confluence of these systems.

Only section 2 does not have the quality of the rest of the paper: there the authors do not seem to understand “compile time” and “run time.” Sections 3 to 7 are well organized with appropriate examples, although the proof of proposition 3.10 is insufficient--it simply repeats the proposition word for word. The reader should have a good background in term rewriting theory, mathematical logic, and algebraic specification.