Programming Languages and Systems Book

Invited Talk
Techniques for Contextual Equivalence in Higher-Order, Typed Languages   Andrew Pitts     1
Models and Languages for Web Services
Structured Communication-Centred Programming for Web Services   Marco Carbone   Kohei Honda   Nobuko Yoshida     2
CC-Pi: A Constraint-Based Language for Specifying Service Level Agreements   Maria Grazia Buscemi   Ugo Montanari     18
A Calculus for Orchestration of Web Services   Alessandro Lapadula   Rosario Pugliese   Francesco Tiezzi     33
A Concurrent Calculus with Atomic Transactions   Lucia Acciai   Michele Boreale   Silvano Dal Zilio     48
Verification
Modal I/O Automata for Interface and Product Line Theories   Kim G. Larsen   Ulrik Nyman   Andrzej Wasowski     64
Using History Invariants to Verify Observers   K. Rustan M. Leino   Wolfram Schulte     80
Term Rewriting
On the Implementation of Construction Functions for Non-free Concrete Data Types   Frederic Blanqui   Therese Hardin   Pierre Weis     95
Anti-pattern Matching   Claude Kirchner   Radu Kopetz   Pierre-Etienne Moreau     110
Language Based Security
A Certified LightweightNon-interference Java Bytecode Verifier   Gilles Barthe   David Pichardie   Tamara Rezk     125
Controlling the What and Where of Declassification in Language-Based Security   Heiko Mantel   Alexander Reinhard     141
Cost Analysis of Java Bytecode   E. Albert   P. Arenas   S. Genaim   G. Puebla   D. Zanardini     157
Logics and Correctness Proofs
On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning   Xinyu Feng   Rodrigo Ferreira   Zhong Shao     173
Abstract Predicates and Mutable ADTs in Hoare Type Theory   Aleksandar Nanevski   Amal Ahmed   Greg Morrisett   Lars Birkedal     189
Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic   Guodong Li   Scott Owens   Konrad Slind     205
Static Analysis and Abstract Interpretation I
Modular Shape Analysis for Dynamically Encapsulated Programs   N. Rinetzky   A. Poetzsch-Heffter   G. Ramalingam   M. Sagiv   E. Yahav     220
Static Analysis by Policy Iteration on Relational Domains   Stephane Gaubert   Eric Goubault   Ankur Taly   Sarah Zennou      237
Computing Procedure Summaries for Interprocedural Analysis   Sumit Gulwani   Ashish Tiwari     253
Small Witnesses for Abstract Interpretation-Based Proofs   Frederic Besson   Thomas Jensen   Tiphaine Turpin     268
Static Analysis and Abstract Interpretation II
Interprocedurally Analysing Linear Inequality Relations   Helmut Seidl   Andrea Flexeder   Michael Petter     284
Precise Fixpoint Computation Through Strategy Iteration   Thomas Gawlitza   Helmut Seidl     300
Semantic Theories for Object Oriented Languages
A Complete Guide to the Future   Frank S. de Boer   Dave Clarke   Einar Broch Johnsen     316
The Java Memory Model: Operationally, Denotationally, Axiomatically   Pietro Cenciarelli   Alexander Knapp   Eleonora Sibilio     331
Immutable Objects for a Java-Like Language   C. Haack   E. Poll   J. Schafer   A. Schubert     347
Process Algebraic Techniques
Scalar Outcomes Suffice for Finitary Probabilistic Testing   Yuxin Deng   Rob van Glabbeek   Carroll Morgan   Chenyi Zhang     363
Probabilistic Anonymity Via Coalgebraic Simulations   Ichiro Hasuo   Yoshinobu Kawabe     379
A Fault Tolerance Bisimulation Proof for Consensus   Adrian Francalanza   Matthew Hennessy     395
A Core Calculus for a Comparative Analysis of Bio-inspired Calculi   Cristian Versari     411
Applicative Programming
A Rewriting Semantics for Type Inference   George Kuan   David MacQueen   Robert Bruce Findler     426
Principal Type Schemes for Modular Programs   Derek Dreyer   Matthias Blume     441
A Consistent Semantics of Self-adjusting Computation   Umut A. Acar   Matthias Blume   Jacob Donham     458
Multi-language Synchronization   Robert Ennals   David Gay     475
Types for Systems Properties
Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts   Kohei Suenaga   Naoki Kobayashi     490
Type Reconstruction for General Refinement Types   Kenneth Knowles   Cormac Flanagan     505
Dependent Types for Low-Level Programming   Jeremy Condit   Matthew Harren   Zachary Anderson   David Gay   George C. Necula     520
Author Index     537