FingerTree.h : ephemeral finger tree.
Poly.agda : formalization of a higher-kinded (HM-like) type system.
fol.v : formalization of first order logic. too silly though.
phoas.ml : try parameterized higher-order abstract syntax.
rbt.ml : persistent red-black tree.
turing.scm : a simple turing-machine dsl.
wbt.cpp : persistent weight-balanced tree with maximal sharing.