Sciweavers

17
Voted
TLDI
2003
ACM
135views Formal Methods» more  TLDI 2003»
13 years 10 months ago
Typed compilation of recursive datatypes
Standard ML employs an opaque (or generative) semantics of datatypes, in which every datatype declaration produces a new type that is different from any other type, including othe...
Joseph Vanderwaart, Derek Dreyer, Leaf Petersen, K...
TLDI
2003
ACM
102views Formal Methods» more  TLDI 2003»
13 years 10 months ago
A typed interface for garbage collection
An important consideration for certified code systems is the interaction of the untrusted program with the runtime system, most notably the garbage collector. Most certified cod...
Joseph Vanderwaart, Karl Crary
TLDI
2003
ACM
134views Formal Methods» more  TLDI 2003»
13 years 10 months ago
Scrap your boilerplate: a practical design pattern for generic programming
We describe a design pattern for writing programs that traverse data structures built from rich mutually-recursive data types. Such programs often have a great deal of “boilerpl...
Ralf Lämmel, Simon L. Peyton Jones
TLDI
2003
ACM
110views Formal Methods» more  TLDI 2003»
13 years 10 months ago
Type-safe multithreading in cyclone
We extend Cyclone, a type-safe polymorphic language at vel of abstraction, with threads and locks. Data races can violate type safety in Cyclone. An extended type system staticall...
Dan Grossman
TLDI
2003
ACM
121views Formal Methods» more  TLDI 2003»
13 years 10 months ago
Types for atomicity
Ensuring the correctness of multithreaded programs is difficult, due to the potential for unexpected and nondeterministic interactions between threads. Previous work has addresse...
Cormac Flanagan, Shaz Qadeer
TLDI
2003
ACM
115views Formal Methods» more  TLDI 2003»
13 years 10 months ago
Deciding validity in a spatial logic for trees
Cristiano Calcagno, Luca Cardelli, Andrew D. Gordo...
TLDI
2003
ACM
108views Formal Methods» more  TLDI 2003»
13 years 10 months ago
Inferring annotated types for inter-procedural register allocation with constructor flattening
We introduce an annotated type system for a compiler intermediate language. The type system is designed to support inter-procedural register allocation and the representation of t...
Torben Amtoft, Robert Muller
TLDI
2003
ACM
13 years 10 months ago
The logical approach to stack typing
We develop a logic for reasoning about adjacency and separation of memory blocks, as well as aliasing of pointers. We provide a memory model for our logic and present a sound set ...
Amal J. Ahmed, David Walker