Agda

定理証明機。依存型がすごいらしい。