Lambda the Ultimate

A Framework for Comparing Models of Computation by Edward A. Lee and Alberto Sangiovanni-Vincentelli, 1998.

We give a denotational framework (a “meta model”) within which certain properties of models of computation can be compared. It describes concurrent processes in general terms as sets of possible behaviors. A process is determinate if, given the constraints imposed by the inputs, there are exactly one or exactly zero behaviors. Compositions of processes are processes with behaviors in the intersection of the behaviors of the component processes. The interaction between processes is through signals, which are collections of events. Each event is a value-tag pair, where the tags can come from a partially ordered or totally ordered set. Timed models are where the set of tags is totally ordered. Synchronous events share the same tag, and synchronous signals contain events with the same set of tags. Synchronous processes have only synchronous signals as behaviors. Strict causality (in timed tag systems) and continuity (in untimed tag systems) ensure determinacy under certain technical conditions. The framework is used to compare certain essential features of various models of computation, including Kahn process networks, dataflow, sequential processes, concurrent sequential processes with rendezvous, Petri nets, and discrete-event systems.

The generality of the approach looks very impressive. Can anyone share first-hand experience with this framework? Would be great to see E compared to Oz!

Coinductive proof principles for stochastic processes, Dexter Kozen, Logical Methods in Computer Science 2007.

We give an explicit coinduction principle for recursively-defined stochastic processes. The principle applies to any closed property, not just equality, and works even when solutions are not unique. The rule encapsulates low-level analytic arguments, allowing reasoning about such processes at a higher algebraic level. We illustrate the use of the rule in deriving properties of a simple coin-flip process.

This paper has a clever little program, a clever little proof principle for it, and exploits connections to a bit of mathematics you don't normally see in PL research.

Here's the deal: Let's design a short booklet of irresistible programs, sure to intrigue and delight programmers and geeks. The programs should be short (one page), real (not made up for this occasion) and preferably of historical value, and must look interesting (bonus points to those suggesting programs written in amusing glyphs).

Here are a couple examples: McCarthy's Lisp (1960), Quicksort in Haskell (and for comparison: Hoare's definition of Partition), first winners of the Obfuscated C Code Contest.

Now is your turn. Which programs do you find simply irresistible?