Abstract

I’ll present an informal, friendly walkthrough of the technique of normalization by evaluation (NbE), which is the underlying normalization technology in Idris and Agda. NbE is useful not only as an implementation technology for proof systems, but also for metatheory.

Whiteboard Photos