Casper Bach Poulsen casperbp
rntz
/ MinimalNBE.hs
Last active
May 13, 2024 09:17
Normalisation by evaluation for the simply-typed lambda calculus, in Agda
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -- A simply-typed lambda calculus, and a definition of normalisation by | |
| -- evaluation for it. | |
| -- | |
| -- The NBE implementation is based on a presentation by Sam Lindley from 2016: | |
| -- http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf | |
| -- | |
| -- Adapted to handle terms with explicitly typed contexts (Sam's slides only | |
| -- consider open terms with the environments left implicit/untyped). This was a | |
| -- pain in the ass to figure out. |