From: Gerard Boudol <Gerard.Boudol@sophia.inria.fr>
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.