Normalization by Evaluation in the Delay Monad: An Extended Case Study for Coinduction Via Copatterns

In this paper, we present an Agda formalization of a normalizer for simply-typed lambda terms and its accompanying normalization proof. 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. This paper builds on our workshop paper[Abel and Chapman, 2014] which presented only the normalizer and termination proof. Here we also show soundness and completeness of the normalizer, thus completing the normal-ization proof. The complete 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.