Description of the Main Courses
-
Interaction Categories
Samson
Abramsky, Dept. of Computer Science,
University of Edimburgh,
Edimburgh, UK
-
The Interaction Category paradigm for semantics
is a radical revision of the classical denotational paradigm for
semantic universes (categories), in which the types (objects)
are structured sets (e.g. domains), the program denotations (morphisms)
are functions, and composition is function composition.
Interaction categories have specifications as objects,
processes as morphisms, and interaction as composition.
The overall effect
is that process calculus in the CCS/CSP tradition is reconstituted
in functorial form, and integrated with type theory and functional
programming.
Another dimension of the theory is motivated by the problem: how to
combine the Propositions-as-Types and Verification paradigms smoothly in
a single framework. We propose a general solution, based on the
notion of specification structures. These general ideas are then applied
to Interaction Categories, and illustrated with a number of examples.
Firstly, a specification structure for
liveness properties is described. This allows a new and conceptually
satisfying treatment of the thorny old problem of fairness.
Secondly, a specification structure supporting a compositional treatment
of deadlock-freedom is described. This combines ideas from concurrency
theory and Linear realizability (orthogonality).
In this fashion, we obtain a working version of the Propositions-as-Types
paradigm for concurrency, in which the standard typing rule for
composition (in logical terms, the Cut rule of sequent calculus)
plays the role of a compositional proof rule for parallel composition.
- Probabilistic Theories and Methods for
Concurrency
Prakash Panangaden,
Dept. of Computer Science,
Mc Gill University,
Montreal,
Ca
-
(List of topics.) Basics in measure theory and probability. Stochastic processes and Markov
processes. Some categories and monads that arise in probability theory.
Probabilistic relations. Bisimulation for Markov processes. Kozen's
Probabilistic semantics and probabilistic version of Stone duality.
Probabilistic powerdomains d'apres Jones and Plotkin.
-
An introduction to the pi-calculus
Davide Sangiorgi,
INRIA, Sophia-Antipolis, Fr
-
Process calculi are formalisms for the description and analysis of
concurrent activities. The pi-calculus is emerging as one of the
most influential of such calculi. The pi-calculus naturally models
systems with a changing structure. It can be used as a
metalanguage for a variety of languages ranging from functional to
imperative and to object-oriented. It is also being studied for the
design of new programming languages.
The pi-calculus will be introduced viewing it both as a basic model
of concurrent computations and as core programming language. Topics
that will be surveyed include: Algebraic theory; behavioural
equivalences and preorders; reasoning techniques; type systems;
applications. Some open problems will be discussed.
No special prerequisites are expected, but some familiarity with the
lambda-calculus and process algebras are welcome.
[Scope]
[Programme]
[Application]
[Grants]
[Accomodation]
[Travel]
[Main Page]
Last Updated: 27 April 1997
by Catuscia Palamidessi