roconnor
JLimperg
/ default.nix
Created
November 22, 2014 14:17
— forked from bennofs/default.nix
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
| # This file was auto-generated by cabal2nix. Please do NOT edit manually! | |
| { cabal, convertible, exceptions, HDBC, HDBCSqlite3, monadHdbc, mtl | |
| , options, text, time, transformers | |
| }: | |
| cabal.mkDerivation (self: { | |
| pname = "scrumgr"; | |
| version = "0.1.0.0"; | |
| src = ./.; |
rntz
/ MinimalNBE.hs
Last active
November 21, 2023 15: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. |