your first link points to Tim Sheard's Omega, a dependently typed programming language. Dependent types allow the programmer to codify arbitrary invariants in t

your first link points to Tim Sheard's Omega, a dependently typed programming language. Dependent types allow the programmer to codify arbitrary invariants in the types of the expressions. Some notes on depend types: http://axisofeval.blogspot.com/2010/10/notes-on-dependent-types.html http://axisofeval.blogspot.com/2010/10/notes-on-dependent-ty...