ESOP 2014 Accepted Papers

Véronique Benzaken, Evelyne Contejean and Stefania Dumbrava. A Coq Formalization of the Relational Data Model

Ravi Mangal, Mayur Naik and Hongseok Yang. A Correspondence between Two Approaches to Interprocedural Analysis in the Presence of Join

Boris Düdder, Moritz Martens and Jakob Rehof. Staged Composition Synthesis

Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno and Naoki Kobayashi. Termination Verification for Higher-Order Functional Programs

Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey and Germán Andrés Delbianco. Communicating State Transition Systems for Fine-Grained Concurrent Resources

Jesper Cockx, Frank Piessens and Dominique Devriese. Overlapping and Order-Independent Patterns

João Matos, João Garcia and Paolo Romano. REAP: Reporting Errors Using Alternative Paths

Laura Bocchi, Hernan Melgratti and Emilio Tuosto. Resolving Non-determinism in Choreographies

Lennart Beringer, Gordon Stewart, Robert Dockins and Andrew W. Appel. Verified Compilation for Shared-Memory C

Oren Zomer, Guy Golan-Gueta, G. Ramalingam and Mooly Sagiv. Checking Linearizability of Encapsulated Extended Operations

James T. Perconti and Amal Ahmed. Verifying an Open Compiler Using Multi-Language Semantics

Aparna Kotha, Kapil Anand, Timothy Creech, Khaled Elwazeer, Matthew Smithson and Rajeev Barua. Affine Parallelization of Loops with Run-time Dependent Bounds from Binaries

Zhoulai Fu. Targeted update --- Aggressive Memory Abstraction Beyond Common Sense, and its Application on Static Numeric Analysis

Paul Downen and Zena Ariola. The duality of construction

Akira Yoshimizu, Ichiro Hasuo, Claudia Faggian and Ugo Dal Lago. Measurements in Proof Nets as Higher-Order Quantum Circuits

Aloïs Brunel, Marco Gaboardi, Damiano Mazza and Steve Zdancewic. A Core Quantitative Coeffect Calculus

Peter Thiemann and Luminous Fennell. Gradual Typing for Annotated Type Systems

Caterina Urban and Antoine Miné. An Abstract Domain to Infer Ordinal-Valued Ranking Functions

Tony Garnock-Jones, Sam Tobin-Hochstadt and Matthias Felleisen. The Network as a Language Construct

Dan Ghica and Alex I. Smith. Bounded Linear Types with Generalised Resources

Casper Bach Poulsen and Peter D. Mosses. Deriving Pretty-Big-Step Semantics from Small-Step Semantics

Kasper Svendsen and Lars Birkedal. Impredicative Concurrent Abstract Predicates

Martin Brain, Cristina David, Daniel Kroening and Peter Schrammel. Model and Proof Generation for Heap-Manipulating Programs

Justin Slepak, Olin Shivers and Panagiotis Manolios. An array-oriented language with static rank polymorphism

Philippa Gardner, Gian Ntzik and Adam Wright. Local Reasoning about File Systems

Raphaelle Crubille and Ugo Dal Lago. Probabilistic Applicative Bisimulation and Call-by-Value Lambda Calculi

Joaquin Aguado, Michael Mendler, Reinhard von Hanxleden and Insa Fuhrmann. Grounding Synchronous Deterministic Concurrency in Sequential Programming