Agda Agda (programming language)
Agda是一个依赖类型的函数式编程语言，同时亦可作为一个用于构建构造性证明的证明辅助工具。Agda最早由瑞典查尔摩斯工学院的 Ulf Norell 设计并开发，作为他的博士论文课题。目前的版本，Agda 2，则在第一版的基础上完全重写。
Agda体现了柯里-霍华德同构（Curry-Howard correspondence）。它的理论根基是 Zhaohui Luo 的UTT，该理论与 Per Martin-Löf 的直觉类型论相类似。
Agda与Coq的几点显着不同之处在于：它本身并不支持tactics；所有的证明均以函数式编程的方式书写；语言本身吸收了许多常规的进程语言元素，诸如：数据类型、模式匹配（pattern matching）、记录类型（records）、let表达式和模块（modules）等，而其语法则非常类似Haskell。