Normal-order direct-style beta-evaluator with syntax-rules, and the repeated applications of call/cc

Oleg's presentation at the workshop in honor of Daniel Friedman is great fun as usual. The topic of repeated applications of call/cc has been mentioned on LtU previously, a few years ago. New this time: the full and correct beta-normalizer written as a direct-style syntax-rule. The normalizer implements calculus of explicit substitutions. The talk presents probably the shortest (and the fastest) normal-order beta-normalizer as a (stand-alone) Scheme macro. Another new feature is the discussion of self-applications of delimited continuation operators. The talk mentions incidentally that shift, control, shift0 and other, less-delimited control operators are the members of the same family: gshift/greset.

Hot stuff.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Normal-order etc.

Oleg's talk was entertaining, and great fun. And his evaluator macro is very clever.

Note that his evaluator is an abstract machine, not a reduction semantics. In fact, it is Krivine's machine with named (rather than de Bruijn indexed) terms.