Lambda the Ultimate

Theory and Practice of Constraint Handling Rules, Thom Fruewirth, Journal of Logic Programming, 1994.

Constraint Handling Rules (CHR) are our proposal to allow more flexibility and application-oriented customization of constraint systems. CHR are a declarative language extension especially designed for writing user-defined constraints. CHR are essentially a committed-choice language consisting of multi-headed guarded rules that rewrite constraints into simpler ones until they are solved.

In this broad survey we cover all aspects of CHR as they currently present themselves. Going from theory to practice, we will define the syntax and semantics of CHR, introduce an important decidable property, confluence, of CHR programs and define a tight integration of CHR with constraint logic programming languages. This survey then describes implementations of the language before we review several constraint solvers -- both traditional and non-standard ones -- written in the CHR language. Finally we introduce two innovative applications that benefited from being written in CHR.

In the last post, we had some requests for constraint programming, so here you go. Constraint solving programs are often essentially stateful algorithms, and I see CHR as a particularly nice way of handling all that state in a declarative way. (They have a very pretty semantics as proof search in linear logic, too.)

The first annual D Programming Language Conference is being held in Seattle this week.

You can get a taste by following the live blogging here.

VamOz: Visual Abstract Machine for Oz

VamOz is a visual abstract machine executing kernel language programs as defined in the book Concepts, Techniques and Models of Computer Programming by Peter Van Roy and Seif Haridi.

VamOz has been developed by Frej Drejhammar and Dragan Havelka with contributions from Christian Schulte. The idea is to give students a tool with which they can increase their understanding of how the abstract machine computes. VamOz has been used successfully in 2003 in the Datalogi II course taught by Christian Schulte at KTH.

A functional correspondence between evaluators and abstract machines by Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard, 2003.

We bridge the gap between functional evaluators and abstract machines for the lambda-calculus, using closure conversion, transformation into continuation-passing style, and defunctionalization of continuations.
We illustrate this bridge by deriving Krivine's abstract machine from an ordinary call-by-name evaluator and by deriving an ordinary call-by-value evaluator from Felleisen et al.'s CEK machine. The first derivation is strikingly simpler than what can be found in the literature. The second one is new. Together, they show that Krivine's abstract machine and the CEK machine correspond to the call-by-name and call-by-value facets of an ordinary evaluator for the lambda-calculus.
We then reveal the denotational content of Hannan and Miller's CLS machine and of Landin's SECD machine. We formally compare the corresponding evaluators and we illustrate some relative degrees of freedom in the design spaces of evaluators and of abstract machines for the lambda-calculus with computational effects.

I was surprized not to find this paper featured in a story on LtU, as it looks very important both from implementation and understanding points of view.
See also more recent paper by Dariusz Biernacki and Olivier Danvy: From Interpreter to Logic Engine by Defunctionalization, which applies similar ideas in context of Prolog-like language.

For a "concepts of programming languages" class back in school I found a book in the library that helped very nicely--but I've since forgotten the title and author! It had a pelican J.J. Audubon-style on the cover, and had, I believe, "semantics" in the title. The author was, I believe, from Iowa St. Anyone know what book this is?