Sciweavers

ESOP
2008
Springer
13 years 9 months ago
Regular Expression Subtyping for XML Query and Update Languages
Abstract. XML database query languages such as XQuery employ regular expression types with structural subtyping. Subtyping systems typically have two presentations, which should be...
James Cheney
ESOP
2008
Springer
13 years 9 months ago
Oracle Semantics for Concurrent Separation Logic
Aquinas Hobor, Andrew W. Appel, Francesco Zappa Na...
ESOP
2008
Springer
13 years 9 months ago
Open Bisimulation for the Concurrent Constraint Pi-Calculus
Abstract. The concurrent constraint pi-calculus (cc-pi-calculus) has been introduced as a model for concluding Service Level Agreements. The cc-pi calculus combines the synchronous...
Maria Grazia Buscemi, Ugo Montanari
ESOP
2008
Springer
13 years 9 months ago
A Formal Implementation of Value Commitment
In an optimistic approach to security, one can often simplify protocol design by relying on audit logs, which can be analyzed a posteriori. Such auditing is widely used in practice...
Cédric Fournet, Nataliya Guts, Francesco Za...
ESOP
2008
Springer
13 years 9 months ago
A Theory of Hygienic Macros
David Herman, Mitchell Wand
ESOP
2008
Springer
13 years 9 months ago
Inferring Channel Buffer Bounds Via Linear Programming
We present a static analysis for inferring the maximum amount of buffer space used by a program consisting of concurrently running processes communicating via buffered channels. We...
Tachio Terauchi, Adam Megacz
ESOP
2008
Springer
13 years 9 months ago
Upper Adjoints for Fast Inter-procedural Variable Equalities
We present a polynomial-time algorithm which at the extra cost of a factor O(k) (k the number of variables) generalizes inter-procedural copy constant propagation. Our algorithm in...
Markus Müller-Olm, Helmut Seidl
ESOP
2008
Springer
13 years 9 months ago
Verification of Equivalent-Results Methods
K. Rustan M. Leino, Peter Müller
ESOP
2008
Springer
13 years 9 months ago
A Realizability Model for Impredicative Hoare Type Theory
We present a denotational model of impredicative Hoare Type Theory, a very expressive dependent type theory in which one can and reason about mutable abstract data types. The model...
Rasmus Lerchedahl Petersen, Lars Birkedal, Aleksan...
ESOP
2008
Springer
13 years 9 months ago
Programming in JoCaml (Tool Demonstration)
Abstract. JoCaml is a language for concurrent and distributed programming. The language is an extension of Objective Caml with concurrent features inspired by the join-calculus. We...
Louis Mandel, Luc Maranget