ICFP 2022
Sun 11 - Fri 16 September 2022 Ljubljana, Slovenia
Sun 11 Sep 2022 14:00 - 14:18 at Club CD - TyDe 3 / Zena's Birthday 1 Chair(s): Gabriel Scherer, Marco Gaboardi

Normalization-by-Evaluation (NbE) is a well-established technique for normalizing terms via an interpretation in a semantic domain. NbE provides a unified treatment of the implementation and verification of normalization algorithms, but extending it to support new features requires a certain amount of ingenuity and is often achieved in an ad hoc manner. Free extensions (frex) are a new technique for partial evaluation based on concepts from universal algebra. We present NbE for a language with higher-order functions and an algebraic structure over a primitive type. Augmenting NbE with a frex for the algebraic structure yields a generic NbE algorithm that works for all such instantiations, and thus for all primitive types with this structure. We show that this implementation also seamlessly extends to the inclusion of a monadic construct for information-flow control. We outline ongoing work extending frex to deal with higher-order features, programmatically in OCaml and semantically through Cartmell’s generalised algebraic theories.

Sun 11 Sep

Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change

14:00 - 15:30
TyDe 3 / Zena's Birthday 1TyDe at Club CD
Chair(s): Gabriel Scherer INRIA Saclay, Marco Gaboardi Boston University
14:00
18m
Short-paper
Normalization by Evaluation with Free Extensions (Extended Abstract)
TyDe
Nathan Corbyn University of Oxford, Ohad Kammar University of Edinburgh, Sam Lindley The University of Edinburgh, UK, Nachiappan Valliappan Chalmers University of Technology, Jeremy Yallop University of Cambridge
Pre-print
14:18
18m
Talk
Zena's birthday introduction
TyDe
Marco Gaboardi Boston University
14:36
18m
Talk
Compiling without continuations
TyDe
Simon Peyton Jones Epic Games
14:54
18m
Talk
On the power of syntactic methods: It is all syntax after all…
TyDe
Amr Sabry Indiana University
15:12
18m
Talk
The impact of delimited control and call-by-need in proof theory
TyDe