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

Andreas Abel, James Chapman

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: On…