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.
Answering a question of Henson, Jockush, Rubel and Takeuti, we prove that the rationals, the irrationals and the Cantor set are all elementary equivalent as topological spaces. "Unfortunately, Gurevich's proof ... contains a small gap, which we take the opportunity to fill. The oversight does…
This three-page note is about presenting a paper at a conference, but it offers good advice for any talk. Except for a couple of suggestions about hand-written slides, it still applies today.
A corrigendum was published in ACM Transactions on Programming Languages and Systems 2, 1 (January 1980), 134 and is available here. Like everyone else at the time, when I began studying concurrent algorithms, I reasoned about them behaviorally. Such reasoning typically involved arguments based on…
This circuit expands the capabilities of a balanced analog signal multiplier by adding a third single-polarity input, which can be used as a gain control, for example. The voltage-to-current converter connecting the third input to the modulator chip ensures high linearity for the third input…
Assuming the Continuum Hypothesis, we interprete the theory of (the cardinal of) continuum with quantification over constructible (monadic, dyadic, etc.) predicates in the monadic (second-order) theory of real line, in the monadic theory of any other short non-modest chain, in the monadic topology of Cantor's…
Fortunately, this note has been completely forgotten. It was written when people were still proposing new programming-language constructs. The one presented here may have little to recommend it, but it was no worse than many others.
