Sciweavers

ESOP
2006
Springer
13 years 8 months ago
Approaches to Polymorphism in Classical Sequent Calculus
Alexander J. Summers, Steffen van Bakel
ESOP
2006
Springer
13 years 8 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 8 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 8 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 8 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
ESOP
2006
Springer
13 years 8 months ago
Inference of User-Defined Type Qualifiers and Qualifier Rules
Abstract. In previous work, we described a new approach to supporting userdefined type qualifiers, which augment existing types to specify and check additional properties of intere...
Brian Chin, Shane Markstrum, Todd D. Millstein, Je...
ESOP
2006
Springer
13 years 8 months ago
Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types
We present a sound and complete proof technique, based on syntactic logical relations, for showing contextual equivalence of expressions in a -calculus with recursive types and imp...
Amal J. Ahmed
ESOP
2006
Springer
13 years 8 months ago
Polymorphic Type Inference for the JNI
We present a multi-lingual type inference system for checking type safety of programs that use the Java Native Interface (JNI). The JNI uses specially-formatted strings to represe...
Michael Furr, Jeffrey S. Foster