Program of FOSSACS

MONDAY 2/4
 9.30
10.30

Session chair: Furio Honsell
Gordon Plotkin (Invited lecture)
11.00
12.30
Concurrency and Mobility
Session chair: Luca Cardelli

Secrecy Types for Asymmetric Communication
Martin Abadi (Bell Labs Research),
Bruno Blanchet (INRIA Rocquencourt)

High-Level Petri Nets as Type Theories in the Join Calculus
Maria Grazia Buscemi, Vladimiro Sassone (Università di Catania)

The Complexity of Model Checking Mobile Ambients
Witold Charatonik (Max-Planck-Institut für Informatik and University of Wroclaw)
Silvano Dal Zilio, Andrew D. Gordon (Microsoft Research),
Supratik Mukhopadhyay, Jean-Marc Talbot (Max-Planck-Institut für Informatik)

15.00
17.00
Type Theory
Session chair: Pawel Urzyczyn

Type inference with recursive type equations
Mario Coppo (Università di Torino)

Axioms for Recursion in Call-by-Value
Masahito Hasegawa, Yoshihiko Kakutani (Kyoto University)

Type Isomorphisms and Proof Reuse in Dependent Type Theory
Gilles Barthe (INRIA), Olivier Pons (Universidade do Minho)

The Rho Cube
Horatiu Cirstea (LORIA and UHP), Claude Kirchner (LORIA and INRIA), Luigi Liquori (LORIA and INPL)

17.30
19.00
Formal Verification
Session chair: Carolyn Talcott

Verified Bytecode Verifiers
Tobias Nipkow (Technische Universität München)

Higher-Order Abstract Syntax with Induction in Isabelle/HOL:
Formalizing the Pi-Calculus and Mechanizing the Theory of Contexts

Christine Röckl (Technische Universität München),
Daniel Hirschkoff (LIP, ENS de Lyon),
Stefan Berghofer (Technische Universität München)

Marrella and the Verification of an Embedded System (DEMO)
Dominique Ambroise, Patrick Auge (Université de Paris Sud),
Kamel Bouchefra (Université Paris 13),
Brigitte Rozoy (Université de Paris Sud)

TUESDAY 3/4
10.30
12.30
Automata
Session chair: Pierre Lescanne

On the Complexity of Parity Word Automata
Valerie King (University of Victoria),
Orna Kupferman (Hebrew University),
Moshe Vardi (Rice University)

On the Modularity of Deciding Call-by-Need
Irèene Durand (Université Bordeaux I),
Aart Middeldorp (University of Tsukuba)

On the Decidability of the Finite Model Problem
Mikolaj Bojanczyk (Warsaw University)

Axiomatizing Tropical Semirings
Luca Aceto (Aalborg University),
Zoltan Esik (A. Jozsef University, Szeged),
Anna Ingólfsdóttir (Aalborg University)

16.00
17.00
Automata and Language
Session chair: Colin Stirling

On Rational Message Sequence Chart Languages and Relationships to Mazurkiewicz Trace Theory
Remi Morin (TU-Dresden)

Synchronized Tree Languages Revisited and New Applications
Valerie Gouranton (Université d'Orléans),
Pierre Rety (Université d'Orléans),
Helmut Seidl (University of Trier)

17.30
19.00
Categorical Foundations
Session chair: Bart Jacobs

On the Duality between Observability and Reachability
Michel Bidoit (CNRS & ENS de Cachan),
Rolf Hennicker (Ludwig-Maximilians-Universität München),
Alexander Kurz (CWI, Amsterdam)

Foundations for a Graph-Based Approach to the Specification of Access Control Policies
Manuel Koch (PSI AG),
Luigi Vincenzo Mancini, Francesco Parisi-Presicce (Univ. Roma "La Sapienza")

Coalgebra of Abstract Processes
Sava Krstic, John Launchbury (Oregon Graduate Institute),
Dusko Pavlovic (Kestrel Institute)

WEDNESDAY 4/4
10.30
12.30
Transition Systems
Session chair: Ugo Montanari

Decidability of Weak Bisimilarity for a Subset of Basic Parallel Processes
Colin Stirling (Edinburgh University)

Temporary Data in Shared Dataspace Coordination Languages
Nadia Busi, Roberto Gorrieri, Gianluigi Zavattaro (Università di Bologna)

Model Checking CTL+ and FCTL is Hard
Francois Laroussinie, Nicolas Markey, Philippe Schnoebelen (CNRS, ENS de Cachan)

Computational Completeness of Programming Languages Based on Graph Transformation
Annegret Habel (Universitaet Oldenburg),
Detlef Plump (The University of York)

17.30
19.00
Semantics
Session chair: Mariangiola Dezani

On Garbage and Program Logic
Peter W. O'Hearn (Queen Mary and Westfield College, London),
Cristiano Calcagno (QMW College, London, and Università di Genova)

Class Analysis of Object-Oriented Programs through Abstract Interpretation
Thomas Jensen, Fausto Spoto (IRISA, France)

An Axiomatic Semantics for the Synchronous Language Gentzen
Simone Tini (Università di Pisa)