Thursday, 16 January 2014, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Abstract: We present an Agda formalization of a normalizer for simply-typed lambda terms. The first step is to write a coinductive evaluator using the delay monad. The other component of the normalizer, a type-directed reifier from values to eta-long beta-normal forms, resides in the delay monad as well. Their composition, normalization-by-evaluation, is shown to be a total function, using a standard logical-relations argument.
The successful formalization serves as a proof-of-concept for coinductive programming and proving using sized types and copatterns, a new and presently experimental feature of Agda.
This is joint work with Andreas Abel (Chalmers).