Abstracts.2018.NbE.STLC

Normalization for typed lambda calculus with co-products

by Nachiappan Valliappan

Abstract

In this talk, I’ll present a normalization technique called “Normalization By Evaluation” (NBE) for the Simply Typed Lambda Calculus with product and sum types (STLC), and it’s implementation in Agda.

For the implementation, we’ll use Andreas’ notes [1] on NBE for Intuitionistic Propositional Calculus (IPC) from an earlier talk (last summer). As we will see, the NBE algorithm for IPC readily adapts to STLC.

Given the Curry-Howard-Lambek correspondence, it is only natural to ask whether this technique can also be used to implement normalization for morphisms in free Bi-Cartesian Closed Categories (BiCCCs). We will ponder over this and observe some subtleties involved in doing so.

Normalization for STLC and free BiCCCs has some very useful corollaries for implementing and optimizing functional languages—something which we’ll also discuss during the talk.

[1] https://andreasabel.github.io/ipl/nbeSum.pdf

Agda implementation

https://github.com/nachivpn/nbe-stlc