Programming Languages and Systems: 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings

Philip Wadler, Robert Bruce Findler (auth.), Giuseppe Castagna (eds.)3642005896, 9783642005893

This book constitutes the refereed proceedings of the 18th European Symposium on Programming, ESOP 2009, held in York, UK, in March 2009, as part of ETAPS 2009, the European Joint Conferences on Theory and Practice of Software.

The 26 revised full papers presented together with two abstracts of invited talks were carefully reviewed and selected from 98 full paper submissions. The topics addressed are typed functional programming, computational effects, types for object-oriented languages, verification, security, concurrency, service-oriented computing, parallel and concurrent programming.

Table of contents :
Front Matter….Pages –
Well-Typed Programs Can’t Be Blamed….Pages 1-16
Exploring the Design Space of Higher-Order Casts….Pages 17-31
Practical Variable-Arity Polymorphism….Pages 32-46
Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming….Pages 47-61
Using Category Theory to Design Programming Languages….Pages 62-63
Modular Monad Transformers….Pages 64-79
Handlers of Algebraic Effects….Pages 80-94
Is Structural Subtyping Useful? An Empirical Study….Pages 95-111
An Interval-Based Inference of Variant Parametric Types….Pages 112-127
Existential Quantification for Variant Ownership….Pages 128-142
Formalising and Verifying Reference Attribute Grammars in Coq….Pages 143-159
Verified, Executable Parsing….Pages 160-174
An Efficient Algorithm for Solving the Dyck-CFL Reachability Problem on Trees….Pages 175-189
Amortised Memory Analysis Using the Depth of Data Structures….Pages 190-204
The Financial Crisis, a Lack of Contract Specification Tools: What Can Finance Learn from Programming Language Design?….Pages 205-206
All Secrets Great and Small….Pages 207-221
Type-Based Automated Verification of Authenticity in Cryptographic Protocols….Pages 222-236
A Theory of Non-monotone Memory (Or: Contexts for free )….Pages 237-251
Abstraction for Concurrent Objects….Pages 252-266
Minimization Algorithm for Symbolic Bisimilarity….Pages 267-284
Conversation Types….Pages 285-300
Abstract Processes in Orchestration Languages….Pages 301-315
Global Principal Typing in Partially Commutative Asynchronous Sessions….Pages 316-332
Tisa: A Language Design and Modular Verification Technique for Temporal Policies in Web Services….Pages 333-347
Automatic Parallelization with Separation Logic….Pages 348-362
Deny-Guarantee Reasoning….Pages 363-377
A Basis for Verifying Multi-threaded Programs….Pages 378-393
SingleTrack: A Dynamic Determinism Checker for Multithreaded Programs….Pages 394-409
Back Matter….Pages –