Scott Owens (auth.), Sophia Drossopoulou (eds.)3540787380, 9783540787389
The 25 revised full papers presented together with the abstract of one invited talk and two tool presentations were carefully reviewed and selected from 104 submissions and address fundamental issues in the specification, analysis, and implementation of programming languages and sytems. The papers are organized in topical sections on static analysis, security, concurrency and program verification.
Table of contents :
Front Matter….Pages –
A Sound Semantics for OCaml light ….Pages 1-15
Parametric Polymorphism through Run-Time Sealing or, Theorems for Low, Low Prices!….Pages 16-31
Regular Expression Subtyping for XML Query and Update Languages….Pages 32-47
A Theory of Hygienic Macros….Pages 48-62
A Hybrid Denotational Semantics for Hybrid Systems….Pages 63-77
Full Abstraction for Linda….Pages 78-92
Practical Programming with Higher-Order Encodings and Dependent Types….Pages 93-107
Programming in JoCaml (Tool Demonstration)….Pages 108-111
Playing with $cal{TOY}$ : Constraints and Domain Cooperation….Pages 112-115
Typing Safe Deallocation….Pages 116-130
Iterative Specialisation of Horn Clauses….Pages 131-145
Constructive Mathematics and Functional Programming (Abstract)….Pages 146-147
Ranking Abstractions….Pages 148-162
Non-disjunctive Numerical Domain for Array Predicate Abstraction….Pages 163-177
Upper Adjoints for Fast Inter-procedural Variable Equalities….Pages 178-192
Cover Algorithms and Their Combination….Pages 193-207
Tapido : Trust and Authorization Via Provenance and Integrity in Distributed Objects (Extended Abstract)….Pages 208-223
Linear Declassification….Pages 224-238
Just Forget It – The Semantics and Enforcement of Information Erasure….Pages 239-253
Open Bisimulation for the Concurrent Constraint Pi-Calculus….Pages 254-268
The Conversation Calculus: A Model of Service-Oriented Computation….Pages 269-283
Inferring Channel Buffer Bounds Via Linear Programming….Pages 284-298
Verification of Higher-Order Computation: A Game-Semantic Approach….Pages 299-306
Verification of Equivalent-Results Methods….Pages 307-321
Semi-persistent Data Structures….Pages 322-336
A Realizability Model for Impredicative Hoare Type Theory….Pages 337-352
Oracle Semantics for Concurrent Separation Logic….Pages 353-367
Certificate Translation in Abstract Interpretation….Pages 368-382
A Formal Implementation of Value Commitment….Pages 383-397
Back Matter….Pages –
Reviews
There are no reviews yet.