Normalization by Evaluation (NBE)

This repo contains a Scala port of the code that has been demonstrated in a tutorial written by David Christiansen.

• Normalizing Untyped λ-Calculus

• Typed Normalization by Evaluation

• Type checking the Tartlet, It's a tiny dependently-typed language (A Tiny Piece of Pie)

  • bidirectional type checking rules for Tartlet

  Feature list: (as listed in tutorial)

  • Add a sum type, Either, with constructors left and right.

  • Add lists and vectors (length-indexed lists).

  • Add non-dependent function types and non-dependent pair types to the type checker. This should not require modifications to the evaluator.

  • Add functions that take multiple arguments, but elaborate them to single-argument Curried functions.

  • Add holes and/or named metavariables to allow incremental construction of programs/proofs.

  • Make the evaluation strategy lazy, either call-by-name or better yet call-by-need.

  • Replace U with an infinite number of universes and a cumulativity relation. To do this, type equality checks should be replaced by a subsumption check, where each type constructor has variance rules similar to other systems with subtyping.