pi - An implementation of type-in-type MLTT, with pi, sigma, identity, and natural number types.
hm - An implementation of a Hindley-Milner type system with non-indexed inductive types. Strictly terminating, other than a hole in the positivity checker.