Skip to content

Instantly share code, notes, and snippets.

rntz / MinimalNBE.hs
Last active Apr 21, 2019
Normalisation by evaluation for the simply-typed lambda calculus, in Agda
View MinimalNBE.hs
-- 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:
-- 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.
View default.nix
# 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 = "";
src = ./.;