Skip to content

Latest commit

 

History

History
28 lines (14 loc) · 1.73 KB

README.md

File metadata and controls

28 lines (14 loc) · 1.73 KB
Raw

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.