Workshop: Logic Programming and Concurrency
Marseille
February 27 - March 3, 2006
Presentation
Logic programming, in the sense of proof search in sequent calculus,
has been used to describe the operational semantics of concurrent
computational systems in at least two distinct fashions.
In the process-as-term approach, process combinators and relations
between them (one-step, bisimulation, etc), are encoded as non-logical
primitives, whose axiomatization is provided by structured operational
semantics (SOS). Here, classical and intuitionistic logics are
generally used in such axiomatizations. Recent challenges in this
setting have been capturing both may and must properties of processes,
uncovering declarative approaches to link mobility, and exploiting
evident connections to model checking and game semantics.
In the process-as-formula approach, process combinators are encoded
directly as logical connective and the operational semantics of
processes is provided directly by an underlying logic, such as linear
logic. Such encodings have been most successfully employed to date
with asynchronous process calculi. Recent challenges here have been
finding ways to exploit the meta-theory of linear logic to provide
results about processes and declarative approaches to sequentiality
and security protocols. This workshop will focus on examining various
connections between concurrent computation and the proof search
paradigm, whether or not that connection falls neatly into the above
mentioned approaches.
Programme
Note: The two talks by Dale Miller are independent.
Abstracts
-
David Baelde,
LIX, Ecole Polytechnique
Title: Linear logic and process algebras
Abstract:
Following the process-as-formula approach, we'll present in this talk
the strong relations between the dynamics of asynchronous pi-calculus
and linear logic proof search, and see how this kind of result can be
extended to other well-known concurrency calculi like Join-calculus
and even synchronous pi-calculus. We then try to outline possible
applications of such relations.
-
Christophe Fouqueré and
Virgile Mogbil,
LIPN - Paris 13
Title: Logic Programming revisited
Abstract:
We consider a polarized version of proofnets we call binary
modules. This slight modification does not change anything to the
logical theory underlining proofnets. However, we will show that the
proof search process becomes natural in this respect. Binary modules
are combination of elementary ones, each representing some clause of
the program. We first consider computation on elementary modules able
to represent the progression principle as well as its dual part as a
resource-conscious Prolog style ALPL. We prove that this fragment
does not need any correctness criteria except unification for applying
the computation principle. In a second section, we mix the previous
situation and its dual one. This allows us to model disjunctiv e
linear programs. Once again, no correctness criteria are necessary.
We then extend it to the full multiplicative linear logic without
exponentials, hence including necessarily correctness criteria to deal
with parallelism. Finally, we present an extension where exponentials
are partially allowed.
-
Deepak Garg,
Carnegie Mellon University
Title: Focussing in Proof-search and Concurrent Synchronization
Abstract:
In recent work we have showed that the asynchronous pi-calculus can be
encoded in a variant of intuitionistic first-order linear logic using
a process-as-formula approach, where processes are encoded directly as
formulas of the logic, and the dynamic semantics of the pi-calculus
are simulated through a combination of backward proof-search and
forward chaining. We showed that focussing during backward
proof-search plays a critical role in this encoding because it makes
simulation of message reception atomic in the logic. We build upon
this work, and show how focussing can be used to simulate other
synchronization behavior in the asynchronous pi-calculus, including a
specific form of external choice and simultaneous n-way message
reception. This allows us to translate a very expressive extension of
the asynchronous pi-calculus into linear logic. We expect that this
extension is as expressive as the synchronous pi-calculus with
external choice. We describe correctness results for the encoding, and
use the encoding to demonstrate a direct correspondence between
process-calculi combinators and the connectives of intuitionistic
linear logic.
-
Dale Miller I,
INRIA-Futurs and LIX, Ecole Polytechnique
Title: A Proof Theoretic Approach to Operational Semantics
Abstract:
Proof theory can be applied to the problem of specifying and reasoning
about the operational semantics of process calculi. We overview some
recent research in which lambda-tree syntax is used to encode
expressions containing bindings and sequent calculus is used to reason
about operational semantics. There are various benefits of this proof
theoretic approach for the pi-calculus: the treatment of bindings
can be captured with no side conditions; bisimulation has a simple and
natural specifications in which the difference between bound input and
bound output is given by changing a quantifier; various modal logics
for mobility can be specified declaratively; and simple logic
programming-like deduction involving subsets of second-order
unification provides immediate implementations of symbolic
bisimulation. These benefits should extend to other process calculi
as well. As partial evidence of this, a simple lambda-tree syntax
extension to the tyft/tyxt rule format for name-binding and
name-passing has been made that allows one to conclude that (open)
bisimilarity is a congruence.
Joint work with Alwen Tiu, Axelle Zeigler, and Catuscia Palamidessi.
-
Dale Miller II,
INRIA-Futurs and LIX, Ecole Polytechnique
Title: A game semantics for proof search: Preliminary results
Abstract:
We describe an ongoing project in which we attempt to describe a
neutral approach to proof and refutation. In particular, we present a
language of neutral expressions which contains one element for
each de Morgan pair of connectives in (linear) logic. Our goal is
then to describe, in a neutral fashion, what it means to prove or
refute. For this, we use games where moves are described as
transitions between positions built with neutral expressions. We can
then relate winning a game with provability. More precisely we relate
winning strategies for an expression N with proofs for a linear
logic formula obtained from N: to winning
exists-forall-strategies for N we associate proofs of the
positive (synchronous) translation of N into logic. On the other
hand, to winning forall-exists-strategies for N we associate
proofs of the negative (asynchronous) translation of N into logic.
This work is joint with Alexis Saurin. This abstract is based on a
paper presented at Mathematical Foundations of Programming
Semantics (MFPS) 2005.
-
Frank Pfenning,
Carnegie Mellon University
Title: Spurious Causal Dependency and Proof Irrelevance
Abstract:
In recent work we have proposed a logic programming language integrating
Prolog-style backward chaining and committed choice forwarded chaining.
Its formal foundation is CLF, a linear dependent type theory with a
monad for concurrency. Its definitional equality is intended to
identify concurrent computations that differ only in the order of
independent events, thereby modeling true concurrency.
We have observed a class of examples, including Petri nets, some
planning domains, and shared memory imperative computation, where the
framework's definitional equality is too weak to capture all desired
equivalences. For example, a straightforward representation of shared
memory distinguishes different orders of concurrent read operations,
in effect imposing a spurious causal dependency.
We discuss how this problem might be addressed to obtain more
satisfactory representations. Techniques include the explicit
definition of an equivalence as part of the representation, and
exploiting an extension of CLF with proof irrelevance currently
under development.
Joint work with Ruy Ley-Wild.
-
Lutz Straßburger,
INRIA-Futurs
Title: Noncommutativity and Exponentials in the Calculus of
Structures
Abstract:
It has been observed recently, that the sequent calculus cannot capture a
simple self-dual noncommutative connective. In this talk I present a
logic which conservatively extends multiplicative exponential linear logic
(plus mix) by this new connective. Although this logic cannot be presented in
the sequent calculus, it has a natural presentation in the calculus of
structures. Interestingly, we can observe a new property, called
"decomposition", that exhibits certain, hitherto unknown properties
of the exponentials of linear logic. Decomposition also allows to take a new
approach towards cut elimination.
Joint work with Alessio Guglielmi
-
Axelle Ziegler,
LIX, Ecole Polytechnique
Title: TBA
Abstract:
TBA
Organization
Organizers:
Dale Miller
and
Lutz Straßburger.
Context: This workshop is part of Geometry of Computation 2006 (
Geocal06), a special series of
events in theoretical computer science organized by the
GEOCAL group and taking
place at the
CIRM from January 30 to
March 3, 2006. Geocal06 is supported by the following institutions:
IML,
FRUMAM,
Luminy,
UnivMed,
Genopole,
CIRM,
CNRS.