Programming Languages and Systems [recurso electrónico] 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. 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 FliPpr : A Prettier Invertible Printing System....Pages 101-120 Slicing-Based Trace Analysis of Rewriting Logic Specifications with i Julienne ....Pages 121-124 Why3 — Where Programs Meet Provers....Pages 125-128 Compositional Invariant Checking for Overlaid and Nested Linked Lists....Pages 129-148 A Discipline for Program Verification Based on Backpointers and Its Use in Observational Disjointness....Pages 149-168 Modular Reasoning about Separation of Concurrent Data Structures....Pages 169-188 Ribbon Proofs for Separation Logic....Pages 189-208 Abstract Refinement Types....Pages 209-228 Constraining Delimited Control with Contracts....Pages 229-248 Verifying Concurrent Memory Reclamation Algorithms with Grace....Pages 249-269 Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels....Pages 270-289 Verifying Concurrent Programs against Sequential Specifications....Pages 290-309 On Distributability in Process Calculi....Pages 310-329 Behavioral Polymorphism and Parametricity in Session-Based Communication....Pages 330-349 Higher-Order Processes, Functions, and Sessions: A Monadic Integration....Pages 350-369 Concurrent Flexible Reversibility....Pages 370-390 Structural Lock Correlation with Ownership Types....Pages 391-410 Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems....Pages 411-430 Model-Checking Higher-Order Programs with Recursive Types....Pages 431-450 Counterexample-Guided Precondition Inference....Pages 451-471 Information Reuse for Multi-goal Reachability Analyses....Pages 472-491 Quarantining Weakness....Pages 492-511 Software Verification for Weak Memory via Program Transformation....Pages 512-532 Checking and Enforcing Robustness against TSO....Pages 533-553 GADTs Meet Subtyping....Pages 554-573 A Data Driven Approach for Algebraic Loop Invariants....Pages 574-592 Automatic Type Inference for Amortised Heap-Space Analysis....Pages 593-613 Back Matter....Pages - Distributed Electronic Rights in JavaScript The Compiler Forest Pretty-Big-Step Semantics Language Constructs for Non-Well-Founded Computation Laziness by Need FliPpr: A Prettier Invertible Printing System Slicing-Based Trace Analysis of Rewriting Logic Specifications with iJULIENNE Why3 — Where Programs Meet Provers Compositional Invariant Checking for Overlaid and Nested Linked Lists A Discipline for Program Verification Based on Backpointers and Its Use in Observational Disjointness Modular Reasoning about Separation of Concurrent Data Structures Ribbon Proofs for Separation Logic Abstract Refinement Types Constraining Delimited Control with Contracts Verifying Concurrent Memory Reclamation Algorithms with Grace Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels Verifying Concurrent Programs against Sequential Specifications On Distributability in Process Calculi Behavioral Polymorphism and Parametricity in Session-Based Communication Higher-Order Processes, Functions, and Sessions: A Monadic Integration Concurrent Flexible Reversibility Structural Lock Correlation with Ownership Types Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems Model-Checking Higher-Order Programs with Recursive Types Counterexample-Guided Precondition Inference Information Reuse for Multi-goal Reachability Analyses Quarantining Weakness: Compositional Reasoning under Relaxed Memory Models (Extended Abstract) Software Verification for Weak Memory via Program Transformation Checking and Enforcing Robustness against TSO GADTs Meet Subtyping A Data Driven Approach for Algebraic Loop Invariants Automatic Type Inference for Amortised Heap-Space Analysis.