From: Gerard Boudol
Subject: CONFER workshop programme
Dear All,
here is a (very) tentative programme for our CONFER workshop.
------------------------------------------------------------------------
Monday, September 14.
9h - 9h45 Martin Odersky: "The Join Calculus from a Functional Perspective"
9h45 - 10h30 Didier Remy: "From the Join-Calculus to a Class-Based,
Concurrent OO Language"
10h30 - 11h pause
11h - 11h30 Peter Sewell: "Communication Infrastructure for Mobile Agents:
Calculi for Algorithms"
11h30 - 12h Bjorn Victor: "Fusion Particles: Symmetrically Asynchronous
Mobile Processes"
12h - 14h lunch
14h - 14h45 Alain Deutsch: "Static Analysis of Concurrent Programs, with
Applications (Verification of the Ariane
Rocket's Programming)"
14h45 - 15h30 Ugo Montanari: "Final Semantics for the Pi-Calculus"
15h30 - 16h pause
16h - 16h45 Pascal Brisset: "Towards Certified Byte-Code Verification and
Proof-Carrying Code"
------------------------------------------------------------------------
Tuesday, September 15.
9h - 9h45 Marco Pistore: "Finite State Verification for the Asynchronous
Pi-Calculus"
9h45 - 10h30 Cedric Fournet (bisimulation and confluence?)
10h30 - 11h pause
11h - 11h30 Paul-Andre Mellies (games?)
------------------------------------------------------------------------
Some Abstracts:
Martin Odersky:
The talk will explore some variations how join calculus
can be regarded as a natural extension of traditional techniques
developed for the operational semantics of sequential programs.
Bjorn Victor:
encodings of prefix and summation in a calculus without
ANY prefix operator.
Ugo Montanari:
We show that the final semantics paradigm, originated
by Aczel and Rutten for CCS-like languages, can be successfully
applied also here. This is achieved by suitably generalizing the
standard techniques so as to accomodate the mechanism of name creation
and the behaviour of the binding operators peculiar to the
pi-calculus. As a preliminary step, we give a higher order
presentation of the pi-calculus using as metalanguage LF, a logical
framework based on typed lambda-calculus. Such a presentation
highlights the nature of the binding operators and elucidates the role
of free and bound channels. The final semantics is defined making use
of this higher order presentation, within a category of hypersets
(joint work with F. Honsell, M. Lenisa and M. Pistore).
Pascal Brisset:
We use the Coq proof-assistant to formally specify and
verify a virtual machine inpired from a small subset of Sun's Java
Virtual Machine. Topics covered include basic type safety, arrays,
simple exceptions and subroutines (objects and method invocation are
not handled yet). A byte-code verification algorithm is proved
correct with respect to the operational semantics and security policy
of the virtual machine. We also show how CMU's Proof-Carrying Code
technique can be safely integrated in this framework to remove
additional run-time checks.