11h00-12h00 Dale Miller, CSE, Penn State
(joint work with Raymond McDowell and Catuscia Palamidessi)
Encoding Generic Judgments
Operational semantics is often presented in a rather syntactic
fashions using relations specified by inference rules or equivalently
by logic programming clauses in a suitable meta-logic. As is well
known, the specifications involving syntactic objects containing bound
variables can be greatly eased if that meta-logic has its own,
generic notion of binder that is available to the specification.
We shall attempt to extend this specificational setting to include the
problem of specifying not only relations capturing operational
semantics, such as one-step evaluation, but also properties and
relations about such semantics, such as simulation.
We shall do this by staying within a suitable meta-logic and provide a
presentation that is still centered around syntactic considerations.
We shall use the $\pi$-calculus to help illustrate our approach.
14h00-14h45 Jeremie Wajs, CSE Penn State
Reasoning about logic programs
In this talk, we will exhibit work revolving around the FOLDN framework
defined by Raymond McDowell and Dale Miller [LICS'97]. After going over
some of the background work on FOLDN, we will show how FOLDN can be used
for performing program transformations on Horn Clause definitions, and
study the effects of performing such program transformations on
definitions and on FOLDN proofs in general.
This work makes use of rich induction principles to produce simpler
proofs, such as one derived from Sorin Craciunescu's work [JFPLC'01].
14h45-15h30 Sorin Craciunescu, INRIA Rocquencourt
A Soundness Proof of a Formal System for Equivalence of Logic Programs
In this talk we will present the proof of soundness for a formal system
for equivalence proofs of logic programs.
The language for these programs is the classical CLP to which the
universal quantifier is added. The system is based on classical logic
and can be used in conjunction with a proof system for specific domain
of constraints. We use an induction rule for proving success equivalence
and a coinduction one for finite failure equivalence.
The soundness is proved with respect to classical semantics for
successes and its dual for finite failures.
11h00-12h00 Catuscia Palamidessi, CSE, Penn State
(joint work with Oltea Mihaela)
Challenges and Promising Directions in the Distributed Implementation of Choice
We consider the problem of implementing the Mixed Guarded Choice
mechanism that exists in process calculi like, for instance, the pi-calculus.
We
show that an exact solution does not exist, and we focus therefore on randomized
solutions. We review some of the algorithms proposed in literature and we
argue
about their limitations connected to the lack of robustness wrt arbitrary
schedulers. Finally, we propose a solution which works in some particular
connection topologies, under any scheduler, and a solution which works in
any
topology, under the fairness assumption.
14h00-14h45 Frank Valencia, BRICS, Aarhus, Danemark
Joint work with Catuscia Palamidessi (CSE, Penn State, USA)
A Calculus for Temporal Constraint Programming
The tcc model is a concurrent constraint formalism for
synchronous and deterministic timed computation. In this talk
we will describe a model, which we call the ntcc calculus,
adding to tcc the capability of modeling asynchronous and
non-deterministic temporal behavior.
The expressiveness of ntcc is illustrated by modeling cells and
asynchronous bounded broadcasting, by specifying temporal requirements
such as response and invariance, and by modeling timed systems
such as RCX controllers. We will present a denotational semantics
for modeling the strongest-postcondition behavior of ntcc processes,
and, based on this semantics, we will present a proof system for
proving linear temporal properties of these processes.
We will also describe work on progress. Preliminary results show that
the problem of deciding whether to programs are (input-output)
equivalent under all possible contexts is decidable for nondeterministically
bounded processes. Finally, we will talk about an extension of ntcc to a
probabilistic model following ideas in \cite{Palamidessi:00:FoSSaCS}. This
is
justified by the existence of RCX examples involving stochastic behavior.
14h45-15h30 Lionel Kalill, ENS Paris
(joint work with Maribel Fernandez)
Reseaux d'interaction avec ambiguite
We will present an extension of interaction nets with a non-deterministic agent analogous to McCarthy's amb operator. In this extension of interaction nets we are able to encode non-sequential functions, such as parallel-or or Berry's function. More generally, we will discuss the encoding in this formalism of general constructor term rewriting systems, and we will show that interaction nets with amb can express angelic merge and infinity merge but not fair merge.