I explained in three blog posts (parts one, two, three) how to implement a small dependent type theory. The language tt is suitable for the PL zoo (and in fact, I stole code from the old PL zoo to implement tt). The repo for tt is at https://github.com/andrejbauer/andromeda (branches blog-part-I, blog-part-II and blog-part-III). Probably the part-III version is most suitable for the PL Zoo.
I explained in three blog posts (parts one, two, three) how to implement a small dependent type theory. The language
ttis suitable for the PL zoo (and in fact, I stole code from the old PL zoo to implementtt). The repo forttis at https://github.com/andrejbauer/andromeda (branchesblog-part-I,blog-part-IIandblog-part-III). Probably the part-III version is most suitable for the PL Zoo.