Agda

Agda 是一种依赖类型函数式编程语言。它支持归纳族，即依赖于值的数据类型，例如指定长度的向量类型。它还支持参数化模块、混合符号运算符、Unicode 字符，以及一个交互式的 Emacs 界面，可帮助程序员编写程序。
Agda 是一个证明助手。它是一个用于编写和检查证明的交互式系统。Agda 基于直觉类型论，这是一种由瑞典逻辑学家 Per Martin-Löf 开发的构造性数学基础体系。它与基于依赖类型的其他证明助手（如 Coq、Epigram、Matita 和 NuPRL）有许多相似之处。