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 21 Issue 3, May 1999

Reasoning about Grover's quantum search algorithm using probabilistic wp
Michael Butler, Pieter Hartel
Pages: 417-429
DOI: 10.1145/319301.319303
Grover's search algorithm is designed to be executed on a quantum-mechanical computer. In this article, the probabilistic wp-calculus is used to model and reason about Grover's algorithm. It is demonstrated that the calculus...

Compile-time memory reuse in logic programming languages through update in place
Gudjón Gudjónsson, William H. Winsborough
Pages: 430-501
DOI: 10.1145/319301.319309
Standard implementation techniques for single-assignment languages modify a data structure without destroying the original, which may subsequently be accessed. Instead a variant structure is created by using newly allocated cells to represent...

Should your specification language be typed
Leslie Lamport, Lawrence C. Paulson
Pages: 502-526
DOI: 10.1145/319301.319317
Most specification languages have a type system. Type systems are hard to get right, and getting them wrong can lead to inconsistencies. Set theory can serve as the basis for a specification language without types. This possibility, which has...

From system F to typed assembly language
Greg Morrisett, David Walker, Karl Crary, Neal Glew
Pages: 527-568
DOI: 10.1145/319301.319345
We motivate the design of typed assembly language (TAL) and present a type-preserving ttranslation from Systemn F to TAL. The typed assembly language we pressent is based on a conventional RISC assembly language, but its static type sytem...

Efficient logic variables for distributed computing
Seif Haridi, Peter Van Roy, Per Brand, Michael Mehl, Ralf Scheidhauer, Gert Smolka
Pages: 569-626
DOI: 10.1145/319301.319347
We define a practical algorithm for distrubuted rational tree unification and prove its correctness in both the off-line and on-line cases. We derive the distributed algorithm from a centralized one, showing clearly the trade-offs between local...

Partial redundancy elimination in SSA form
Robert Kennedy, Sun Chan, Shin-Ming Liu, Raymond Lo, Peng Tu, Fred Chow
Pages: 627-676
DOI: 10.1145/319301.319348
The SSAPRE algorithm for performing partial redundancy elimination based entirely on SSA form is presented. The algorithm is formulated based on a new conceptual framework, the factored redundancy graph, for analyzing redundancy, and representes...

Specificational functions
J. M. Morris, A. Bunkenburg
Pages: 677-701
DOI: 10.1145/319301.319350
Mathematics supplies us with various operators for creating functions from relations, sets, known functions, and so on. Function inversion is a simple example. These operations are useful in specifying programs. However, many of them have strong...