Programming Languages and Systems (TOPLAS)


Search Issue
enter search term and/or author name


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...