Programming Languages and Systems: 12th European Symposium on Programming, ESOP 2003 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003 Warsaw, Poland, April 7–11, 2003 Proceedings

Xavier Leroy (auth.), Pierpaolo Degano (eds.)3540008861, 9783540008866

This book constitutes the refereed proceedings of the 12th European Symposium on Programming, ESOP 2003, held in Warsaw, Poland, in April 2003.

The 25 revised full papers presented together with two invited papers were carefully reviewed and selected from 99 submissions. Among the topics addressed are programming paradigms and their integration, program semantics, calculi of computation, security, advanced type systems, program analysis, program transformation, and practical algorithms based on theoretical developments.

Table of contents :
Computer Security from a Programming Language and Static Analysis Perspective….Pages 1-9
What Makes a Cryptographic Protocol Secure? The Evolution of Requirements Specification in Formal Cryptographic Protocol Analysis….Pages 10-21
A Tail-Recursive Semantics for Stack Inspections….Pages 22-37
Flexible Models for Dynamic Linking….Pages 38-53
Correction of Functional Logic Programs….Pages 54-68
Approximate Pruning in Tabled Logic Programming….Pages 69-83
Goal-Independent Suspension Analysis for Logic Programs with Dynamic Scheduling….Pages 84-98
Security Properties: Two Agents Are Sufficient….Pages 99-113
A Simple Language for Real-Time Cryptographic Protocol Analysis….Pages 114-128
Rule Formats for Non Interference….Pages 129-143
On the Secure Implementation of Security Protocols….Pages 144-158
Handling Encryption in an Analysis for Secure Information Flow….Pages 159-173
Using Controller-Synthesis Techniques to Build Property-Enforcing Layers….Pages 174-188
Automatic Software Model Checking Using CLP….Pages 189-203
Verifying Temporal Heap Properties Specified via Evolution Logic….Pages 204-222
Correctness of Data Representations Involving Heap Data Structures….Pages 223-237
Modeling Web Interactions….Pages 238-252
Type Inference for a Distributed π-Calculus….Pages 253-268
Type-Safe Update Programming….Pages 269-283
Type Error Slicing in Implicitly Typed Higher-Order Languages….Pages 284-301
Core Formal Molecular Biology….Pages 302-318
Requirements on the Execution of Kahn Process Networks….Pages 319-334
Tagging, Encoding, and Jones Optimality….Pages 335-347
The Rely-Guarantee Method in Isabelle/HOL….Pages 348-362
Building Certified Libraries for PCC: Dynamic Storage Allocation….Pages 363-379
Finite Differencing of Logical Formulas for Static Analysis….Pages 380-398
Register Allocation by Proof Transformation….Pages 399-413