Invited Paper

Adequacy for Algebraic Effects

Gordon Plotkin

John Power

Contributed Papers

Secrecy Types for Asymmetric Communication

Martin Abadi

Bruno Blanchet

Axiomatizing Tropical Semirings

Luca Aceto

Zoltan Esik

Anna Ingolfsdottir

Type Isomorphisms and Proof Reuse in Dependent Type Theory

Gilles Barthe

Olivier Pons

On the Duality between Observability and Reachability

Michel Bidoit

Rolf Hennicker

Alexander Kurz

The Finite Graph Problem for Two-Way Alternating Automata

Mikolaj Bojanczyk

High-Level Petri Nets as Type Theories in the Join Calculus

Maria Grazia Buscemi

Vladimiro Sassone

Temporary Data in Shared Dataspace Coordination Languages

Nadia Busi

Roberto Gorrieri

Gianluigi Zavattaro

On Garbage and Program Logic

Cristiano Calcagno

Peter W. O'Hearn

The Complexity of Model Checking Mobile Ambients

Witold Charatonik

Silvano Dal Zilio

Andrew D. Gordon

Supratik Mukhopadhyay

Jean-Marc Talbot

The Rho Cube

Horatiu Cirstea

Claude Kirchner

Luigi Liquori

Type Inference with Recursive Type Equations

Mario Coppo

On the Modularity of Deciding Call-by-Need

Irene Durand

Aart Middeldorp

Synchronized Tree Languages Revisited and New Applications

Valerie Gouranton

Pierre Rety

Helmut Seidl

Computational Completeness of Programming Languages Based on Graph Transformation

Annegret Habel

Detlef Plump

Axioms for Recursion in Call-by-Value (Extended Abstract)

Masahito Hasegawa

Yoshihiko Kakutani

Class Analysis of Object-Oriented Programs through Abstract Interpretation

Thomas Jensen

Fausto Spoto

On the Complexity of Parity Word Automata

Valerie King

Orna Kupferman

Moshe Y. Vardi

Foundations for a Graph-Based Approach to the Specification of Access Control Policies

Manuel Koch

Luigi Vincenzo Mancini

Francesco Parisi-Presicce

Categories of Processes Enriched in Final Coalgebras

Sava Krstic

John Launchbury

Dusko Pavlovic

Model Checking CTL+ and FCTL Is Hard

Francois Laroussinie

Nicolas Markey

Philippe Schnoebelen

On Regular Message Sequence Chart Languages and Relationships to Mazurkiewicz Trace Theory

Remi Morin

Verified Bytecode Verifiers

Tobias Nipkow

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

Christine Rockl

Daniel Hirschkoff

Stefan Berghofer

Decidability of Weak Bisimilarity for a Subset of Basic Parallel Processes

Colin Stirling

An Axiomatic Semantics for the Synchronous Language Gentzen

Simone Tini

Tool Presentation

MARRELLA and the Verification of an Embedded System

Dominique Ambroise

Patrick Auge

Kamel Bouchefra

Brigitte Rozoy

Author Index