ACM DL

Programming Languages and Systems (TOPLAS)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 22 Issue 1, Jan. 2000

Local type inference
Benjamin C. Pierce, David N. Turner
Pages: 1-44
DOI: 10.1145/345099.345100
We study two partial type inference methods for a language combining subtyping and impredicative polymorphism. Both methods are local in the sense that missing annotations are recovered using only information from adjacent nodes...

Lazy rewriting on eager machinery
Wan Fokkink, Jasper Kamperman, Pum Walters
Pages: 45-86
DOI: 10.1145/345099.345102
The article introduces a novel notion of lazy rewriting. By annotating argument positions as lazy, redundant rewrite steps are avoided, and the termination behavior of a term-rewriting system can be improved. Some transformations of rewrite...

An automata-theoretic approach to modular model checking
Orna Kupferman, Moshe Y. Vardi
Pages: 87-128
DOI: 10.1145/345099.345104
In modular verification the specification of a module consists of two part. One part describes the guaranteed behavior of the module. The other part describes the assumed behavior of the system in which the module is...

Efficient and safe-for-space closure conversion
Zhong Shao, Andrew W. Appel
Pages: 129-161
DOI: 10.1145/345099.345125
Modern compilers often implement function calls (or returns) in two steps: first, a “closure” environment is properly installed to provide access for free variables in the target program fragment; second, the control is transferred...

Undecidability of context-sensitive data-dependence analysis
Thomas Reps
Pages: 162-186
DOI: 10.1145/345099.345137
A number of program-analysis problems can be tackled by transforming them into certain kinds of graph-reachability problems in labeled directed graphs. The edge labels can be used to filter out paths that are not interest: a path...