LICK is a correct-by-construction implementation of the simply-typed lamba calculus' expressions, beta-reduction, and evaluation. It was built during my Habito lunch hours with that dude who writes all the PureScript, Liam.
LICK introduces a few motivating examples for GADTs and dependent types. I wrote a blog series going through all the interesting concepts in this repo :)