11h00-12h00 Dale Miller, CSE, Penn State
(joint work with Raymond McDowell and Catuscia Palamidessi)
Encoding Transition Systems in Sequent Calculus
Abstract. Intuitionistic and linear logics can be used to specify
the
operational semantics of transition systems in various ways.
We
consider here two encodings: one uses linear logic and maps states
of
the transition system into formulas, and the other uses intuitionistic
logic and maps states into terms. In both cases, it is possible
to
relate transition paths to proofs in sequent calculus. In neither
encoding, however, does it seem possible to capture properties, such
as simulation and bisimulation, that need to consider all possible
transitions or all possible computation paths. We consider augmenting
both intuitionistic and linear logics with a proof theoretical
treatment of definitions. In both cases, this addition allows
proving
various judgments concerning simulation and bisimulation (especially
for noetherian transition systems). We also explore the use of
infinite proofs to reason about infinite sequences of transitions.
Finally, combining definitions and induction into sequent calculus
proofs makes it possible to reason more richly about properties of
transition systems completely within the formal setting of sequent
calculus.
This paper is to appear in Theoretical Computer Science. It can
be
found at ftp://ftp.cse.psu.edu/pub/dale/tcs97.ps.gz
14h00-14h45 Jeremie Wajs, CSE Penn State
(joint work with Dale Miller)
A theorem prover for operational semantics
We describe a new theorem prover that we plan to use to reason about
the operational semantics of programs and programming languages,
although it should have wider applications.
At the core of this prover is a sequent calculus that extends
intuitionistic logic with introduction rules for natural number
induction and definitions. Several papers report on initial experiments
on
using this logic, called FOLDN, to reason about computation.
These
experiments profit significantly from the availability of higher-order
abstract syntax in coding up computations.
Recent work on the logic of operational semantics suggests that
different logics can be productively used to assist in encoding
different kinds of computation paradigms. For example, intuitionistic
linear logic has been used to encode references and state
encapsulation, while classical linear logic provides natural ways to
encode concurrency. We describe how these various object logics
can be
encoded into this theorem prover and show via several examples how
we can reason about a number of aspects of computation.
This theorem prover is being prototyped in the Teyjus implementation
of Lambda Prolog. Our prover is thus able to capitalize on such
recent
technologies as explicit substitutions, efficient term representation,
backtracking, and dynamic scoping of program elements since the Teyjus
compiler and runtime system contains all of these. We are also
using a
recent parser generator written for Lambda Prolog.
14h45-15h20 Sorin Craciunescu, INRIA Rocquencourt
Proofs by Coinduction for Logic Programs
Most of the existent proof systems for programs use the theory of inductive
types
where new axioms are introduced for recursive definitions. Some syntactical
termination conditions are used in order to guarantee the coherence
of the resulting system. Proofs systems based on induction do not have
the same
restrictions but they allow one to reason about terminating computations
only.
We present a proof system for logic programs based on coinduction
which permits the reasoning about terminating and non-terminating
computations. The proof system is presented as a sequent calculus
that has been directly implemented in Prolog
15h40-16h20 Sylvain Soliman, INRIA Rocquencourt
(joint work with François Fages and Rajeev Goré)
Semantics and Precision
After remarking that the observables that are addressed by the logical
semantics of Concurrent Constraint Programs are interesting for verification
purposes, but that the semantics characterizations are often approximative,
we try to refine the logical semantics to achieve an exact characterization
of
success stores of CC agents. Starting with a modal-logics approach
aimed at
distinguishing the constraints of the store from the constraints in
agents, we then
realize that it is not necessary to modify the original logic
(ILL) but only to enrich
the translation to obtain a more precise logical semantics.
11h00-12h00 Catuscia Palamidessi , CSE, Penn State
(joint work with David Gilbert)
Concurrent Constraint Programming with Process Mobility
Abstract. We propose an extension of concurrent constraint programming
with primitives for process migration within a hierarchical network,
and we study its semantics.
To this purpose, we first investigate a ``pure'' paradigm for process
migration, namely a paradigm where the only actions are those dealing
with transmissions of processes. Our goal is to give a structural
definition of the semantics of migration; namely, we want to describe
the behaviour of the system, during the transmission of a process,
in
terms of the behaviour of the components. We achieve this goal
by
using a labeled transition system where the effects of sending a
process, and requesting a process, are modeled by symmetric rules
(similar to handshaking-rules for synchronous communication) between
the two partner nodes in the network.
Next, we extend our paradigm with the primitives of concurrent
constraint programming, and we show how to enrich the semantics
to cope with the notions of environment and constraint store.
Finally, we show how the operational semantics can be used
to define an interpreter for the basic calculus.
14h00-14h45 Oltea Mihaela Herescu, CSE, Penn State.
(joint work with Catuscia Palamidessi)
Probabilistic Asynchronous Pi-Calculus
Abstrcat. We propose an extension of the asynchronous pi-calculus with
a notion of
random choice. We define an operational semantics which distinguishes
between probabilistic choice, made internally by the process, and
nondeterministic choice, made externally by an adversary scheduler.
This
distinction will allow us to reason about the probabilistic correctness
of algorithms under certain schedulers. We show that in this language
we
can solve the electoral problem, which was proved not possible in the
asynchronous pi-calculus. Finally, we show an implementation of the
probabilistic asynchronous pi-calculus in a Java-like language.
14h45-15h30 Lionel Khalil, ENS Paris
(joint work with Maribel Fernandez)
Generalization of Interaction Nets with a Unique Parallel Agent
The purpose of this generalisation is to give parallel property
to the Interaction nets. This generalisation is based on
the addition of a unique agent to the classic Interaction nets.