Research on encryption-based secure communication protocols has reached a stage where it is feasible to construct end-to-end secure protocols. The design of such a protocol, built as part of a remote procedure call package, is described. The security abstraction presented to users of the package,…
An experimental methodology for contrasting certain design alternatives and quickly determining user preferences and performance tradeoffs is presented. It is shown how this experimental paradigm, used for psychophysical measurement, may be applied to the field of human-computer interaction. Where it can be applied, it promises…
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…
