[tikhonj]

If you're interested in something similar but a little more theoretical, take a look at "Simply Easy"[1], a little paper on implementing a couple of variations on the lambda calculus. The main idea is to demonstrate how to evaluate a dependently typed language.

It starts by looking at how to evaluate the simply typed lambda calculus and then going from that to a dependently typed lambda calculus. Surprisingly, the transformation is not all that complicated!

The actual code is in Haskell.

[1]: http://strictlypositive.org/Easy.pdf