We describe a plan to create an auditable version of Multics. The engineering experiments of that plan are now complete. Type extension as a design discipline has been demonstrated feasible, even for the internal workings of an operating system, where many subtle intermodule dependencies were…
This paper describes a system for full-duplex communication between a time-shared computer and its terminals. The system consists of a communications computer directly connected to the time-shared system, a number of small remote computers to which the terminals are attached, and connecting medium speed telephone…
Homogeneous coordinates have long been a standard tool of computer graphics. They afford a convenient representation for various geometric quantities in two and three dimensions. The representation of lines in three dimensions has, however, never been fully described. This paper presents a homogeneous formulation for…
This paper describes some of the techniques which can be used for managing the run time storage required for an ALGOL68 program. The emphasis is on stack storage, since garbage collection techniques would require another paper. The Frcblems caused by some ALGOL68 constructs are described:…
Classical logic is symmetric with respect to True and False but intuitionistic logic is not. We introduce and study a conservative extension of first-order intuitionistic logic that is symmetric with respect to True and False.
The first-order theory of ordered abelian groups was analyzed in 3. However, algebraic results on ordered abelian groups in the literature usually cannot be stated in first-order logic. Typically they involve so-called convex subgroups. Here we introduce an expanded theory of ordered abelian groups that…
We disprove two Shelah's conjectures and prove some more results on the monadic theory of linearly orderings and topological spaces. In particular, if the Continuum Hypothesis holds then there exist monadic formulae expressing the predicates ``X is countable'' and ``X is meager'' over the real…
When I first learned about the mutual exclusion problem, it seemed easy and the published algorithms seemed needlessly complicated. So, I dashed off a simple algorithm and submitted it to CACM. I soon received a referee's report pointing out the error. This had two effects.…
I wrote this brief note in January, 1977. It came about because I was struck by the use of the term program maintenance, which conjured up in my mind images of lubricating the branch statements and cleaning the pointers. So, I wrote this to make…
In the production of computer generated pictures of three-dimensional objects, one stage of the calculation is the determination of the intensity of a given object once its visibility has been established. This is typically done by modeling the surface as a perfect diffuser, sometimes with…
Several interfaces between a strongly typed language and a storage allocator or deallocator are defined. Using these interfaces, it is possible to program a wide variety of allocation and automatic deallocation strategies: boundary tag allocator, buddy system, reference counting, trace-and-mark garbage collection and many others.…
When I wrote [12], a colleague at Massachusetts Computer Associates pointed out that the concurrent reading and writing of a single register, assumed in the bakery algorithm, requires an arbiter--a device for making a binary decision based on inputs that may be changing. In the…
