Programming Languages and Systems

Name: 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
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

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

Helmut Seidl(Herausgeber*in)

Springer (Verlag)

Erschienen am 22. März 2012

XV, 602 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-28869-2 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

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

Systemvoraussetzungen

Als PDF speichern Als Link merken