MiniAgda, an experimental language with sized dependent types. (http://www.tcs.ifi.lmu.de/~abel/miniagda)