Higher-Order and Symbolic Computation, 20(1/2)

The first papers on rewriting logic were published in 1990, and six years later the First Workshop on Rewriting Logic and its Applications was held at the Asilomar Conference Center, California. After two more workshops in Pont-à-Mousson, France (1998), and Kanazawa, Japan (2000), J. Meseguer and N. Martí-Oliet edited a special issue about this subject of the journal Theoretical Computer Science, which was published as volume 285, issue 2, in August 2002. This series of workshops continued in Pisa, Italy (2002), and Barcelona, Spain (2004), after which we thought that there was enough new available material to make it worth the publication of another special issue. To this end, we selected, with the wise help of other members of the WRLA 2004 program committee, among the seventeen papers accepted for the workshop plus two invited talks (that have appeared in the WRLA 2004 proceedings published as volume 117 of Electronic Notes in Theoretical Computer Science), seven papers to be invited for this special issue. A rigorous reviewing process in which each paper was evaluated by at least three referees allowed us to select out of them the five papers that we summarize next.

The paper Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types, by I. Cervesato and M.-O. Stehr, presents an efficient embedding of the security protocol specification language MSR, which is based on a form of first-order multiset rewriting extended with existential name generation and a flexible type infrastructure centered on dependent types with subsorting, into an extension of rewriting logic with dependent types integrating key concepts from equational logic, rewriting logic, and type theory. This encoding has served as the basis for the implementation of an MSR specification and analysis environment using the rewriting engine Maude.

In A rho-calculus of explicit constraint application, H. Cirstea, G. Faure, and C. Kirchner describe two versions of the rho-calculus, one with explicit matching and one with explicit substitutions, together with a version that combines the two and considers efficiency issues. In this way, it bridges theoretical presentations of the rho-calculus, which often treat the matching constraint computations as an atomic operation, with actual implementations, where solving a matching equation can require costly computations for some matching theories and the substitution application usually involves a term traversal.

The paper A new generic scheme for functional logic programming with constraints, by F. J. López Fraguas, M. Rodríguez Artalejo, and R. del Vado Vírseda, proposes a new generic scheme CFLP(D), for lazy Constraint Functional Logic Programming over a parametrically given constraint domain D, which is assumed to provide domain specific data values and constraints. CFLP(D) programs consist of sets of constrained rewrite rules that define the behavior of possibly higher-order and/or non-deterministic lazy functions over D. A declarative semantics for these programs is obtained through a Constraint Rewriting Logic CRWL(D) which relies on a new formalization of constraint domains and program interpretations, allowing a flexible combination of domain specific data values and user defined data constructors.

In Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols, J. Meseguer and P. Thati propose a generalization of narrowing, traditionally used to solve equations in initial and free algebras modulo a set of equations E, to solve reachability goals in initial and free models of a rewrite theory R. Under appropriate executability assumptions about the rewrite theory R, narrowing is sound and weakly complete (i.e., complete for normalized solutions), but in general it is not strongly complete, that is, not complete when some solutions can be further rewritten by R. Several large classes of rewrite theories for which narrowing is strongly complete are identified, trying to cover many practical applications. Of particular interest is the application of narrowing to analysis of cryptographic protocols.

We want to express our most sincere thanks to all the people that have made this special issue possible. First of all, to the authors, who agreed to write extended versions of their works and later incorporated all the corrections and improvements required by a thorough refereeing process. Secondly, to all the referees, who have kindly contributed their time and effort to ensure the highest scholarly quality for each paper. Finally, to Miguel Palomino, who helped us in revising the final versions of most of these papers to improve their presentation before publication.