Sciweavers

ESOP
2006
Springer
13 years 11 months ago
A Typed Assembly Language for Confidentiality
Language-based information-flow analysis is promising in protecting data confidentiality. Although much work has been carried out in this area, relatively little has been done for ...
Dachuan Yu, Nayeem Islam
ESOP
2006
Springer
13 years 11 months ago
Coinductive Big-Step Operational Semantics
Using a call-by-value functional language as an example, this article illustrates the use of coinductive definitions and proofs in big-step operational semantics, enabling it to d...
Xavier Leroy
ESOP
2006
Springer
13 years 11 months ago
A Verification Methodology for Model Fields
Model fields are specification-only fields that encode abstractions of the concrete state of a data structure. They allow specifications to describe the behavior of object-oriented...
K. Rustan M. Leino, Peter Müller
ESOP
2006
Springer
13 years 11 months ago
Path Optimization in Programs and Its Application to Debugging
We present and solve a path optimization problem on programs. Given a set of program nodes, called critical nodes, we find a shortest path through the program's control flow g...
Akash Lal, Junghee Lim, Marina Polishchuk, Ben Lib...
ESOP
2006
Springer
13 years 11 months ago
Approaches to Polymorphism in Classical Sequent Calculus
Alexander J. Summers, Steffen van Bakel
ESOP
2006
Springer
13 years 11 months ago
Bisimulations for Untyped Imperative Objects
We present a sound and complete method for reasoning about contextual equivalence in the untyped, imperative object calculus of Abadi and Cardelli [1]. Our method is based on bisim...
Vasileios Koutavas, Mitchell Wand
ESOP
2006
Springer
13 years 11 months ago
A Basic Contract Language for Web Services
We design a schema language that includes channel schemas with capabilities of input, output, and input-output. These schemas may describe documents containing references to operat...
Samuele Carpineti, Cosimo Laneve
ESOP
2006
Springer
13 years 11 months ago
Linear Regions Are All You Need
Abstract. The type-and-effects system of the Tofte-Talpin region calculus makes it possible to safely reclaim objects without a garbage collector. However, it requires that regions...
Matthew Fluet, Greg Morrisett, Amal J. Ahmed
ESOP
2006
Springer
13 years 11 months ago
Embedding Dynamic Dataflow in a Call-by-Value Language
This paper describes FrTime, an extension of Scheme designed for writing interactive applications. Inspired by functional reactive programming, the language embeds dynamic dataflow...
Gregory H. Cooper, Shriram Krishnamurthi