There is a new draft on my web page! It is called Tagless and Typeful Normalization by Evaluation using Generalized Algebraic Data Types, which is a mouthful, but only describes accurately the cool new OCaml development we elaborated together with Olivier and Chantal. The world of Normalization by Evaluation (NbE) is still relatively new to me, but its wonders keep amazing me. It’s a program specialization algorithm… no, it’s a completeness proof for first-order logic… wait, it’s a technique to turn an interpreter into a compiler! Definitely, Aarhus University, my new home, is not the worst place to learn about it.
Since the introduction of GADTs in OCaml, a whole new realm of applications emerged, the most well-known being to faithfully represent typed languages: it allows to define compact and correct interpreters, and type-preserving program transformations. Ok, if you never saw this, here is a small snippet that…
View original post 321 more words
