|
|
| SOS Workshop |
|
||
| August 30, 2004 | ||
| London, England | ||
| Held in conjunction with the conference CONCUR 2004. |
|
|
| Author | Title/Abstract |
|---|---|
| Rob van Glabbeek | The Meaning of Negative Premises: Part II |
| This tutorial reviews several methods to associate transition relations to transition system specifications with negative premises. Besides a formal comparison on generality and relative consistency, the methods are also evaluated on their taste in determining which specifications are meaningful and which are not. Additionally, it presents a proof theoretic characterisation of the well-founded semantics for logic programs. | |
| Andrew Pitts | Equivariant and Nominal SOS |
|
Many kinds of names occurring in programming languages and logical
calculi are "atomic", in the sense that the structure of a name is
immaterial: all that matters are distinctions between names and the
association of names to the things named. One says that a semantic
construct involving such atomic names is "equivariant" if its meaning
is preserved under the operation of permuting the atoms. A simple, but
useful, result about finitary inductive definitions shows that
equivariant relations already abound for structural operational
semantics carried out in ordinary (naive) set theory. However, to
really exploit the power of this permutation-oriented viewpoint for
general inductive and co-inductive definitions (such as occur in
concurrency theory) and for modelling locality and abstraction of
names, requires a modest change of foundation to "nominal sets". This
is a mathematical framework with names as atoms that makes
equivariance ubiquitous and can express the crucial property of
"freshness" of names in a syntax-independent way.
In this talk I will discuss equivariance in SOS and give an introduction to the use of nominal sets for semantics. |
|
| David Sands | TBA |
| Author(s) | Title/Abstract |
|---|---|
| Marija Kulas | Toward the concept of backtracking computation |
| This article proposes a new mathematical definition of the execution of pure Prolog, in the form of axioms in a structural operational semantics. The main advantage of the model is its ease in representing backtracking, due to the functionality of the transition relation and its converse. Thus, forward and backward derivation steps are possible. A novel concept of stages is introduced, as a refinement of final states, which captures the evolution of a backtracking computation. An advantage over the traditional stack-of-stacks approaches is a modularity property. Finally, the model combines the intuition of the traditional `Byrd box' metaphor with a compact representation of execution state, making it feasible to formulate and prove theorems about the model. In this paper we introduce the model and state some useful properties. | |
| Matthias Mann | Congruence of Bisimulation in a Non-Deterministic Call-By-Need Lambda Calculus |
|
We present a call-by-need lambda-calculus Lambda-ND with an erratic
non-deterministic operator pick and a non-recursive let. A definition
of a bisimulation is given, which has to be based on a further
calculus named Lambda-Approx, since the naive bisimulation definition
is useless. The main result is that this bisimulation is a congruence
and coincides with the contextual equivalence.
The proof is a non-trivial extension of Howe's method. This might be a step towards in defining useful bisimulation relations and proving them to be congruences in calculi that extend the Lambda-ND-calculus. | |
| Olivier Tardieu | A Deterministic Logical Semantics for Esterel |
| Esterel is a synchronous design language for the specification of reactive systems. There exist two main semantics for Esterel. On the one hand, the logical behavioral semantics provides a simple and compact formalization of the behavior of programs using SOS rules. But it does not ensure deterministic executions for all programs and all inputs. As non-deterministic programs have to be rejected as incorrect, this means it defines behaviors for incorrect programs, which is not convenient. On the other hand, the constructive semantics is deterministic (amongst other properties) but at the expense of a much more complex formalism. In this work, we construct and thoroughly analyze a new deterministic semantics for Esterel that retains the simplicity of the logical behavioral semantics, from which it derives. In our view, it provides a much better framework for formal reasoning about Esterel programs. |
| Author(s) | Title/Abstract |
|---|---|
| Bartek Klin | TBA |
| Ralf Laemmel | Evolution of Rule-Based Programs |
| Peter Mosses | Modular Structural Operational Semantics |
Last modified: Friday, 09-Jul-2004 12:46:21 CEST.