Colloquium

We outline the paper and pencil correctness proof for an operating system microkernel written in C. The key ingredients of the proof are 1) a simulation of virtual machines by physical processors with swap memory. Here physical memory serves as a cache for virtual memory.

While men and women use desktop and Internet applications at nearly equal rates, the participation gap in the development of new computing technologies and applications remains undiminished, and may even be widening.

We will describe definitions and algorithmic results for the ``census problem''. Informally, in a census individual respondents give private information to a trusted (and trustworthy) party, who publishes a sanitized version of the data.

Recent election problems have sparked great interest in managing the election process through the use of electronic voting systems.

Google faces two large technical challenges: ensuring that our search results are as relevant as possible, and serving hundreds of millions of queries in a fraction of a second at a reasonable cost.

The American Heritage dictionary defines the term "Black-Box" as

While the traditional IP network supports unicast datagram service, Deering, in his seminal SIGCOMM'88 paper, advocated extending the IP service model and router functionalities to support multicast.