Programming Languages and Systems
20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26--April 3, 2011, Proceedings
Published on 14. March 2011
XIV, 501 pages
978-3-642-19718-5 (ISBN)
Description
This book constitutes the refereed proceedings of the 20th European Symposium on Programming, ESOP 2011, held in Saarbrücken, Germany, March 30-April 1, 2011, as part of ETAPS 2011, the European Joint Conferences on Theory and Practice of Software.
The 24 revised full papers presented together with one full length invited talk were carefully reviewed and selected from 93 full paper submissions. Papers were invited on all aspects of programming language research including: programming paradigms and styles, methods and tools to write and specify programs and languages, methods and tools for reasoning about programs, methods and tools for implementation, and concurrency and distribution.
More details
Other editions
Additional editions
Gilles Barthe
Programming Languages and Systems
20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26--April 3, 2011, Proceedings
Book
03/2011
1st Edition
Springer
€53.49
Shipment within 5-7 days
Content
- 6602
- Foreword
- Preface
- Organization
- Table of Contents
- Verified Software Toolchain
- Observables
- The Programming Language and Compiler
- Oracle Semantics
- The Program Logic
- Instrumenting Static Analyses
- Semantic Modeling of Assertions
- Partial Erasure before Bisimulation
- Bisimulation
- Weak Memory Models
- Foundational Verification
- What Is the Trusted Base?
- Conclusion
- References
- Polymorphic Contracts
- Introduction
- Examples
- Defining FH
- Parametricity
- Subtyping and Upcast Elimination
- Related Work
- Future Work
- References
- Proving Isolation Properties for Software Transactional Memory
- Introduction
- Execution Traces
- Successful Commits
- Read Conflicts
- Snapshot Isolation
- Semantics of Haskell's orElse
- Formalization of Transactions
- Syntax
- Operational Semantics
- Opacity
- Well-Formedness
- Related Work
- Conclusion and Outlook
- References
- Typing Copyless Message Passing
- Introduction
- Syntax and Semantics of CoreSing#
- Type System
- Extensions
- Conclusions
- References
- Measure Transformer Semantics forBayesian Machine Learning
- Introduction
- Bayesian Models as Probabilistic Expressions
- Syntax, Informal Semantics, and Bayesian Reading
- Syntactic Conventions and Monomorphic Typing Rules
- Semantics as Measure Transformers
- Types as Measurable Spaces
- Finite Measures
- Measure Transformers
- Measure Transformer Semantics of Fun
- Semantics as Factor Graphs
- Imp: An Imperative Core Calculus
- Translating from Fun to Imp
- Factor Graphs
- Factor Graph Semantics for Imp
- Implementation Experience
- Related Work
- Conclusion
- References
- Transfer Function Synthesis without Quantifier Elimination
- Introduction
- Deriving Transfer Functions by Quantifier Elimination
- The Drawbacks of Quantifier Elimination
- Avoiding Quantifier Elimination
- Outline of the Approach
- Deriving Guards
- Deriving Interval Guards by Range Refinement
- Deriving Octagonal Guards by Range Refinement
- Deriving Updates
- Inferring Affine Equalities
- Lifting Affine Equalities to Interval Updates
- Lifting Affine Equalities to Octagonal Updates
- Inferring Affine Inequalities for Octagonal Updates
- Inferring Bounds for Octagons
- Evaluating Transfer Functions
- A Single Guard and Update Pair
- A System of Guard and Update Pairs
- Experiments
- Related Work
- Concluding Discussion
- References
- Semantics of Concurrent Revisions
- Introduction
- Discussion
- Revisions vs. Interleaved Tasks
- Local Reasoning vs. Serializability
- State Merging
- Nesting of Revisions
- Related Work
- Revision Calculus
- Syntax and Semantics
- Executions
- Determinacy
- State Merging
- Merge Functions
- Commutative Merges
- Snapshot Isolation
- Abstract Data Types and Sequential Merges
- Revision Diagrams
- Conclusion and Future Work
- References
- Type-Based Access Control in Data-Centric Systems
- Introduction
- Syntax
- Operational Semantics
- Type System
- Discussion and Related Work
- Concluding Remarks
- References
- Linear Absolute Value Relation Analysis
- Introduction
- Linear Absolute Value Inequality Systems and Their Equivalents
- Linear Absolute Value Inequality Systems (AVIs)
- Extended Linear Complementarity Problems (XLCPs)
- Interval Linear Inequality Systems (ILIs)
- Equivalence among AVIs, XLCPs and ILIs
- Double Description Method for XLCP
- Conversion from the Constraint to the Generator Representation
- Conversion from the Generator to the Constraint Representation
- An Abstract Domain of Linear Absolute Value Inequalities
- Representation
- Domain Operations
- Implementation and Experimental Results
- Related Work
- Conclusion
- References
- Generalizing the Template Polyhedral Domain
- Introduction
- Preliminaries
- Generalized Templates
- Two Parameters per Template Entry
- Projecting to Two Dimensions Efficiently
- Efficient Approximations
- Applications
- Implementation and Experiments
- Related Work
- Conclusion
- Dataflow Analysis for Datarace-Free Programs
- Introduction
- Overview of Our Approach
- Related Work
- Preliminaries
- Program Structure
- Execution
- Datarace-Free Programs
- Analysis for Sequential Programs
- Value Set Analysis
- Abstractions of Value Set Semantics
- Null-Pointer Analysis
- Analysis for Concurrent Programs
- Proof of Soundness
- For Value Set Analysis
- For Abstractions of Value Set Semantics
- Context-Sensitive Analysis
- Implementation
- References
- Compiling Information-Flow Security to Minimal Trusted Computing Bases
- Programming with TPMs
- An Imperative Higher-Order Language
- Information Flow Security
- Command Semantics for Secure Instructions
- CFLOW Revisited
- Implementing Virtual Hosts on TPMs
- References
- Improving Strategies via SMT Solving
- Introduction
- Basics
- A Lower Bound on the Complexity
- Determining Improved Strategies
- Solving Systems of Concave Equations
- Computing Greatest Finite Pre-solutions
- An Upper Bound on the Complexity
- Conclusion
- References
- Typing Local Control and State Using Flow Analysis
- Introduction
- Control and State in Scripting Languages
- Semantics and Types
- Relating Static Types and Runtime Tags
- Automatically Inserting Safe tagchecks
- Flow Analysis via CPS
- CPS Transformation
- Modular Flow Analysis
- Combining Typing and Flow Analysis
- Related Work
- References
- Barriers in Concurrent Separation Logic
- Introduction
- Syntax, Separation Algebras, Shares, and Assertions
- Programming Language Syntax
- Disjoint Multi-unit Separation Algebras
- Shares
- Assertion Language
- Example
- Barrier Definitions and Consistency Requirements
- Hoare Logic
- Semantic Models
- Coq Development
- Limitations and Future Work
- Related Work
- Conclusion
- References
- From Exponential to Polynomial-Time Security Typing via Principal Types
- Introduction
- Flow-Sensitive Security Types
- FST with a pc-Variable
- Principal Typings
- The Principal Type System
- Complexity
- Termination Typing
- Erasure Types
- Non-algorithmic Erasure Type System
- Generalised Erasure Type System
- Principal Types for Erasure Typing
- Procedures
- Procedure Typing, Algorithmically
- Related Work
- Conclusions and Future Work
- References
- Secure the Clones
- Introduction
- Cloning of Objects
- Copy Policies
- Enforcement
- Language and Copy Policies
- Policies and Inheritance
- Semantics of Copy Policies
- Type and Effect System
- From Annotation to Type
- Type Interpretation
- Sub-typing
- Type and Effect System
- Inference
- Experiments
- Related Work
- Conclusions and Perspectives
- References
- Biochemical Reaction Rules with Constraints
- Introduction
- Reaction Rules with Equality Constraints
- An Alternative Stochastic Semantics
- Expressing the Stochastic -Calculus
- Biochemical Reaction Rules with General Constraints
- Stochastic Simulator
- Conclusion
- References
- A Testing Theory for a Higher-Order Cryptographic Language
- Introduction
- Semantics of HOspi
- First-Order Semantics
- Configurations
- Transitions
- History Equivalence
- Set Simulations
- Examples
- Messaging Servers
- Example 2: Conference Servers
- Related and Future Work
- References
- A New Method for Dependent Parsing
- Introduction
- Gul, a User-Level Language
- The Intermediate Language Gil
- The Coroutine Transformation
- Assumptions on the Target Language
- Coroutines by Example
- Coroutines Formalized
- Correctness
- Typed Target Languages
- Evaluation
- Related Work
- References
- Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs
- Introduction
- Non-parallel Programs
- Syntax
- Concrete Structured Semantics P
- Abstract Structured Semantics P
- Concrete Path-Based Semantics
- Parallel Programs in Shared Memory
- Concrete Interleaving Semantics P*
- Concrete Interference Semantics PI
- Abstract Interference Semantics PI
- Weakly Consistent Memory Semantics P'*
- Parallel Programs with a Scheduler
- Priorities and Synchronization Primitives
- Concrete Scheduled Interleaving Semantics PH
- Scheduled Weakly Consistent Memory Semantics P'H
- Concrete Scheduled Interference Semantics PC
- Abstract Scheduled Interference Semantics PC
- Experimental Results
- Related Work
- Conclusion
- References
- Algorithmic Nominal Game Semantics
- Introduction
- Finitary Reduced ML
- Game Semantics
- Automata
- From Terms to Plays-with-Stores
- Automata for Protoplays
- Bisimulation
- Further Work
- References
- The Relationship between Separation Logic and Implicit Dynamic Frames
- Introduction
- Background and Motivation
- Standard Separation Logic
- Chalice and Implicit Dynamic Frames
- A Total Heaps Semantics for Separation Logic
- Verification Conditions
- Chalice
- Relationship
- Related Work
- Extensions and Applications
- References
- Precise Interprocedural Analysis in the Presence of Pointers to the Stack
- Introduction
- The Language and Its Standard Semantics
- An Equivalent Local Semantics
- Local Semantics
- Preservation of Properties by the Local Semantics
- Interprocedural Abstraction
- Representing Sets and Relations of Activation Records
- Abstracting Sets of Activation Records
- Related Work
- Conclusion
- References
- General Bindings and Alpha-Equivalence in Nominal Isabelle
- Introduction
- A Short Review of the Nominal Logic Work
- General Bindings
- Specifying General Bindings
- Alpha-Equivalence and Free Atoms
- Establishing the Reasoning Infrastructure
- Strong Induction Principles
- Related Work
- Conclusion
- References
- Author Index
