This paper describes a cryptographic scheme for holding a secure secret ballot election in which all communication is public. Voters cast their votes electronically, suitably encrypted, and a “government” releases a tally and a proof of its correctness which can be verified by all.
This paper appeared in a workshop held in Colle-sur-Loup, in the south of France, in October, 1984. There is a long history of work on the semantics of programming languages. When people began studying concurrency in the 70s, they naturally wrote about the semantics of…
In this chapter we make a case for the monadic second-order logic (that is to say, for the extension of first-order logic allowing quantification over monadic predicates) as a good source of theories that are both expressive and manageable. We illustrate two powerful decidability techniques…
Define a tree to be any partial order satisfying the following requirement: if (y < x and z < x) then (y < z or y = z or y > z). The main result of the two papers [62, 63] is the decidability of…
The first announcement of the "new thesis", latern known as the Abstract State Machine thesis.
Among the advantages claimed for a purely functional programming style is ease of designing and implementing large programs. However, little experience of actually doing so has been gained so far. The experience of writing a particular medium sized program in a functional language is described…
There has been a great deal of interest among artificial intelligence researchers in methodologies for using subjective measures of belief for reasoning about uncertain events. We emphasize the fundamental difference between the use of measures of absolute belief and measures of change in belief. We…
The Web search ranking task has become increasingly important due to the rapid growth of the internet. With the growth of the Web and the number of Web search users, the amount of available training data for learning Web ranking models has also increased. We…
The zero-one law, known to hold for first-order logic but not for monadic or even existential monadic second-order logic, is generalized to the extension of first-order logic by the least (or iterative) fixed-point operator. We also show that the problem of deciding, for any pi,…
The distributed snapshot algorithm described here came about when I visited Chandy, who was then at the University of Texas in Austin. He posed the problem to me over dinner, but we had both had too much wine to think about it right then. The…
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…
