Typeful Normalization by Evaluation

International audienceWe present the first typeful implementation of Normalization by Evaluation for the simply typed λ-calculus with sums and control operators: we guarantee type preservation and η-long (modulo commuting conversions), β-normal forms using only Generalized Algebraic Data Types in a general-purpose programming language, here OCaml; and we account for sums and control operators with Continuation-Passing Style. Our presentation takes the form of a typed functional pearl. First, we implement the standard NbE algorithm for the implicational fragment in a typeful way that is correct by construction. We then derive its continuation-passing counterpart, in call-by-value and call-by-name, that maps a λ-term with sums and call/cc into a CPS term in normal form, which we express in a typed, dedicated syntax. Beyond showcasing the expressive power of GADTs, we emphasize that type inference gives a smooth way to re-derive the encodings of the syntax and typing of normal forms in Continuation-Passing Style