SIGPLAN

Ensuring the correctness of multithreaded programs is difficult, due to the potential for unexpected and nondeterministic interactions, between threads. Previous work addressed this problem by devising tools for detecting race conditions, a situation ...

We extend Cyclone, a type-safe polymorphic language at the C level of abstraction, with threads and locks. Data races can violate type safety in Cyclone. An extended type system statically guarantees their absence by enforcing that thread-shared data is ...

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 "boilerplate" code that simply walks the structure, hiding a small amount of "real" ...

As probabilistic computation plays an increasing role in diverse fields in computer science, researchers have designed new languages to facilitate the development of probabilistic programs. In this paper, we develop a probabilistic calculus by extending ...

Various resources such as files and memory are associated with certain protocols about how they should be accessed. For example, a memory cell that has been allocated should be eventually deallocated, and after the deallocation, the cell should no ...

(MATH) We consider a propositional spatial logic for finite trees. The logic includes A ???? Par B (tree composition), A ???? B (the implication induced by composition), and O (the unit of composition). We show that the satisfaction and validity ...

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 of natural deduction-style inference rules. We deploy the logic in a ...

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 tuples and variants directly in the register file. We present an algorithm ...

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 other identically defined datatypes. A natural way of accounting for this is ...

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 code systems that treat the garbage collector as part of the trusted computing ...

In this paper, we prove the safety of integrating region-based memory management and Cheney-style copying garbage collection. The safety property relies on a refinement of the region typing rules that forbids dangling pointers during evaluation.To ...