I must have spent a lot of time at SRI arguing with Schwartz and Melliar-Smith about the relative merits of temporal logic and transition axioms. (See the discussion of [50].) I don't remember exactly what happened, but this paper's acknowledgment section says that "they kept…
The effect of pressure anisotropy on the stability of ideal-MHD ballooning modes is studied for a large-aspect-ratio tokamak of circular cross-section. Significant increase of the perpendicular energy of electrons or ions can cause strong modifications of the stability boundary, especially at low shear.
Practical implementation of Byzantine agreement requires synchronized clocks. For an implementation to tolerate Byzantine faults, it needs a clock synchronization algorithm that can tolerate those faults. When I arrived at SRI, there was a general feeling that we could synchronize clocks by just having each…
The minimal Gddel class with identity (MGCI) is the class of closed, prenex quantificational formulas whose prefixes have the form Vx1 Vx2x3 and whose matrices contain arbitrary predicate letters and the identity sign " = ", but contain no function signs or individual constants. The…
I have observed that the arbiter problem, discussed in [22], occurs in daily life. Perhaps the most common example is when I find myself unable to decide for a fraction of a second whether to stop for a traffic light that just turned yellow or…
This three-page note gives an example that appears to contradict a theorem in a TOPLAS article by Gary Peterson. Whether or not it does depends on the interpretation of the statement of the theorem, which is given only informally in English. I draw the moral…
A small set of constructs can simulate a wide variety of apparently distinct features in modern programming languages. Using a kernel language called Pebble based on the typed lambda calculus with bindings, declarations, dependent types, and types as compile-time values, we show how to build…
This is the invited address I gave at the 1983 PODC conference, which I transcribed from a tape recording of my presentation. The first few minutes of the talk were not taped, so I had to reinvent the beginning. This talk is notable because it…
This is the preliminary conference version of [62].
C onsider the fine coordination between the eye and the hand of a young child who picks a cookie out of a jar. Although the cookies are roughly uniform in size and shape, the pile of cookies at the top of the jar is a…
This is an extended abstract I submitted to the 1995 POPL conference. (I never wrote the complete version.) It proposes the idea of recursive compiling, in which a program constructs a text string and calls the compiler to compile it in the context of the…
My generalized Hoare logic requires reasoning about control predicates, using the at, in, and after predicates introduced in [47]. These are not independent predicates--for example, being after one statement is synonymous with being at the following statement. At some point, Schneider and I realized that…
