Programming Languages and Systems

1. Front Matter

   PDF

2. Invited Talks

   1. Composable Transactional Objects: A Position Paper

      • Maurice Herlihy, Eric Koskinen

      Pages 1-7

   2. Application-Scale Secure Multiparty Computation

      • John Launchbury, Dave Archer, Thomas DuBuisson, Eric Mertens

      Pages 8-26

3. Type Systems

   1. An Array-Oriented Language with Static Rank Polymorphism

      • Justin Slepak, Olin Shivers, Panagiotis Manolios

      Pages 27-46

   2. Gradual Typing for Annotated Type Systems

      • Peter Thiemann, Luminous Fennell

      Pages 47-66

   3. Staged Composition Synthesis

      • Boris Düdder, Moritz Martens, Jakob Rehof

      Pages 67-86

   4. Overlapping and Order-Independent Patterns

      • Jesper Cockx, Frank Piessens, Dominique Devriese

      Pages 87-106

4. Verified Compilation

   1. Verified Compilation for Shared-Memory C

      • Lennart Beringer, Gordon Stewart, Robert Dockins, Andrew W. Appel

      Pages 107-127

   2. Verifying an Open Compiler Using Multi-language Semantics

      • James T. Perconti, Amal Ahmed

      Pages 128-148

5. Program Verification I

   1. Impredicative Concurrent Abstract Predicates

      • Kasper Svendsen, Lars Birkedal

      Pages 149-168

   2. Local Reasoning for the POSIX File System

      • Philippa Gardner, Gian Ntzik, Adam Wright

      Pages 169-188

   3. A Coq Formalization of the Relational Data Model

      • Véronique Benzaken, Évelyne Contejean, Stefania Dumbrava

      Pages 189-208

6. Semantics

   1. On Probabilistic Applicative Bisimulation and Call-by-Value λ-Calculi

      • Raphaëlle Crubillé, Ugo Dal Lago

      Pages 209-228

   2. Grounding Synchronous Deterministic Concurrency in Sequential Programming

      • Joaquín Aguado, Michael Mendler, Reinhard von Hanxleden, Insa Fuhrmann

      Pages 229-248

   3. The Duality of Construction

      • Paul Downen, Zena M. Ariola

      Pages 249-269

   4. Deriving Pretty-Big-Step Semantics from Small-Step Semantics

      • Casper Bach Poulsen, Peter D. Mosses

      Pages 270-289

7. Concurrency

   1. Communicating State Transition Systems for Fine-Grained Concurrent Resources

      • Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, Germán Andrés Delbianco

      Pages 290-310

   2. Checking Linearizability of Encapsulated Extended Operations

      • Oren Zomer, Guy Golan-Gueta, G. Ramalingam, Mooly Sagiv

      Pages 311-330

8. Linear Types

   1. Bounded Linear Types in a Resource Semiring

      • Dan R. Ghica, Alex I. Smith

      Pages 331-350

   2. A Core Quantitative Coeffect Calculus

      • Aloïs Brunel, Marco Gaboardi, Damiano Mazza, Steve Zdancewic

      Pages 351-370

This book constitutes the proceedings of the 23rd European Symposium on Programming, ESOP 2014, which took place in Grenoble, France, in April 2014, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014. The 27 papers presented in this volume were carefully reviewed and selected from 109 submissions. In addition, the book contains two invited talks. The contributions are organized in topical sections named: type systems; verified compilation; program verification; semantics; concurrency; linear types; network and process calculi; and program analysis.

• calculus
• concurrency
• formal methods
• linear types
• models of computation
• process calculi
• program analysis
• program reasoning
• program semantics

• Yale University, New Haven, USA

  Zhong Shao

Policies and ethics