Programming Languages and Systems (TOPLAS)


Search Issue
enter search term and/or author name


ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 30 Issue 4, July 2008

Checking type safety of foreign function calls
Michael Furr, Jeffrey S. Foster
Article No.: 18
DOI: 10.1145/1377492.1377493

Foreign function interfaces (FFIs) allow components in different languages to communicate directly with each other. While FFIs are useful, they often require writing tricky low-level code and include little or no static safety checking, thus...

Relations as an abstraction for BDD-based program analysis
Ondřej Lhoták, Laurie Hendren
Article No.: 19
DOI: 10.1145/1377492.1377494

In this article we present Jedd, a language extension to Java that supports a convenient way of programming with Binary Decision Diagrams (BDDs). The Jedd language abstracts BDDs as database-style relations and operations on relations, and...

Types for atomicity: Static checking and inference for Java
Cormac Flanagan, Stephen N. Freund, Marina Lifshin, Shaz Qadeer
Article No.: 20
DOI: 10.1145/1377492.1377495

Atomicity is a fundamental correctness property in multithreaded programs. A method is atomic if, for every execution, there is an equivalent serial execution in which the actions of the method are not interleaved with actions of other threads....

Java bytecode verification via static single assignment form
Andreas Gal, Christian W. Probst, Michael Franz
Article No.: 21
DOI: 10.1145/1377492.1377496

Java Virtual Machines (JVMs) traditionally perform bytecode verification by way of an iterative dataflow analysis. Bytecode verification is necessary to ensure type safety because temporary variables in the JVM are not statically typed. We present...

Remote specialization for efficient embedded operating systems
Sapan Bhatia, Charles Consel, Calton Pu
Article No.: 22
DOI: 10.1145/1377492.1377497

Prior to their deployment on an embedded system, operating systems are commonly tailored to reduce code size and improve runtime performance. Program specialization is a promising match for this process: it is predictable and modules, and it...

Register allocation for software pipelined multidimensional loops
Hongbo Rong, Alban Douillet, Guang R. Gao
Article No.: 23
DOI: 10.1145/1377492.1377498

This article investigates register allocation for software pipelined multidimensional loops where the execution of successive iterations from an n-dimensional loop is overlapped. For single loop software pipelining, the lifetimes of a loop...

Local reasoning about a copying garbage collector
Noah Torp-Smith, Lars Birkedal, John C. Reynolds
Article No.: 24
DOI: 10.1145/1377492.1377499

We present a programming language, model, and logic appropriate for implementing and reasoning about a memory management system. We state semantically what is meant by correctness of a copying garbage collector, and employ a variant of the novel...