MiniAgda

MiniAgda 是一门整合了 sized type 和 dependent type 的编程语言，支持 inductive datatype 和 coinductive datatype 以及他们各自的 termination check 和 productivity check。

源码：https://github.com/andreasabel/miniagda
网站：http://www.cse.chalmers.se/~abela/miniagda

网站做的很漂亮