2014/06/09 by Andreas Abel, James Chapman
Computer Science · #cs.LO #cs.PL
paper · pdf · doi:10.4204/eptcs.153.4
published as EPTCS 153, 2014, pp. 51-67 · In Proceedings MSFP 2014, arXiv:1406.1534
arxiv created 2014/06/09 · arxiv updated 2014/06/10
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.