surface

interval-functor

General purpose intervals of functors.

abstract-interpretation

Experiments in abstracting definitional interpreters

tilec

Sometimes when I feel sad I implement a dependently typed lambda calculus.

coatl

silly dependently-typed language

Manifold

Another experiment in dependently typed languages, this time with some quantitative type theory s...

sprite-lang

An tutorial-style implementation of liquid/refinement types for a subset of Ocaml/Reason.

path

A lambda calculus to explore type-directed program synthesis.

higher-rank

A small Haskell implementation of Complete and Easy Bidirectional Typechecking for Higher-Rank Po...

language-haskell-ast

Generic interface over the AST provided by haskell-src-exts

seq

a µµ̃ calculus with pretty-printing and evaluating interpreters

cha

A port of miniprl to Haskell with co-/inductive types bolted on the side.

derivative-parsing

Parsing with Derivatives, in Haskell, with GADTs.

haskell-proofs

Examples using dependent types for mathematical proofs at the type level

type-systems

ui-effects

An experiment towards a UI programming model inspired by algebraic effects.