The semantics of hardware description languages can be represented in higher order logic. This provides a formal definition that is suitable for machine processing. Experiments are in progress at Cambridge to see whether this method can be the basis of practical tools based on the…
When I developed TLA, I realized that, for the first time, I had a formalism that really was completely formal--so formal that mechanically checking TLA proofs should be straightforward. Working out a tiny example (the specification and trivial implementation of mutual exclusion) using the LP…
Part I. The Pathfinder project Pathfinder is an expert system that assists surgical pathologists with the diagnosis of lymph-node diseases. The program is one of a growing number of normative expert systems that use probability and decision theory to acquire, represent, manipulate, and explain uncertain…
Providing high concurrency in B+ -trees has been studied extensively. But few efforts have been documented for combining concurrency methods with a recovery scheme that preserves well-formed trees across system crashes. We describe an approach for this that works for a class of index trees…
We describe how we selectively reformulate portions of a belief network that pose difficulties for solution with a stochastic-simulation algorithm. With employ the selective conditioning approach to target specific nodes in a belief network for decomposition, based on the contribution the nodes make to the…
It is shown that if X and Y are jointly distributed random variables such that the regression function of Y on Xis linear and is the inverse of that of X on Y then the joint distribution of X and Y is degenerate, if second moments exist.
Research on computer-based decision support in medical informatics has been concerned largely with the development of representation and inference methodologies, and the delivery of reasoning techniques on traditional computing platforms. Nevertheless, there has been growing attention to the development of more powerful and elegant human-computer…
C has been used as a portable target language for implementing languages like Standard ML and Scheme. Previous efforts at compiling these languages to C have produced efficient code, but have compromised on portability and proper tail recursion. We show how to compile Standard ML…
The general subset sum problem is NP-complete. However, there are two algorithms, one due to Brickell and the other to Lagarias and Odlyzko, which in polynomial time solve almost all subset sum problems of sufficiently low density. Both methods rely on basis reduction algorithms to…
This document describes the OpenGL graphics system: what it is, how it acts, and what is required to implement it. We assume that the reader has at least a rudimentary understanding of computer graphics. This means familiarity with the essentials of computer graphics algorithms as…
We show how local spatial image frequency is related to the surface normal of a textured surface. We find that the Fourier power spectra of any two similarly textured patches on a plane are approximately related to each other by an affine transformation. The transformation…
Profiling tools, which measure and display the dynamic space and time behaviour of programs, are essential for identifying execution bottlenecks. A variety of such tools exist for conventional languages, but almost none for non-strict functional languages. There is a good reason for this: lazy evaluation…
