Update on Typeful Normalization by Evaluation

In October, I publicized here a new draft on normalization by evaluation, which provoked some very helpful comments and constructive criticisms. Together with Chantal and Olivier, we thus revised the draft profoundly and a revamped version is available on my web site.

Besides the enhanced form and better explanations, we included a completely new section on what it means for NbE to be written in Continuation-Passing Style, that I am particularly excited about. This allowed us to extend our typeful NbE formalization beyond the minimal λ-calculus to sums and call/cc (which is known to be difficult). Taking our code, you can write a program with call/cc and if statements, and partially evaluate it: all redexes will be removed and your code will be specialized. All this, as before, is done typefully, thanks to OCaml’s GADTs: this means that the transformation is guaranteed to map well-typed terms to well-typed normal forms.

Read the rest of this entry »