WRLA2002

Keywords: Lambda Calculus, Rho Calculus, Type Systems, Pattern Matching, Theoretical Frameworks and Foundations, Curry-Howard, Logics. Pure Patterns Type Systems.

Abstract: In this talk we present a framework of algebraic type systems, in which we consider rules as lambda terms with patterns, and rule applications as lambda applications with pattern matching facilities. The framework is based on the Rewriting Calculus (or Rho Calculus), a simple calculus that uniformly integrates abstractions on patterns.
More generally, the framework, can be ''customized'' with more sophisticated theories, like commutativity, associativity, associativity-commutativity, etc. This allows us to encode complex structures such as list, sets, and objects.
Its powerful type system, based on the Calculus of Constructions of Coquand and Huet, allows to statically type-checks terms of the framework.
This work can be seen as a (little) contribution to a formal connection between logics and rewriting, a (little) step towards the Curry-Howard isomorphism relating logics and type systems and a (little) formal basis to build powerful theorem provers based on lambda calculus and efficient rewriting.

Keywords:

Abstract: Protocols for secure group management are essential in applications that are concerned with confidential authenticated communication among coalition members, authenticated group decisions, or the secure administration of group membership and access control. New languages and models are necessary to appropriately capture the concepts of such protocols and make them amenable to formal analysis.
For this purpose, we developed MuCAPSL (Multicast Common Authentication Protocol Specification Language) and its intermediate language MuCIL (MuCAPSL Intermediate Language). MuCIL is based on multiset term rewriting rules that permit state changes to be presented concisely, and in a way that closely matches the requirements of existing protocol analysis tools. With the help of the Group-Diffie-Hellman protocol suite we illustrate how secure group communication principles are modeled using multiset term rewriting.

Keywords:

Abstract: The pi-calculus is based on two ideas, name passing and some forms of composition of processes. Through the study of many researchers, a stunning expressive power of this combination has been uncovered for representing dynamics and algebra of diverse classes of computations. However there is certain lack of precision in known representations (for example they are rarely equationally fully abstract).
Recently Berger, Yoshida and I found that a use of certain notions of types, suggested from Linear Logic and game semantics, can make the representation of known programming languages semantically exact. The representability extends from higher-order procedures to imperative constructs (such as references and control) to objects to generic computation to concurrency to elements of distributed computing.
In this talk I illustrate how and why the use of types makes the pi-calculus a powerful tool for representing computation, and how we can apply such representation to practice, both through concrete examples. I will also suggest how the encounter between this line of study and general theories from rewriting logics would lead to several fascinating research topics.

Keywords: Maude, executable model, Biological pathways, formal analysis, metamodeling

Abstract: In this paper we describe the use of the rewriting logic based Maude tool to model and analyze mammalian signaling pathways. We discuss the representation of the underlying biological concepts and events and describe the use of the new search and model checking capabilities of Maude 2.0 to analyze the modeled network. We also discuss the use of Maude's reflective capability for meta modeling and analyzing the models themselves. The idea of symbolic biological experiments opens up an exciting new world of challenging applications for formal methods in general and for rewriting logic based formalisms in particular.

Keywords: tile logic, rewriting logic, category theory, transactions, zero-safe nets, Petri nets.

Abstract: We propose a modular high-level approach to the specification of transactions in rewriting logic, where the operational and the abstract views are related by suitable adjunctions between categories of tile theories and of rewrite theories.

Keywords: PLAN, Maude, executable specification, CINNI calculus, formal analysis

Abstract: PLAN is a language designed for programming active networks, and can more generally be regarded as a model of mobile computation. PLAN generalizes the paradigm of imperative functional programming in an elegant way that allows for recursive, remote function calls, and it provides a clear mechanism for the interaction between host and mobile code. Techniques for specifying and reasoning about such languages are of growing importance. In this paper we describe our specification of PLAN in the rewriting logic language Maude. We show how techniques for specifying the operational semantics of imperative functional programs (syntax-based semantics) and for formalizing variable binding constructs and mobile environments (CINNI calculus) are used in combination with the natural representation of concurrency and distribution provided by rewriting logic to develop a faithful description of the informal PLAN semantics. We also illustrate the wide-spectrum approach to formal modeling supported by Maude: executing PLAN programs; analyzing PLAN programs using search and model-checking; proving properties of particular PLAN programs; and proving general properties of the PLAN language.

Keywords: Rewriting, termination, outermost, strategy, rule based languages, induction, narrowing, ordering constraints.

Abstract: We propose a semi-automatic inductive process to prove termination of outermost rewriting on ground term algebras. The method is based on an abstraction mechanism, schematizing normalisation of subterms, and on narrowing, schematizing reductions on ground terms. The induction ordering is not needed a priori, but is a solution of constraints set along the proof. Our method applies in particular to systems that are non-terminating for the standard strategy nor even for the lazy strategy.

Keywords: Declarative programming, OBJ, strategy annotations

Abstract: Strategy annotations are used in several programming languages as replacement restrictions aimed at improving efficiency and/or reducing the risk of nontermination. Unfortunately, rewriting restrictions can have a negative impact on the ability to compute normal forms. In this paper, we first ascertain/clarify the conditions ensuring correctness and completeness (regarding normalization) of computing with strategy annotations. Then, we define a program transformation methodology for (correct and) complete evaluations which applies to OBJ-like languages.

Keywords: pi-calculus, asynchrony, may testing, traces, Maude

Abstract: We describe an executable specification of the operational semantics of an asynchronous version of the pi-calculus in Maude by means of conditional rewrite rules with rewrites in the conditions. We also present an executable specification of the may testing equivalence on non-recursive asynchronous pi-calculus processes, using the Maude metalevel. Specifically, we describe our use of the metaSearch operation to both calculate the set of all finite traces of a non-recursive process, and to compare the trace sets of two processes according to a preorder relation that characterizes may testing in asynchronous pi-calculus. Thus, in both the specification of the operational semantics and the may testing, we make heavy use of new features introduced in version 2.0 of the Maude language and system.

Keywords: protocol specification, meta-objects

Abstract: Meta-objects are used to factor the specification of the first asynchronous, proactive, secret-sharing protocol into secret-sharing, replication and encryption layers.

Keywords: wide area languages, mobile computation, mobile agents, Mobile Maude

Abstract: A useful way of presenting a new language is by means of complete examples that show the language features in action. In this paper we do so for the Mobile Maude language, an extension of Maude that supports mobile computation. We implement an ambitious wide area application, namely a conference reviewing system, an example described by Cardelli as a challenge for any wide area language to demonstrate its usability.

Keywords: reflection, reflective logics, universal theory, reflective rewriting logic, reflective membership equational logic, reflective Horn logic with equality

Abstract: We show that the more general variant of rewriting logic where the underlying equational specifications are membership equational theories, and where the rules are conditional and can have equations, memberships and rewrites in the conditions is reflective. We also show that membership equational logic, many-sorted equational logic, and Horn logic with equality are likewise reflective. These results provide logical foundations for reflective languages and tools based on these logics, and in particular for the Maude language itself.

Keywords: authentication protocols, CafeOBJ, the NSPK protocol, observational transition systems, rewriting, verification

Abstract: We propose a method of formally analysing security protocols based on rewriting. The method is roughly as follows. A security protocol is modeled as an observational transition system, which is described in CafeOBJ. Proof scores showing that the protocol has safety (security) properties are then written in CafeOBJ and the proof scores are executed (rewritten) by the CafeOBJ system.

Keywords: executable semantic framework, operational semantics, CCS, modal logic

Abstract: This paper describes in detail how to bridge the gap between theory and practice in a new implementation of the CCS operational semantics in Maude, where transitions become rewrites and inference rules become conditional rewrite rules with rewrites in the conditions, as made possible by the new features in Maude 2.0. We implement both the usual transition semantics and the weak transition semantics where internal actions are not observed, and on top of them we also implement the Hennessy-Milner modal logic for describing processes. We compare this implementation with a previous one where transitions become judgements and inference rules become rewrites, and also comment on extensions to the LOTOS language.

Keywords:

Abstract: The Maude LTL model checker supports on-the-fly explicit-state model checking of concurrent systems expressed as rewrite theories with performance comparable to that of current tools of that kind, such as SPIN. This greatly expands the range of applications amenable to model checking analysis. Besides traditional areas well supported by current tools, such as hardware and communication protocols, many new applications in areas such as rewriting logic models of cell biology, or next-generation reflective distributed systems can be easily specified and model checked with our tool.

Abstract: Strategy annotations have been used in a number of programming languages and rewriting-based systems (e.g., OBJ2, OBJ3, CafeOBJ, Maude, JITty, ...) for improving the termination behavior and avoiding useless computations. They also accomplish the important task of providing a simple interface for understanding and eventually modifying the execution of programs. They have been given different formats and operational interpretations: a recent classification distinguishes between E-strategies, just-in-time style, and laziness annotations. In all these cases, context-sensitive rewriting (CSR) provides a framework for analyzing and ensuring essential computational properties such as termination, correctness and completeness (regarding the usual semantics: head-normalization, normalization, functional evaluation, and infinitary normalization). Thus, CSR and its associated techniques (e.g., for ensuring normalization or termination) provide a useful tool for the programmers and designers of software systems aimed at supporting the practical use of such programming languages and rewriting-based systems. In this tutorial, we summarize the main results and techniques regarding CSR, and exemplify their use with programs using strategy annotations.

Abstract: Since the first papers on rewriting logic in 1990 a lot has happened, both in theoretical developments, in logical and semantic framework applications, and in rewriting-logic-based tool development. I will try to give a personal view of some of the most recent developments that have taken place in all these areas. This will not be a survey (the rewriting logic "Roadmap and Bibliography" by Meseguer and Marti-Oliet in TCS Vol. 285, No. 2 is the last survey that could be consulted). Rather than trying to be exhaustive, I will focus on some recent developments that, among others, seem promising to me.

Abstract: Tile logic (TL) is a rule-based framework that attempts at transferring ordinary operational and abstract semantics techniques to compositional, interactive, concurrent, open systems. TL extends SOS with a uniform treatment of open and closed terms: configurations can be partially specified and transitions are labeled by pairs trigger/effect. When triggers and effects are vacuous, TL rules become ordinary rewrite rules. By analogy with rewriting logic (RL), where logical formulas define concurrent rewrites, TL admits a sequent calculus presentation. However, TL extends RL by handling rewriting with side effects and synchronization, and the categorical models of RL are 2-categories, while TL requires double categories. As for SOS, bisimilarity abstract semantics of tiles can be given in coalgebraic terms, and certain formats can be specified which guarantee that bisimilarity is a congruence.
In the tutorial, the double categorical and coalgebraic foundations of tile logic are presented. States and trigger/effects are arrows of certain symmetric monoidal categories able to model up to isomorphism several interesting classes of graphs and pomsets. A cartesian higher order version is also described, equipped with a double lambda-calculus as internal language.
The expressiveness of tile logic is demonstrated by modeling in a natural way several concurrent models of computations, including process algebras, graph transformations and logic programming.

Abstract: We first show how a well-known class of pure type systems can be represented in a first-order logical framework, namely rewriting logic, in an operationally useful way. To obtain a small representational distance and to avoid the problem of alpha-closure, pointed out earlier by Pollack, we use the CINNI explicit substitution calculus, and we introduce a notion of uniform pure type systems with explicit names. Based on these ideas, the second part of the tutorial motivates and develops the open calculus of constructions (OCC), a type theory with dependent types that has membership equational logic and rewriting logic as computational sublanguages. Its applications in programming, specification and interactive theorem proving are illustrated using several examples.