most citedNormalization by Evaluation in the Delay Monad: A Case Study for Coinduction via Copatterns and Sized Types

21 citations · 37 across the 3 of their papers we have counts for

collaborators
Showing cs.LOShow all

2 papers · 1 filter

cs.LO2014★ 21 cited

Normalization by Evaluation in the Delay Monad: A Case Study for Coinduction via Copatterns and Sized Types

Andreas Abel, James Chapman

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: On…

cs.LO2012

Proceedings Fourth Workshop on Mathematically Structured Functional Programming

James Chapman, Paul Blain Levy

This volume contains the proceedings of the Fourth Workshop on Mathematically Structured Functional Programming (MSFP 2012), taking place on 25 March, 2012 in Tallinn, Estonia, as…