Ebook: Programming Languages and Systems: 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings

This book constitutes the refereed proceedings of the 22nd European Symposium on Programming, ESOP 2013, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, which took place in Rome, Italy, in March 2013. The 31 papers, presented together with a full-length invited talk, were carefully reviewed and selected from 120 full submissions. The contributions have been organized according to ten topical sections on programming techniques; programming tools; separation logic; gradual typing; shared-memory concurrency and verification; process calculi; taming concurrency; model checking and verification; weak-memory concurrency and verification; and types, inference, and analysis.

---

This book constitutes the refereed proceedings of the 22nd European Symposium on Programming, ESOP 2013, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, which took place in Rome, Italy, in March 2013. The 31 papers, presented together with a full-length invited talk, were carefully reviewed and selected from 120 full submissions. The contributions have been organized according to ten topical sections on programming techniques; programming tools; separation logic; gradual typing; shared-memory concurrency and verification; process calculi; taming concurrency; model checking and verification; weak-memory concurrency and verification; and types, inference, and analysis.

---

This book constitutes the refereed proceedings of the 22nd European Symposium on Programming, ESOP 2013, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, which took place in Rome, Italy, in March 2013. The 31 papers, presented together with a full-length invited talk, were carefully reviewed and selected from 120 full submissions. The contributions have been organized according to ten topical sections on programming techniques; programming tools; separation logic; gradual typing; shared-memory concurrency and verification; process calculi; taming concurrency; model checking and verification; weak-memory concurrency and verification; and types, inference, and analysis.
Content:
Front Matter....Pages -
Distributed Electronic Rights in JavaScript....Pages 1-20
The Compiler Forest....Pages 21-40
Pretty-Big-Step Semantics....Pages 41-60
Language Constructs for Non-Well-Founded Computation....Pages 61-80
Laziness by Need....Pages 81-100
Why3 — Where Programs Meet Provers....Pages 101-120
Compositional Invariant Checking for Overlaid and Nested Linked Lists....Pages 121-124
A Discipline for Program Verification Based on Backpointers and Its Use in Observational Disjointness....Pages 125-128
Modular Reasoning about Separation of Concurrent Data Structures....Pages 129-148
Ribbon Proofs for Separation Logic....Pages 149-168
Abstract Refinement Types....Pages 169-188
Constraining Delimited Control with Contracts....Pages 189-208
Verifying Concurrent Memory Reclamation Algorithms with Grace....Pages 209-228
Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels....Pages 229-248
Verifying Concurrent Programs against Sequential Specifications....Pages 249-269
On Distributability in Process Calculi....Pages 270-289
Behavioral Polymorphism and Parametricity in Session-Based Communication....Pages 290-309
Higher-Order Processes, Functions, and Sessions: A Monadic Integration....Pages 310-329
Concurrent Flexible Reversibility....Pages 330-349
Structural Lock Correlation with Ownership Types....Pages 350-369
Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems....Pages 370-390
Model-Checking Higher-Order Programs with Recursive Types....Pages 391-410
Counterexample-Guided Precondition Inference....Pages 411-430
Information Reuse for Multi-goal Reachability Analyses....Pages 431-450
Quarantining Weakness....Pages 451-471
Software Verification for Weak Memory via Program Transformation....Pages 472-491
Checking and Enforcing Robustness against TSO....Pages 492-511
GADTs Meet Subtyping....Pages 512-532
A Data Driven Approach for Algebraic Loop Invariants....Pages 533-553
Automatic Type Inference for Amortised Heap-Space Analysis....Pages 554-573
Back Matter....Pages 574-592
....Pages 593-613