The sound modes of He II in a waveguide partially packed with superleak are investigated for the case of a free surface within the waveguide. In the limit of zero vapor density, two propagating modes are found: one a gravity wave whose velocity depends on…
This paper presents three scan line methods for drawing pictures of parametrically defined surfaces. A scan line algorithm is characterized by the order in which it generates the picture element of the image. These are generated left to right, top to bottom in the much…
After graduating from Cornell, Susan Owicki joined the faculty of Stanford. Some time around 1978, she organized a seminar to study the temporal logic that Amir Pnueli had recently introduced to computer science. I was sure that temporal logic was some kind of abstract nonsense…
Sound propagation has been studied in He II films adsorbed on alumina powder grains (Al2O3). Sound velocity and adsorption isotherm data provide evidence that surf ace tension forces can exceed the van der Waals forces as the film thickness increases. A model of capillary condensation…
The file system and modularization of a single-user operating system are described. The main points of interest are the openness of the system, which establishes no sharp boundary between itself and the user’s programs, and the techniques used to make the system robust.
Isolating with four analog switches the frequency-determining portion of the circuit from that controlling the charging and discharging of its RC integrator, this ramp generator achieves independent selection of slope ratio and repetition rate. Such a unit is useful in a music synthesizer, where timbre…
In the May, 1979 CACM, De Millo, Lipton, and Perlis published an influential paper titled Social Process and Proofs of Theorems and Programs. This paper made some excellent observations. However, by throwing in a few red herrings, they came to some wrong conclusions about program…
At a coffee house in Berkeley around 1975, Whitfield Diffie described a problem to me that he had been trying to solve: constructing a digital signature for a document. I immediately proposed a solution. Though not very practical--it required perhaps 64 bits of published key…
In the May, 1978 CACM, Matthew Geller published a paper titled Test Data as an Aid in Proving Program Correctness. He argued that there were some programs whose correctness is so hard to state formally that formally verifying them is useless because the specification is…
I forget what prompted me to be thinking about memory caching, but it occurred to me one day that multiprocessor synchronization algorithms assume that each processor accesses the same word in memory, but each processor actually accesses its own copy in its cache. It hardly…
The composition (or decomposition) method of Feferman-Vaught is generalized and made much more applicable.
We analyze the monadic theory of the rational line and the theory of real line with quantification over "small" subsets. The results are in some sense the best possible.
