Programming Language Foundations in Agda

Agda is a really interesting language. A great way to learn the power of Dependent Types.