To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

Normalization by evaluati… - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on

Normalization by evaluation in the delay monad: A case study for coinduction via copatterns and sized types

Conference paper
Authors Andreas Abel
James Chapman
Published in Electronic Proceedings in Theoretical Computer Science, EPTCS
ISSN 2075-2180
Publication year 2014
Published at Department of Computer Science and Engineering (GU)
Language en
Subject categories Software Engineering, Theoretical computer science


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 h-long b-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.

Page Manager: Webmaster|Last update: 9/11/2012

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?