A simple functional programming language.

Demo for high-performance type theory elaboration

Minimal implementations for dependent type checking and elaboration

Staged compilation with dependent types

Implementation for ICFP 2020 paper

A Teeny Type Theory

😎TT

A pedagogic implementation of abstract bidirectional elaboration for dependent type theory.

🦠 An experimental elaborator for dependent type theory using effects and handlers

A functional programming language based on system F (omega) ft. NbE and higher order unification

Playing with type systems

high-performance cubical evaluation

Setoid type theory implementation

An example implementation of a dependent type theory in OCaml

⛏️ A refinement proof framework for haskell

A bare-bones LCF-style proof assistant

A work-in-progress core language for Agda, in Agda

Demo for dependent types + runtime code generation

A toy dependent typed language.

algebraic typechecking and elaboration of type systems

A dependently-typed language with unboxed data.

An example of how to use LCF + validations to type check and normalize lambda terms (via cut admissibility)