Accumulating bindings

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

We give a Haskell implementation of Filinski’s normalisation by evaluation algorithm for the computational lambda-calculus with sums. Taking advantage of extensions to the GHC compiler, our implementation represents object
language types as Haskell types and ensures that type errors are detected statically.
Following Filinski, the implementation is parameterised over a residualising monad. The standard residualising monad for sums is a continuation monad. Defunctionalising the uses of the continuation monad we present the binding
tree monad as an alternative.
Original languageEnglish
Title of host publication2009 Workshop on Normalization by Evaluation
Subtitle of host publicationAugust 15, 2009 Los Angeles, California
Number of pages8
Publication statusPublished - 2009

Fingerprint

Dive into the research topics of 'Accumulating bindings'. Together they form a unique fingerprint.

Cite this