Idris

• Haskell っぽい, 依存型 ある
• 正格評価

参考文献

• 定理証明系言語 - mrsekut-p