Normalization by Evaluation in the Delay Monad: A Case Study for Coinduction via Copatterns and Sized Types

TL;DR

This paper formalizes a normalization-by-evaluation technique for simply-typed lambda calculus in Agda, demonstrating coinductive programming with copatterns and sized types for totality proof.

Contribution

It introduces a novel Agda formalization of normalization-by-evaluation using coinductive functions, copatterns, and sized types, showcasing coinductive reasoning in a proof assistant.

Findings

The normalizer is a total function proven via logical relations.

Coinductive programming with copatterns is feasible in Agda.

The approach validates coinductive techniques for normalization in lambda calculus.

Abstract

In this paper, we present an Agda formalization of a normalizer for simply-typed lambda terms. The normalizer consists of two coinductively defined functions in the delay monad: One is a standard evaluator of lambda terms to closures, the other a type-directed reifier from values to eta-long beta-normal forms. Their composition, normalization-by-evaluation, is shown to be a total function a posteriori, using a standard logical-relations argument. The successful formalization serves as a proof-of-concept for coinductive programming and reasoning using sized types and copatterns, a new and presently experimental feature of Agda.