An overview of the K semantic framework
---
paper_title: A Syntactic Approach to Type Soundness

paper_content:

We present a new approach to proving type soundness for Hindley/Milner-style polymorphic type systems. The keys to our approach are (1) an adaptation of subject reduction theorems from combinatory logic to programming languages, and (2) the use of rewriting techniques for the specification of the language semantics. The approach easily extends from polymorphic functional languages to imperative languages that provide references, exceptions, continuations, and similar features. We illustrate the technique with a type soundness theorem for the core of Standard ML, which includes the first type soundness proof for polymorphic exceptions and continuations.
---
paper_title: Rewriting Logic as a Semantic Framework for Concurrency: a Progress Report

paper_content:

This paper surveys the work of many researchers on rewriting logic since it was first introduced in 1990. The main emphasis is on the use of rewriting logic as a semantic framework for concurrency. The goal in this regard is to express as faithfully as possible a very wide range of concurrency models, each on its own terms, avoiding any encodings or translations. Bringing very different models under a common semantic framework makes easier to understand what different models have in common and how they differ, to find deep connections between them, and to reason across their different formalisms. It becomes also much easier to achieve in a rigorous way the integration and interoperation of different models and languages whose combination offers attractive advantages. The logic and model theory of rewriting logic are also summarized, a number of current research directions are surveyed, and some concluding remarks about future directions are made.
---
paper_title: The Rewriting Logic Semantics Project

paper_content:

Rewriting logic is a flexible and expressive logical framework that unifies algebraic denotational semantics and structural operational semantics (SOS) in a novel way, avoiding their respective limitations and allowing succinct semantic definitions. The fact that a rewrite logic theory's axioms include both equations and rewrite rules provides a useful ''abstraction dial'' to find the right balance between abstraction and computational observability in semantic definitions. Such semantic definitions are directly executable as interpreters in a rewriting logic language such as Maude, whose generic formal tools can be used to endow those interpreters with powerful program analysis capabilities.
---
paper_title: Introduction to the Algebraic Theory of Graph Grammars (A Survey)

paper_content:

The aim of this survey is to motivate and introduce the basic constructions and results which have been developed in the algebraic theory of graph grammars up to now. The complete material is illustrated by several examples, especially by applications to a "very small data base system", where consistent states are represented as graphs, operation rules and operations as productions and derivations in a graph grammar respectively. Further applications to recursively defined functions, record handling, compiler techniques and development and evolution in Biology are sketched in the introduction. This survey is divided into the following sections: ::: ::: 1. ::: ::: INTRODUCTION ::: ::: ::: ::: ::: 2. ::: ::: GLUING CONSTRUCTIONS FOR GRAPHS ::: ::: ::: ::: ::: 3. ::: ::: SEQUENTIAL GRAPH GRAMMARS ::: ::: ::: ::: ::: 4. ::: ::: CHURCH-ROSSER PROPERTIES, PARALLELISM — AND CONCURRENCY THEOREMS ::: ::: ::: ::: ::: 5. ::: ::: PROPERTIES OF DERIVATION SEQUENCES ::: ::: ::: ::: ::: 6. ::: ::: PARALLEL GRAPH GRAMMARS ::: ::: ::: ::: ::: 7. ::: ::: LOCALLY STAR GLUING FORMULAS ::: ::: ::: ::: ::: 8. ::: ::: GRAPH LANGUAGES ::: ::: ::: ::: ::: 9. ::: ::: APPENDIUM: CONCEPTS OF CATEGORY THEORY USED IN THE ALGEBRAIC THEORY OF GRAPH GRAMMARS ::: ::: ::: ::: ::: 10. ::: ::: REFERENCES
---
paper_title: Defining and Executing P Systems with Structured Data in K

paper_content:

K is a rewrite-based framework proposed for giving formal executable semantics to programming languages and/or calculi. K departs from other rewrite-based frameworks in two respects: (1) it assumes multisets and lists as builtin, the former modeling parallel features, while the latter sequential ones; and (2) the parallel application of rewriting rules is extended from non-overlapping rules to rules which may overlap, but on parts which are not changed by these rules (may overlap on "read only" parts). This paper shows how P systems and variants can be defined as K (rewrite) systems. This is the first representation of P systems into a rewrite-based framework that captures the behavior (reaction steps) of the original P system step-for-step. In addition to providing a formal executable semantic framework for P systems, the embedding of P systems as K systems also serves as a basis for experimenting with and developing new extensions of P systems, e.g., with structured data. A Maude-based application for executing P systems defined in K has been implemented and experimented with; initial results show computational advantages of using structured objects in P systems.
---
paper_title: A Rewriting Logic Approach to Operational Semantics ∗

paper_content:

This paper shows how rewriting logic semantics (RLS) can be used as a computational logic framework for operational semantic definitions of programming languages. Several operational semantics styles are addressed: big-step and small-step structural operational semantics (SOS), modular SOS, reduction semantics with evaluation contexts, continuation-based semantics, and the chemical abstract machine. Each of these language definitional styles can be faithfully captured as an RLS theory, in the sense that there is a one-to-one correspondence between computational steps in the original language definition and computational steps in the corresponding RLS theory. A major goal of this paper is to show that RLS does not force or pre-impose any given language definitional style, and that its flexibility and ease of use makes RLS an appealing framework for exploring new definitional styles.
---
paper_title: Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools

paper_content:

Formal semantic definitions of concurrent languages, when specified in a well-suited semantic framework and supported by generic and efficient formal tools, can be the basis of powerful software analysis tools. Such tools can be obtained for free from the semantic definitions; in our experience in just the few weeks required to define a language’s semantics even for large languages like Java. By combining, yet distinguishing, both equations and rules, rewriting logic semantic definitions unify both the semantic equations of equational semantics (in their higher-order denotational version or their first-order algebraic counterpart) and the semantic rules of SOS. Several limitations of both SOS and equational semantics are thus overcome within this unified framework. By using a high-performance implementation of rewriting logic such as Maude, a language’s formal specification can be automatically transformed into an efficient interpreter. Furthermore, by using Maude’s breadth first search command, we also obtain for free a semi-decision procedure for finding failures of safety properties; and by using Maude’s LTL model checker, we obtain, also for free, a decision procedure for LTL properties of finite-state programs. These possibilities, and the competitive performance of the analysis tools thus obtained, are illustrated by means of a concurrent Caml-like language; similar experience with Java (source and JVM) programs is also summarized.
---
paper_title: Computing with Membranes

paper_content:

We introduce a new computability model, of a distributed parallel type, based on the notion of a membrane structure. Such a structure consists of several cell-like membranes, recurrently placed inside a unique “skin” membrane. A plane representation is a Venn diagram without intersected sets and with a unique superset. In the regions delimited by the membranes there are placed objects. These objects are assumed to evolve: each object can be transformed in other objects, can pass through a membrane, or can dissolve the membrane in which it is placed. A priority relation between evolution rules can be considered. The evolution is done in parallel for all objects able to evolve. In this way, we obtain a computing device (we call it a P system): start with a certain number of objects in a certain membrane and let the system evolve; if it will halt (no object can further evolve), then the computation is finished, with the result given as the number of objects in a specified membrane. If the development of the system goes forever, then the computation fails to have an output. We prove that the P systems with the possibility of objects to cooperate characterize the recursively enumerable sets of natural numbers; moreover, systems with only two membranes suffice. In fact, we do not need cooperating rules, but we only use catalysts, specified objects which are present in the rules but are not modified by the rule application. One catalyst suffices. A variant is also considered, with the objects being strings over a given alphabet. The evolution rules are now based on string transformations. We investigate the case when either the rewriting operation from Chomsky grammars (with respect to context-free productions) or the splicing operation from H systems investigated in the DNA computing is used. In both cases, characterizations of recursively enumerable languages are obtained by very simple P systems: with three membranes in the rewriting case and four in the splicing case. Several open problems and directions for further research are formulated
---
paper_title: The chemical abstract machine

paper_content:

We introduce a new kind of abstract machine based on the chemical metaphor used in the Γ language of Banâtre & al . States of a machine are chemical solutions where floating molecules can interact according to reaction rules. Solutions can be stratified by encapsulating subsolutions within membranes that force reactions to occur locally. We illustrate the use of this model by describing the operational semantics of the TCCS and CCS process calculi. We also show how to extract a higher-order concurrent λ-calculus out of the basic concepts of the chemical abstract machine.
---
paper_title: A Syntactic Approach to Type Soundness

paper_content:

We present a new approach to proving type soundness for Hindley/Milner-style polymorphic type systems. The keys to our approach are (1) an adaptation of subject reduction theorems from combinatory logic to programming languages, and (2) the use of rewriting techniques for the specification of the language semantics. The approach easily extends from polymorphic functional languages to imperative languages that provide references, exceptions, continuations, and similar features. We illustrate the technique with a type soundness theorem for the core of Standard ML, which includes the first type soundness proof for polymorphic exceptions and continuations.
---
paper_title: A Rewriting Logic Approach to Operational Semantics ∗

paper_content:

This paper shows how rewriting logic semantics (RLS) can be used as a computational logic framework for operational semantic definitions of programming languages. Several operational semantics styles are addressed: big-step and small-step structural operational semantics (SOS), modular SOS, reduction semantics with evaluation contexts, continuation-based semantics, and the chemical abstract machine. Each of these language definitional styles can be faithfully captured as an RLS theory, in the sense that there is a one-to-one correspondence between computational steps in the original language definition and computational steps in the corresponding RLS theory. A major goal of this paper is to show that RLS does not force or pre-impose any given language definitional style, and that its flexibility and ease of use makes RLS an appealing framework for exploring new definitional styles.
---
paper_title: Computing with Membranes

paper_content:

We introduce a new computability model, of a distributed parallel type, based on the notion of a membrane structure. Such a structure consists of several cell-like membranes, recurrently placed inside a unique “skin” membrane. A plane representation is a Venn diagram without intersected sets and with a unique superset. In the regions delimited by the membranes there are placed objects. These objects are assumed to evolve: each object can be transformed in other objects, can pass through a membrane, or can dissolve the membrane in which it is placed. A priority relation between evolution rules can be considered. The evolution is done in parallel for all objects able to evolve. In this way, we obtain a computing device (we call it a P system): start with a certain number of objects in a certain membrane and let the system evolve; if it will halt (no object can further evolve), then the computation is finished, with the result given as the number of objects in a specified membrane. If the development of the system goes forever, then the computation fails to have an output. We prove that the P systems with the possibility of objects to cooperate characterize the recursively enumerable sets of natural numbers; moreover, systems with only two membranes suffice. In fact, we do not need cooperating rules, but we only use catalysts, specified objects which are present in the rules but are not modified by the rule application. One catalyst suffices. A variant is also considered, with the objects being strings over a given alphabet. The evolution rules are now based on string transformations. We investigate the case when either the rewriting operation from Chomsky grammars (with respect to context-free productions) or the splicing operation from H systems investigated in the DNA computing is used. In both cases, characterizations of recursively enumerable languages are obtained by very simple P systems: with three membranes in the rewriting case and four in the splicing case. Several open problems and directions for further research are formulated
---
paper_title: The chemical abstract machine

paper_content:

We introduce a new kind of abstract machine based on the chemical metaphor used in the Γ language of Banâtre & al . States of a machine are chemical solutions where floating molecules can interact according to reaction rules. Solutions can be stratified by encapsulating subsolutions within membranes that force reactions to occur locally. We illustrate the use of this model by describing the operational semantics of the TCCS and CCS process calculi. We also show how to extract a higher-order concurrent λ-calculus out of the basic concepts of the chemical abstract machine.
---
paper_title: A Rewriting Logic Approach to Operational Semantics ∗

paper_content:

This paper shows how rewriting logic semantics (RLS) can be used as a computational logic framework for operational semantic definitions of programming languages. Several operational semantics styles are addressed: big-step and small-step structural operational semantics (SOS), modular SOS, reduction semantics with evaluation contexts, continuation-based semantics, and the chemical abstract machine. Each of these language definitional styles can be faithfully captured as an RLS theory, in the sense that there is a one-to-one correspondence between computational steps in the original language definition and computational steps in the corresponding RLS theory. A major goal of this paper is to show that RLS does not force or pre-impose any given language definitional style, and that its flexibility and ease of use makes RLS an appealing framework for exploring new definitional styles.
---
paper_title: Introduction to the Algebraic Theory of Graph Grammars (A Survey)

paper_content:

The aim of this survey is to motivate and introduce the basic constructions and results which have been developed in the algebraic theory of graph grammars up to now. The complete material is illustrated by several examples, especially by applications to a "very small data base system", where consistent states are represented as graphs, operation rules and operations as productions and derivations in a graph grammar respectively. Further applications to recursively defined functions, record handling, compiler techniques and development and evolution in Biology are sketched in the introduction. This survey is divided into the following sections: ::: ::: 1. ::: ::: INTRODUCTION ::: ::: ::: ::: ::: 2. ::: ::: GLUING CONSTRUCTIONS FOR GRAPHS ::: ::: ::: ::: ::: 3. ::: ::: SEQUENTIAL GRAPH GRAMMARS ::: ::: ::: ::: ::: 4. ::: ::: CHURCH-ROSSER PROPERTIES, PARALLELISM — AND CONCURRENCY THEOREMS ::: ::: ::: ::: ::: 5. ::: ::: PROPERTIES OF DERIVATION SEQUENCES ::: ::: ::: ::: ::: 6. ::: ::: PARALLEL GRAPH GRAMMARS ::: ::: ::: ::: ::: 7. ::: ::: LOCALLY STAR GLUING FORMULAS ::: ::: ::: ::: ::: 8. ::: ::: GRAPH LANGUAGES ::: ::: ::: ::: ::: 9. ::: ::: APPENDIUM: CONCEPTS OF CATEGORY THEORY USED IN THE ALGEBRAIC THEORY OF GRAPH GRAMMARS ::: ::: ::: ::: ::: 10. ::: ::: REFERENCES
---
paper_title: Introduction to the Algebraic Theory of Graph Grammars (A Survey)

paper_content:

The aim of this survey is to motivate and introduce the basic constructions and results which have been developed in the algebraic theory of graph grammars up to now. The complete material is illustrated by several examples, especially by applications to a "very small data base system", where consistent states are represented as graphs, operation rules and operations as productions and derivations in a graph grammar respectively. Further applications to recursively defined functions, record handling, compiler techniques and development and evolution in Biology are sketched in the introduction. This survey is divided into the following sections: ::: ::: 1. ::: ::: INTRODUCTION ::: ::: ::: ::: ::: 2. ::: ::: GLUING CONSTRUCTIONS FOR GRAPHS ::: ::: ::: ::: ::: 3. ::: ::: SEQUENTIAL GRAPH GRAMMARS ::: ::: ::: ::: ::: 4. ::: ::: CHURCH-ROSSER PROPERTIES, PARALLELISM — AND CONCURRENCY THEOREMS ::: ::: ::: ::: ::: 5. ::: ::: PROPERTIES OF DERIVATION SEQUENCES ::: ::: ::: ::: ::: 6. ::: ::: PARALLEL GRAPH GRAMMARS ::: ::: ::: ::: ::: 7. ::: ::: LOCALLY STAR GLUING FORMULAS ::: ::: ::: ::: ::: 8. ::: ::: GRAPH LANGUAGES ::: ::: ::: ::: ::: 9. ::: ::: APPENDIUM: CONCEPTS OF CATEGORY THEORY USED IN THE ALGEBRAIC THEORY OF GRAPH GRAMMARS ::: ::: ::: ::: ::: 10. ::: ::: REFERENCES
---
paper_title: A Rewriting Logic Approach to Operational Semantics ∗

paper_content:

This paper shows how rewriting logic semantics (RLS) can be used as a computational logic framework for operational semantic definitions of programming languages. Several operational semantics styles are addressed: big-step and small-step structural operational semantics (SOS), modular SOS, reduction semantics with evaluation contexts, continuation-based semantics, and the chemical abstract machine. Each of these language definitional styles can be faithfully captured as an RLS theory, in the sense that there is a one-to-one correspondence between computational steps in the original language definition and computational steps in the corresponding RLS theory. A major goal of this paper is to show that RLS does not force or pre-impose any given language definitional style, and that its flexibility and ease of use makes RLS an appealing framework for exploring new definitional styles.
---
paper_title: Modular Structural Operational Semantics

paper_content:

Abstract Modular SOS (MSOS) is a variant of conventional Structural Operational Semantics (SOS). Using MSOS, the transition rules for each construct of a programming language can be given incrementally, once and for all, and do not need reformulation when further constructs are added to the language. MSOS thus provides an exceptionally high degree of modularity in language descriptions, removing a shortcoming of the original SOS framework. After sketching the background and reviewing the main features of SOS, the paper explains the crucial differences between SOS and MSOS, and illustrates how MSOS descriptions are written. It also discusses standard notions of semantic equivalence based on MSOS. Appendix A shows how the illustrative MSOS rules given in the paper would be formulated in conventional SOS.
---
paper_title: Computing with Membranes

paper_content:

We introduce a new computability model, of a distributed parallel type, based on the notion of a membrane structure. Such a structure consists of several cell-like membranes, recurrently placed inside a unique “skin” membrane. A plane representation is a Venn diagram without intersected sets and with a unique superset. In the regions delimited by the membranes there are placed objects. These objects are assumed to evolve: each object can be transformed in other objects, can pass through a membrane, or can dissolve the membrane in which it is placed. A priority relation between evolution rules can be considered. The evolution is done in parallel for all objects able to evolve. In this way, we obtain a computing device (we call it a P system): start with a certain number of objects in a certain membrane and let the system evolve; if it will halt (no object can further evolve), then the computation is finished, with the result given as the number of objects in a specified membrane. If the development of the system goes forever, then the computation fails to have an output. We prove that the P systems with the possibility of objects to cooperate characterize the recursively enumerable sets of natural numbers; moreover, systems with only two membranes suffice. In fact, we do not need cooperating rules, but we only use catalysts, specified objects which are present in the rules but are not modified by the rule application. One catalyst suffices. A variant is also considered, with the objects being strings over a given alphabet. The evolution rules are now based on string transformations. We investigate the case when either the rewriting operation from Chomsky grammars (with respect to context-free productions) or the splicing operation from H systems investigated in the DNA computing is used. In both cases, characterizations of recursively enumerable languages are obtained by very simple P systems: with three membranes in the rewriting case and four in the splicing case. Several open problems and directions for further research are formulated
---
paper_title: The chemical abstract machine

paper_content:

We introduce a new kind of abstract machine based on the chemical metaphor used in the Γ language of Banâtre & al . States of a machine are chemical solutions where floating molecules can interact according to reaction rules. Solutions can be stratified by encapsulating subsolutions within membranes that force reactions to occur locally. We illustrate the use of this model by describing the operational semantics of the TCCS and CCS process calculi. We also show how to extract a higher-order concurrent λ-calculus out of the basic concepts of the chemical abstract machine.
---
paper_title: A Syntactic Approach to Type Soundness

paper_content:

We present a new approach to proving type soundness for Hindley/Milner-style polymorphic type systems. The keys to our approach are (1) an adaptation of subject reduction theorems from combinatory logic to programming languages, and (2) the use of rewriting techniques for the specification of the language semantics. The approach easily extends from polymorphic functional languages to imperative languages that provide references, exceptions, continuations, and similar features. We illustrate the technique with a type soundness theorem for the core of Standard ML, which includes the first type soundness proof for polymorphic exceptions and continuations.
---
paper_title: Matching Logic - Extended Report

paper_content:

Hoare logics rely on the fact that logic formulae can encode, or specify, program states, including environments, stacks, heaps, path conditions, data constraints, and so on. Such formula encodings tend to lose the structure of the original program state and thus to be complex in practice, making it difficult to relate formal systems and program correctness proofs to the original programming language and program, respectively. Worse, since programs often manipulate mathematical objects such as lists, trees, graphs, etc., one needs to also encode, as logical formulae, the process of identifying these objects in the encoded program state. This paper proposes matching logic, an alternative to Hoare logics in which the state structure plays a crucial role. Program states are represented as algebraic datatypes called (concrete) configurations, and program state specifications are represented as configuration terms with variables and constraints on them, called (configuration) patterns. A pattern specifies those configurations that match it. Patterns can bind variables to their scope, allowing both for pattern abstraction and for expressing loop invariants. Matching logic is tightly connected to rewriting logic semantics (RLS): matching logic formal systems can systematically be obtained from executable RLS of languages. This relationship allows to prove soundness of matching logic formal systems w.r.t. complementary, testable semantics. All notions are exemplified using KernelC, a fragment of C with dynamic memory allocation/deallocation.
---
paper_title: KOOL: an application of rewriting logic to language prototyping and analysis

paper_content:

This paper presents KOOL, a concurrent, dynamic, object-oriented language defined in rewriting logic. KOOL has been designed as an experimental language, with a focus on making the language easy to extend. This is done by taking advantage of the flexibility provided by rewriting logic, which allows for the rapid prototyping of new language features. An example of this process is illustrated by sketching the addition of synchronized methods. KOOL also provides support for program analysis through language extensions and the underlying capabilities of rewriting logic. This support is illustrated with several examples.
---
paper_title: Automatic certification of Java source code in rewriting logic

paper_content:

In this paper we propose an abstract certification techniquefor Java which is based on rewriting logic, a very general logical and semanticframework efficiently implemented in the functional programminglanguage Maude. Starting from a specification of the Java semantics writtenin Maude, we develop an abstract, finite-state operational semanticsalso written in Maude which is appropriate for program verification. Asa by-product of the abstract verification, a dependable safety certificateis delivered which consists of a set of (abstract) rewriting proofs thatcan be easily checked by the code consumer using a standard rewritinglogic engine. Our certification methodology extends to other programminglanguages by simply replacing the concrete semantics of Java by asemantics for the programming language at hand. The abstract proofcarryingcode technique has been implemented and successfully testedon several examples, which demonstrate the feasibility of our approach.
---
paper_title: An Executable Semantic Definition of the Beta Language using Rewriting Logic

paper_content:

In this paper, we present an overview of our method of specifying the semantics of programming languages using rewriting logic. This method, which we refer to as the “continuation-based style”, relies on an explicit representation of a program’s control context, allowing flexibility in defining complex, control-intensive features of languages while still allowing simple definitions of simple language constructs. To illustrate this technique, we present a definition of a significant subset of the objectoriented language Beta running in the Maude rewriting engine. This specification gives us an executable platform for running Beta programs and for experimenting with new language features. We illustrate this by extending the language with super calls. We also touch upon some features of the underlying framework, including the ability to model check Beta programs running on our framework with rewriting-based tools. keywords: programming language semantics, rewriting logic, Beta
---
paper_title: A Rewrite Framework for Language Definitions and for Generation of Efficient Interpreters

paper_content:

A rewrite logic semantic definitional framework for programming languages is introduced, called K, together with partially automated translations of K language definitions into rewriting logic and into C. The framework is exemplified by defining SILF, a simple imperative language with functions. The translation of K definitions into rewriting logic enables the use of the various analysis tools developed for rewrite logic specifications, while the translation into C allows for very efficient interpreters. A suite of tests show the performance of interpreters compiled from K definitions.
---
paper_title: A Rewriting Logic Approach to Static Checking of Units of Measurement in C

paper_content:

Many C programs assume the use of implicit domain-specific information. A common example is units of measurement, where values can have both a standard C type and an associated unit. However, since there is no way in the C language to represent this additional information, violations of domain-specific policies, such as unit safety violations, can be difficult to detect. In this paper we present a static analysis, based on the use of an abstract C semantics defined using rewriting logic, for the detection of unit violations in C programs. In contrast to typed approaches, the analysis makes use of annotations present in C comments on function headers and in function bodies, leaving the C language unchanged. Initial evaluation results show that performance scales well, and that errors can be detected without imposing a heavy annotation burden.
---
paper_title: Defining and Executing P Systems with Structured Data in K

paper_content:

K is a rewrite-based framework proposed for giving formal executable semantics to programming languages and/or calculi. K departs from other rewrite-based frameworks in two respects: (1) it assumes multisets and lists as builtin, the former modeling parallel features, while the latter sequential ones; and (2) the parallel application of rewriting rules is extended from non-overlapping rules to rules which may overlap, but on parts which are not changed by these rules (may overlap on "read only" parts). This paper shows how P systems and variants can be defined as K (rewrite) systems. This is the first representation of P systems into a rewrite-based framework that captures the behavior (reaction steps) of the original P system step-for-step. In addition to providing a formal executable semantic framework for P systems, the embedding of P systems as K systems also serves as a basis for experimenting with and developing new extensions of P systems, e.g., with structured data. A Maude-based application for executing P systems defined in K has been implemented and experimented with; initial results show computational advantages of using structured objects in P systems.
---
paper_title: From Rewriting Logic Executable Semantics to Matching Logic Program Verification

paper_content:

Rewriting logic semantics (RLS) is a definitional framework in which a programming language is defined as a rewrite theory: the algebraic signature defines the program configurations, the equations define structural identities on configurations, and the rewrite rules define the irreversible computational steps. RLS language definitions are e ciently executable using conventional rewrite engines, yielding interpreters for the defined languages for free. Matching logic is a program verification logic inspired by RLS. Matching logic specifications are particular first-order formulae with constrained algebraic structure, called patterns. Configurations satisfy patterns i they match their algebraic structure and satisfy their constraints. Patterns can naturally specify data separation and require no special support from the underlying logic. Using HIMP, a C-like language with dynamic memory allocation/deallocation and pointer arithmetic, this paper shows how one can derive an executable matching logic verifier from HIMP’s RLS. It is shown that the derived verifier is sound, that is every verified formula holds in the original, complementary RLS of HIMP, and complete, that is every verified formula is provable using HIMP’s sound matching logic proof system. In passing, this paper also shows that, for the restriction of HIMP without a heap called IMP for which one can give a conventional Hoare logic proof system, a restricted use of the matching logic proof system is equivalent to the Hoare logic proof system, in that any proof derived using any of the proof systems can be turned into a proof using the other. The encoding from Hoare logic into matching logic is generic and should work for any Hoare logic proof system. A matching logic verifier, called MatchC, has been built on top of the Maude rewrite system. A nontrivial MatchC case study is discussed, namely the verification of the partial correctness of the Schorr-Waite algorithm (with graphs). The verifier automatically generated and proved all 227 paths in 16 seconds.
---
paper_title: A rewriting approach to the design and evolution of object-oriented languages

paper_content:

Rewriting logic semantics provides an environment for defining new and existing languages. These language definitions are formal and executable, providing language interpreters almost for free while also providing a framework for building analysis tools, such as type checkers, model checkers, and abstract interpreters. Large subsets of several existing object-oriented languages have been defined, while a new research language, KOOL, has been created as a platform for experimenting with language features and type systems. At the same time, new tools and formalisms aimed specifically at programming languages are being developed.
---
paper_title: Towards a Module System for K

paper_content:

Research on the semantics of programming languages has yielded a wide array of notations and methodologies for defining languages and language features. An important feature many of these notations and methodologies lack is modularity: the ability to define a language feature once, insulating it from unrelated changes in other parts of the language, and allowing it to be reused in other language definitions. This paper introduces ongoing work on modularity features in K, an algebraic, rewriting logic based formalism for defining language semantics.
---
paper_title: On Formal Analysis of OO Languages Using Rewriting Logic: Designing for Performance

paper_content:

Rewriting logic provides a powerful, flexible mechanism for language definition and analysis. This flexibility in design can lead to problems during analysis, as different designs for the same language feature can cause drastic differences in analysis performance. This paper describes some of these design decisions in the context of KOOL, a concurrent, dynamic, object-oriented language. Also described is a general mechanism used in KOOL to support model checking while still allowing for ongoing, sometimes major, changes to the language definition.
---
paper_title: Computing with Membranes

paper_content:

We introduce a new computability model, of a distributed parallel type, based on the notion of a membrane structure. Such a structure consists of several cell-like membranes, recurrently placed inside a unique “skin” membrane. A plane representation is a Venn diagram without intersected sets and with a unique superset. In the regions delimited by the membranes there are placed objects. These objects are assumed to evolve: each object can be transformed in other objects, can pass through a membrane, or can dissolve the membrane in which it is placed. A priority relation between evolution rules can be considered. The evolution is done in parallel for all objects able to evolve. In this way, we obtain a computing device (we call it a P system): start with a certain number of objects in a certain membrane and let the system evolve; if it will halt (no object can further evolve), then the computation is finished, with the result given as the number of objects in a specified membrane. If the development of the system goes forever, then the computation fails to have an output. We prove that the P systems with the possibility of objects to cooperate characterize the recursively enumerable sets of natural numbers; moreover, systems with only two membranes suffice. In fact, we do not need cooperating rules, but we only use catalysts, specified objects which are present in the rules but are not modified by the rule application. One catalyst suffices. A variant is also considered, with the objects being strings over a given alphabet. The evolution rules are now based on string transformations. We investigate the case when either the rewriting operation from Chomsky grammars (with respect to context-free productions) or the splicing operation from H systems investigated in the DNA computing is used. In both cases, characterizations of recursively enumerable languages are obtained by very simple P systems: with three membranes in the rewriting case and four in the splicing case. Several open problems and directions for further research are formulated
---
paper_title: Runtime Verification of C Memory Safety

paper_content:

C is the most widely used imperative system's implementation language. While C provides types and high-level abstractions, its design goal has been to provide highest performance which often requires low-level access to memory. As a consequence C supports arbitrary pointer arithmetic, casting, and explicit allocation and deallocation. These operations are difficult to use, resulting in programs that often have software bugs like buffer overflows and dangling pointers that cause security vulnerabilities. We say a C program is memory safe, if at runtime it never goes wrong with such a memory access error. Based on standards for writing "good" C code, this paper proposes strong memory safety as the least restrictive formal definition of memory safety amenable for runtime verification. We show that although verification of memory safety is in general undecidable, even when restricted to closed, terminating programs, runtime verification of strong memory safety is a decision procedure for this class of programs. We verify strong memory safety of a program by executing the program using a symbolic, deterministic definition of the dynamic semantics. A prototype implementation of these ideas shows the feasibility of this approach.
---
paper_title: Formal analysis of java programs in javafan

paper_content:

JavaFAN is a Java program analysis framework, that can symbolically execute multithreaded programs, detect safety violations searching through an unbounded state space, and verify finite state programs by explicit state model checking. Both Java language and JVM bytecode analyses are possible. JavaFAN's implementation consists of only 3,000 lines of Maude code, specifying formally the semantics of Java and JVM in rewriting logic and then using the capabilities of Maude for efficient execution, search and LTL model checking of rewriting theories.
---

Title: An overview of the K semantic framework

Section 1: Introduction
Description 1: Provide an introduction to the K semantic framework, its origins, applications, and motivation.

Section 2: Rewriting Frameworks
Description 2: Discuss various rewriting approaches used for programming language semantics, including term rewriting, rewriting logic, graph rewriting, chemical abstract machines, and P-systems, and their relationship to K.

Section 3: K Overview by Example
Description 3: Describe the K framework using examples, specifically focusing on the IMP and IMP++ languages, including their executable semantics and type systems.

Section 4: K Semantics of IMP
Description 4: Detail the semantics of the IMP language within the K framework, including the definition of configurations and computational structures.

Section 5: K Semantics of IMP++
Description 5: Expand upon the semantics of IMP++ within the K framework, discussing extensions like output, halt, and thread spawning.

Section 6: K Type System for IMP/IMP++
Description 6: Discuss the type system for IMP/IMP++ using K, defining type-checking rules and ensuring well-typed programs.

Section 7: The K Concurrent Rewrite Abstract Machine
Description 7: Present the Kram, its preliminaries, and how it captures true concurrency, including the definition of K-rules and K-transactions.

Section 8: K-rules and K-systems
Description 8: Elaborate on K-rules, their relation to rewrite rules, and the concept of maximal data-sharing in K-systems.

Section 9: K-Transactions
Description 9: Define K-transactions, the process of concurrent application of multiple K-rules, and how K-transactions differ from standard rewrite rule applications.

Section 10: The K Technique
Description 10: Introduce the guidelines and notations of the K technique for defining programming languages or calculi, emphasizing its flexibility and modularity.

Section 11: K Configurations: Nested Cell Structures
Description 11: Explain the abstract definition and practical importance of configurations in K, represented as nested cell structures.

Section 12: K Computations: Extended Abstract Syntax
Description 12: Define K computations, their role in the K framework, and how they extend abstract syntax with a nested-list structure.

Section 13: K Rules: Computational and Structural
Description 13: Distinguish between computational and structural K rules, explaining their impact on language definitions and evaluation strategies.

Section 14: Strictness Attributes
Description 14: Discuss how strictness attributes in K help define evaluation strategies by automating the generation of heating/cooling rules.

Section 15: Context Transforming
Description 15: Introduce the concept of context transforming in K, which enhances modularity by adapting rules to new configurations.

Section 16: The Locality Principle
Description 16: Explain the locality principle in context transforming, ensuring rules fit as deeply as possible within the target configuration.

Section 17: The Cell-Cloning Principle
Description 17: Describe the cell-cloning principle, which allows rules to apply to multiple instances of the same cell type based on cloning information.

Section 18: The Challenge Language Definition
Description 18: Present a complete definition of the Challenge language, showcasing the benefits of using the K framework for defining complex programming languages.

Section 19: Conclusion, Current Work, and Future Work
Description 19: Summarize the advantages of the K semantic framework, current research projects, and future directions for development and application.