Andrej Bauer, one of the authors of PL Zoo, also implemented a mini dependently typed language: https://github.com/andrejbauer/spartan-type-theory