16th European Symposium on Programming

Braga (Portugal), 24 March - 1 April, 2007



Call for Papers
Important Dates
Invited Speaker
Accepted Papers
Programme Committee
Steering Committee
ETAPS 2007


Accepted Papers

Conference Description

ESOP is a member conference of the European Joint Conferences on Theory and Practice of Software (ETAPS), which is the primary European forum for academic and industrial researchers working on topics relating to Software Science. ETAPS 2007 is the tenth joint conference in this series. The conference is organized by the Universidade do Minho. The prior conferences have been ETAPS 1998 in Lisbon, ETAPS 1999 in Amsterdam, ETAPS 2000 in Berlin, ETAPS 2001 in Genova, ETAPS 2002 in Grenoble, ETAPS 2003 in Warsaw, ETAPS 2004 in Barcelona, ETAPS 2005 in Edinburgh, and ETAPS 2006 in Vienna.

ESOP is an annual conference devoted to fundamental issues in the specification, analysis, and implementation of programming languages and systems. This includes:

  • Design of programming languages and calculi and their formal properties
  • Techniques, methods, and tools for their implementation
  • Exploitation of programming styles within different programming paradigms
  • Automatic and manual methods for generating and reasoning about programs
  • The design and invention of systems and tools to assist in exploitation of the languages

Contributions bridging the gap between theory and practice are particularly welcome. Topics traditionally covered by ESOP include programming paradigms and their integration, semantics, calculi of computation, security and privacy, advanced type systems, program analysis, program transformation, and practical algorithms based on theoretical developments.

Additional information about ESOP can be found at ESOP's home page.



The ETAPS conferences accept two types of contributions: research papers and tool demonstration papers. Both types of contributions will appear in the proceedings, published in the Springer-Verlag Lecture Notes in Computer Science series.

Submitted papers must:

  • be in English
  • present original research which is unpublished and not submitted for publication elsewhere; in particular, simultaneous submission of the same contribution to multiple ETAPS conferences is not permitted
  • be in the format specified by Springer-Verlag at the URL:
  • be submitted electronically in PDF format via the web site of ESOP Conference Service

    Papers submission deadline: Friday 13 October 2006 23.59 Samoa time (GMT -11)

Submissions not adhering to the specified format and length may be rejected immediately, without review. All papers, especially research papers, should clearly identify their novel contributions to the domain of fundamental approaches to software engineering. One author of each accepted paper must attend the conference to present the paper.

Research papers

Research papers should describe a novel contribution to the field. Final papers shall not be more than 15 pages long. Additional material intended for the referee, but not for publication in the final version (for example, details of proofs), may be placed in a clearly marked appendix that is not included in the page limit.

Tool demonstration papers

Tool demonstration papers should describe novel and state-of-the-art tools. Submissions should consist of two parts. The first part, no more than 4 pages, should describe the tool presented. Please include the URL of the tool (if available) and provide information that illustrates the maturity and robustness of the tool. This part will be included in the proceedings. The second part, no more than 6 pages, should explain how the demonstration will be carried out and what it will show, including screen dumps and examples. This part will not be included in the proceedings, but will be evaluated.

Important Dates

  • Friday 6 October 2006: Abstract submission
  • Friday 13 October 2006 23.59 Samoa time (GMT -11): Paper submission
  • Friday 8 December 2006: Author notification
  • Friday 5 January 2007: Camera-ready paper versions due
  • Saturday 24 March to Sunday 1 April 2007: ETAPS 2007
The above deadlines are strict. Making the deadline for submission of abstracts a week early allows the programme committee to start work before full versions are available. Obviously, there is no need to wait with submission of the full version until the final deadline.

Submission of an abstract implies no obligation to submit a full version; abstracts with no corresponding full versions by the final deadline will be treated as withdrawn.


Invited Speaker

Andrew Pitts, Cambridge University, UK

Papers Accepted for Presentation at ESOP 2007

  • Aleksandar Nanevski, Amal Ahmed, Greg Morrisett and Lars Birkedal. Abstract Predicates and Mutable ADTs in Hoare Type Theory
  • Kohei Suenaga and Naoki Kobayashi. Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts
  • Ichiro Hasuo and Yoshinobu Kawabe. Probabilistic Anonymity via Coalgebraic Simulations
  • Robert Ennals and David Gay. Multi-Language Synchronization
  • Derek Dreyer and Matthias Blume. Principal Type Schemes for Modular Programs
  • Jeremy Condit, Matthew Harren, Zachary Anderson, David Gay and George C. Necula. Dependent Types for Low-Level Programming
  • Noam Rinetzky, Arnd Poetzsch-Heffter, Ganesan Ramalingam, Mooly Sagiv and Eran Yahav. Modular Shape Analysis for Dynamically Encapsulated Programs
  • Guodong Li and Konrad Slind. A Proof-producing Compiler for a Subset of Higher Order Logic
  • Stephane Gaubert, Eric Goubault, Ankur Taly and Sarah Zennou. Static Analysis by Policy Interation on Relational Domains
  • Thomas Gawlitza and Hemut Seidl. Precise Fixpoint Computation Through Strategy Iteration
  • Yuxin Deng, Rob van Glabbeek, Carroll Morgan and Chenyi Zhang. Scalar Outcomes Suffice for Finitary Probabilistic Testing
  • Frederic Blanqui, Therese Hardin and Pierre Weis. On the implementation of construction functions for non-free concrete data types
  • Adrian Francalanza and Matthew Hennessy. A Fault Tolerance Bisimulation Proof for Consensus
  • Gilles Barthe, David Pichardie and Tamara Rezk. A Certified Lightweight Non-Interference Java Bytecode Verifier
  • Marco Carbone, Kohei Honda and Nobuko Yoshida. Structured Communication-Centred Programming for Web Services
  • Frédéric Besson, Thomas Jensen and Tiphaine Turpin. Small witnesses for abstract interpreation based proofs
  • Frank S. de Boer, Dave Clarke and Einar Broch Johnsen. A Complete Guide to the Future
  • Hemut Seidl, Andrea Flexeder and Michael Petter. Interprocedurally analyzing linear inequality relations
  • Lucia Acciai, Silvano Dal Zilio and Michele Boreale. A Concurrent Calculus with Atomic Transactions
  • George Kuan, David MacQueen and Robert Bruce Findler. A Rewriting Semantics for Type Inference
  • Maria Grazia Buscemi and Ugo Montanari. CC-Pi: A Constraint-Based Language for Specifying Service Level Agreements
  • Heiko Mantel and Alexander Reinhard. Controlling the What and Where of Declassification in Language-Based Security
  • Cristian Versari. A core calculus for a comparative analysis of bio-inspired calculi
  • Alessandro Lapadula, Rosario Pugliese and Francesco Tiezzi. A Calculus for Orchestration of Web Services
  • Pietro Cenciarelli, Alexander Knapp and Eleonora Sibilio. The Java Memory Model: Operationally, Denotationally, Axiomatically
  • Claude Kirchner, Radu Kopetz and Pierre-Etienne Moreau. Anti-Pattern Matching
  • Elvira Albert, Puri Arenas, Samir Genaim, German Puebla and Damiano Zanardini. Cost Analysis of Java Bytecode
  • Umut Acar, Matthias Blume and Jacob Donham. A Consistent Semantics of Self-Adjusting Computation
  • Christian Haack, Erik Poll, Jan Schaefer and Aleksy Schubert. Immutable Objects for a Java-like Language
  • Kim G. Larsen, Ulrik Nyman and Andrzej Wasowski. Modal I/O Automata for Interface and Product Line Theories
  • Xinyu Feng, Rodrigo Ferreira and Zhong Shao. On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning
  • Kenneth Knowles and Cormac Flanagan. Type Reconstruction for an Undecidable System of Refinement Types
  • Sumit Gulwani and Ashish Tiwari. Computing Procedure Summaries for Interprocedural Analysis
  • Rustan Leino and Wolfram Schulte. Using history invariants to verify observers


Programme Committee

Chair: Rocco De Nicola, University of Firenze (Italy)

  • Steve Brookes, CMU Pitsburgh, USA 
  • Gerard Boudol, INRIA Sophia Antipolis, France
  • Giuseppe Castagna, ENS Paris, France
  • Patrick Cousot, ENS Paris, France
  • Mads Dam, KTH stocholm, Sweden
  • Pierpaolo Degano, U. Pisa, Italy
  • Sophia Drossopoulou, Imperial College, UK
  • Cedric Fournet, Microsoft Cambridge, UK
  • Stefania Gnesi, ISTI CNR, Italy
  • Joshua Guttman, MITRE, USA
  • Chris Hankin, Imperial College, UK
  • Matthew Hennessy, U. Sussex, UK
  • Alan Jeffrey, Bell Labs, USA
  • John Mitchell, Stanford U., USA
  • Fleming Nielson, IMM Copenhagen, DK
  • Catuscia Palamidessi, INRIA Paris, France
  • Benjamin Pierce, U. Pennsilvania, USA
  • Andrei Sabelfeld, Chalmers, Sweden
  • Don Sannella, U. Edinburgh, UK
  • Bernhard Steffen, U. Dortmund, Germany
  • Walid Taha, Rice U., USA
  • Jan Vitek, Purdue U., USA
  • Martin Wirsing, LMU Munich, Germany
  • Xavier Leroy, INRIA Paris, France
  • Gianluigi Zavattaro, U. Bologna, Italy


Steering Committee

Chair: Chris Hankin, U.K.

  • Pierpaolo Degano, Italy
  • Neil Jones, Denmark
  • Daniel Le Metayer, France
  • Alan Mycroft, U.K.
  • Hanne Riis Nielson, Denmark
  • Bengt Nordström, Sweden
  • David Sands, Sweden
  • David Schmidt, USA
  • Gert Smolka, Germany
  • Doaitse Swierstra, The Netherlands
  • Reinhard Wilhelm, Germany