Programming Languages and Systems
21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012, Proceedings
Erschienen am 22. März 2012
XV, 602 Seiten
978-3-642-28869-2 (ISBN)
Beschreibung
This book constitutes the refereed proceedings of the 21st European Symposium on Programming, ESOP 2012, held in Tallinn, Estonia, as part of ETAPS 2012, in March/April 2012.
The 28 full papers, presented together with one full length invited talk, were carefully reviewed and selected from 92 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.
Weitere Details
Weitere Ausgaben
Andere Ausgaben
Helmut Seidl
Programming Languages and Systems
21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012, Proceedings
Buch
03/2012
1. Auflage
Springer
53,49 €
Versand in 7-9 Tagen
Inhalt
- Title page
- Foreword
- Preface
- Organization
- Table of Contents
- Foundations of C++
- Introduction
- Ideals
- Memory and Objects
- Compile-Time Computation
- Error Handling
- Containers
- Copy and Move
- RAII
- Class Hierarchies
- Algorithms
- Type Functions
- Concurrency
- Type Safety
- Challenges
- References
- What's Decidable about Weak Memory Models?
- Introduction
- Preliminary Definitions and Notations
- Weak Memory Models
- Shared Memory Concurrent Systems
- Memory Models
- A Semantics Based on Rewrite Rules
- The State Reachability Problem
- NSW: A Model with Non Speculative Writes
- Absence of Causality Cycles in NSW
- An Operational Model for NSW
- Event Structures
- An Operational Model with Stored Reads
- From Event Structures to FIFO Buffers
- Eliminating Reads from Event Structures
- Eliminating Write Fences from Event Structures
- The State Reachability Problem of NSW
- Nonatomic Writes Cause Undecidability
- Conclusion and Future Work
- References
- A Formally Verified SSA-Based Middle-End: Static Single Assignment Meets CompCert
- Introduction
- Background
- The SSA Language
- Translation Validation of SSA Generation
- Conversion out of SSA
- Validation of SSA-Based Optimizations
- Implementation and Experimental Results
- Related Work
- Conclusion and Future Work
- References
- Eventually Consistent Transactions
- Introduction
- Formulation
- Clients and Transactions
- Sequential Consistency
- Eventual Consistency
- Eventual Consistency in Related Work
- Revision Consistency
- Revision Diagrams
- Graph Properties
- Query and Update Semantics
- Revision Diagrams and Histories
- Proof of Thm 1
- System Implementation
- System Models
- Single Synchronous Server Model
- Server Pool Model
- Related Work
- Conclusion and Future Work
- References
- Concurrent Library Correctness on the TSO Memory Model
- Introduction
- TSO semantics
- Library-Local and Client-Local Semantics
- Linearizability on TSO
- Abstraction Theorem
- Checking Linearizability on TSO
- Related Work and Conclusion
- References
- Automated Verification of Equivalence Properties of Cryptographic Protocols
- Introduction
- Preliminaries
- A Cryptographic Process Calculus
- Modeling Traces as Horn Clauses
- Procedure for Deciding Trace Equivalence
- Knowledge Bases and Saturation
- Algorithm for Checking Equivalence
- Prototype and Case Studies
- Conclusion and Future Work
- References
- The Call-by-Need Lambda Calculus, Revisited
- A Short History of the Calculus
- The Original Call-by-Need Calculi
- A New Call-by-Need Calculus
- Contexts
- The need Axiom and a Derivation
- Consistency, Determinism, and Soundness
- Consistency: Church-Rosser
- Deterministic Behavior: Standard Reduction
- Observational Equivalence
- Correctness
- Overview
- Adapting Launchbury's Natural Semantics
- Parallel Rewriting
- A Transition System for Comparing need and
- Relating All Layers
- Extensions and Variants
- Conclusion
- References
- A Compositional Specification Theory for Component Behaviours
- Introduction
- A Declarative Theory of Components
- Refinement
- Parallel Composition
- Conjunction
- Quotient
- An Operational Theory of Components
- Refinement
- Error-Completion
- Parallel Composition
- Conjunction
- Quotient
- Full-Abstraction Results
- Conclusion and Future Work
- References
- Probabilistic Abstract Interpretation
- Introduction
- The Abstract Interpretation Framework
- Probabilistic Concrete Semantics
- Definition
- Fixpoint Semantics
- Probabilistic Concrete Transformers
- Examples of Probabilistic Semantics
- Probabilistic Concrete Collecting Semantics
- Definition
- Downsizing the Concrete Collecting Domain
- Probabilistic Abstract Semantics
- (I) Abstracting the Semantics
- (II) Abstracting the Scenario Space
- (III) Abstracting Probabilistic Semantics by Distributions
- Iterating in the Abstract and Branch Prediction
- Conditionals
- Loops
- Related Work: Some Well-Known Techniques as Probabilistic Abstractions
- Markov Chains/Decision Processes
- Probabilistic Model Checking
- Quantitative Abstraction
- Probabilistic Strongest Postcondition Semantics
- Probabilistic Weakest Precondition Semantics
- Future Work and Conclusion
- References
- Multiparty Session Types Meet Communicating Automata
- Introduction
- Generalised Multiparty Sessions
- Global Types for Generalised Multiparty Sessions
- Well-formed Global Types
- Multiparty Session Automata (MSA) and their Properties
- Local Types and the Projection Algorithm
- Communicating Finite State Machines
- Multiparty Session Automata (MSA)
- Properties of MSAs
- General Multiparty Session Processes
- Properties of Generalised Multiparty Session Processes
- Typing Generalised Multiparty Session Processes
- Properties of Typed Multiparty Session Processes
- Advanced Properties in a Single Multiparty Session
- Related Work
- Conclusion and Future Work
- References
- Complete Monitors for Behavioral Contracts
- Blame Correctness Is Not Enough
- Beyond Blame Correctness
- Complete Monitors with Pictures
- Complete Monitors Formally
- Indy Is a Complete Monitor
- Neither Lax Nor Picky Is a Complete Monitor
- Mutation Needs Complete Monitors
- Complete Monitors Enable Typed-Untyped Interaction
- Related Work
- References
- A Systematic Approach to Delimited Control with Multiple Prompts
- Introduction
- Lambda Calculus:
- Lambda Calculus with Control: Parigot's
- Delimited Control: $?µ tp$
- Continuation Passing Style ($C^2_?µ tp$)
- Intermediate Languages of Dynamic Binding: $?µ tp,?µ tp^b$
- Translating Control (Ctp"0362tp)
- Translating Dynamic Binding (Dtp"0362tp)
- Backtracking the Environment (Dtp"0362tpb)
- Control with Multiple Prompts: $?µ$ via $?^b$
- Delimited Control with Transparent Prompts: $?µ tp$
- Intermediate Language of Dynamic Unbinding: $? tp$
- Delimited Control with Multiple Prompts: $?µ$ via $?$
- Dynamic Unbinding with Multiple Variables: ?
- Capture Up to a Prompt: $?µ$
- Conclusion
- References
- Generate, Test, and Aggregate: A Calculation-based Framework for Systematic Parallel Programming with MapReduce
- Introduction
- Background: Lists, Monoids and MapReduce
- Lists, Monoids, and Homomorphisms
- MapReduce
- Running Example: The Knapsack Problem
- Semiring Fusion
- Semirings and Their Homomorphisms
- Polymorphic Generators
- Filter Embedding
- Developing Intuitions by Example
- The Generalized Theorem
- A More Complex Application
- Finding a Most Likely Sequence of Hidden States
- Incremental Refinement
- Related Work
- Conclusion
- References
- Trace Spaces: An Efficient New Technique for State-Space Reduction
- Geometric Semantics of Concurrent Processes
- A Toy Shared-Memory Concurrent Language
- Geometric Semantics
- Computing Trace Spaces
- Trace Spaces
- The Index Poset
- Computing Dihomotopy Classes
- An Efficient Implementation
- An Example: The n Dining Philosophers
- Programs with Loops
- Paths in Deloopings
- The Shadow Automaton
- Reducing the Size of the Shadow Automaton
- Preliminary Implementation and Benchmark
- An Application to Static Analysis
- Conclusion and Future Work
- References
- A Process Algebra for Wireless Mesh Networks
- Introduction
- A Process Algebra for Wireless Routing Protocols
- A Language for Sequential Processes
- A Language for Parallel Processes
- A Language for Networks
- Results on the Process Algebra
- Optional Augmentation to Ensure Non-blocking Broadcast
- Illustrative Example
- Routing Protocols
- Ad-Hoc On-Demand Distance Vector Routing Protocol
- A Formal Model of AODV
- Invariants
- Formalising Temporal Properties
- Related Work
- Conclusion and Outlook
- References
- On the Correctness of the SIMT Execution Model of GPUs
- Introduction
- SIMT Hardware Model
- Hardware Architecture and Programming Model
- SIMT Control Flow
- Stack-Based SIMT Reconvergence
- Formalization of the SIMT Execution Model
- Basic Domains and Language Grammar
- Warp Configurations and Transitions
- Warp Operational Semantics
- Simulating SIMT Execution by Interleaved Multi-Threading
- Interleaved Multi-Thread Semantics
- Simulation Relation
- Unfairness of the SIMT Execution Model
- Programs Affected by the Unfairness Problem
- Unfairness of Alternative SIMT Execution Models
- Conclusions and Future Work
- References
- Reasoning about Lock Placements
- Introduction
- FlatMaps
- Lock Placements
- Well-Locked Transactions
- Serializability of Well-Locked Transactions
- Shared/Exclusive Logical Locks
- Mutable Tree-Structured Heaps
- Lock Placements
- Well-Locked Transactions
- Transactions on DAGs of Bounded Degree
- Lock Placements
- Well-Locked Transactions
- Related Work
- Conclusion
- References
- Reasoning about Multi-stage Programs
- Introduction
- Contributions
- The ?U Calculus: Syntax, Semantics, and EquationalTheory
- Syntax and Operational Semantics
- Equational Theory
- Closing Substitutions Compromise Validity
- The Erasure Theorem
- Theorem Statement
- Example: Erasing Staged Power
- Why CBN Facts Are Necessary for CBV Reasoning
- Applicative Bisimulation
- Proof by Bisimulation
- Example: Tying Loose Ends on Staged Power
- Related Works
- Conclusion and Future Work
- References
- Fictional Separation Logic
- Introduction
- Formal Preliminaries
- Abstract Assertion Logic
- Programming Language
- Specification Logic
- Constructing Separation Algebras
- Fictional Separation Logic
- Proof Patterns
- Example: Bit Pair
- Example: Monotonic Counter
- Clients and Separating Products
- Example: Client of Two Modules
- Example: Wrapper
- Indirect Entailment
- Example: Fractional Permissions
- Stacking
- Example: Abstract Fractional Permissions
- Discussion and Related Work
- References
- Validating LR(1) Parsers
- Introduction
- Grammars and Automata
- Symbols
- Grammars
- Semantics of Grammars
- Automata
- Semantics of Automata
- Correctness Properties and Validation
- Soundness
- Safety
- Completeness
- Unambiguity
- Coq Formalization
- Experimentation on a C99 Parser
- Related Work
- Conclusions and Future Work
- References
- Adding Equations to System F Types
- Introduction
- Informal Overview
- Examples
- Applications
- Syntax and Semantics
- Existential Representations of Inductive Datatypes
- Related Work
- System R and Plotkin-Abadi Logic
- Dependent Types
- The Haskell Rules Mechanism
- Extended ML
- Future Work
- References
- GMeta: A Generic Formal Metatheory Framework for First-Order Representations
- Introduction
- Our Solution
- Contributions
- Case Studies
- GMeta Design
- Making GMeta Convenient to Use
- DGP for Datatypes with First-Order Binders
- Inductive Families
- Datatype Generic Programming
- A Universe for Representing First-Order Binding
- Generic Operations and Lemmas
- Locally Nameless
- De Bruijn
- Discussion and Evaluation
- Related Work
- Conclusion
- References
- Expansion for Universal Quantifiers
- Introduction
- Background and Motivation
- Overview of System Fs
- Summary of Contributions
- Syntax
- Typing Rules
- Substitution and Expansion
- Expansion Application
- Substitution Application
- Initial Skeletons
- Solvedness and Subject Reduction
- Solvedness and System F
- Subject Reduction
- Related Work
- Expansion
- Type Inference in System F
- Conclusion and Future Work
- References
- Non-monotonic Self-Adjusting Computation
- Introduction
- Overview
- The Src Language
- Static, Dynamic, and Cost Semantics
- Trace Distance
- The Tgt Language
- Static, Dynamic, and Cost Semantics
- Consistency of Change-Propagation
- Trace Distance
- Translation
- The Change Propagation Algorithm
- Related Work
- Conclusion and Future Work
- References
- Java and the Java Memory Model - A Unified, Machine-Checked Formalisation
- Introduction
- An Informal Introduction to the JMM
- Related Work
- From Sequential Java to the Java Memory Model
- Single-Thread Semantics
- Complete Interleavings
- The Java Memory Model
- Discussion of Our JMM Formalisation
- The Data Race Freedom Guarantee
- The DRF Guarantee
- Sequentially Consistent Completions
- Discussion
- Conclusion and Future Work
- References
- A Type and Effect System for Determinism in Multithreaded Programs
- Introduction
- Deterministic Effects at a Glance
- Effects, Noninterference and Determinism
- Deterministic Effects with Nondeterministism
- A Deterministic Effect System
- Static Semantics
- Dynamic Semantics and Properties
- Discussion
- Extensions
- Related Work
- Future Work
- Conclusion
- References
- Linear Logical Relations for Session-Based Concurrency
- Introduction
- Process Model: Syntax and Semantics
- Session Types as Dual Intutionistic Linear Logic Propositions
- Linear Logical Relations and Termination of Typed Processes
- An Observational Equivalence for Typed Processes
- Soundness of Proof Conversions and Type Isomorphisms
- Related Work
- Concluding Remarks
- References
- Staged Computation with Staged Lexical Scope
- Introduction
- The Challenge
- Our Contributions
- The Staged Type System ?[ ]
- Staged Lexical Scope
- Properties of ?[ ]
- Examples
- The Staged Type System ?[ ]&
- Subtype Polymorphism
- Evaluation and Lifting
- Mutable State
- Semantics of ?[ ]
- Formal Properties
- Standard Results
- Results for Staging
- Subject Reduction
- Progress
- Relation with Existing Type Systems
- Relation to ?
- Relation to ?S4
- Related Work
- Conclusions
- References
- Gradual Ownership Types
- Introduction
- Intuition and Overview
- The Language JO?
- Syntax
- Environments and Owners
- Type Consistency and Subtyping
- Expression, Method and Class Typing
- Type-Directed Translation: The Language JO+?
- Syntax of JO+?
- Helper Relations
- Type-Directed Program Translation
- Operational Semantics of JO+?
- Type Safety
- Implementation
- Experience
- Discussion
- Related Work
- Conclusion
- References
- Author Index
