Agda Agda 是一个依赖类型的纯函数式编程语言目前的版本Agda 最初由瑞典查尔摩斯工学院的 Ulf Norell 作为博士论文课题设计并实现先前的版本 Agda  由 Catarina Coquand 在  年开发而现今的版本则是对其的彻底重写因此可视作一个全新的语言但保留了 Agda 的命名和传统 Agda 的类型系统体现了柯里霍华德同构CurryHoward correspondence因此亦可作为一个构建构造性证明的证明辅助工具英语Proof assistant它的类型理论基于 Zhaohui Luo 提出的 UTTunified theory of dependent types与 Per MartinLöf 的直觉类型论相似 Agda 与另一个基于依赖类型的证明辅助工具 Coq 设计上存在着显著的不同之处它本身并不提供单独的证明策略语言tactics所有的证明均以函数式编程的方式书写Agda 拥有许多常规的函数式程序语言要素诸如数据类型data types模式匹配pattern matching记录类型recordslet表达式和模块modules等而其语法设计则高度仿照 Haskell 语言 用户可通过 Emacs 或 Atom 编辑器的界面与 Agda 系统进行交互Agda 系统亦可藉由命令行单独调用 通过类型检查的 Agda 程序可以被编译到 Haskell并由 GHC 编译器最终编译为可执行的本地机器码亦有编译到 JavaScript 的后端实现 Agda 的名字来自于一首由音乐家 Cornelis Vreeswijk 创作的瑞典语歌曲Hönan Agda歌词讲述了一只名叫 Agda 的母鸡的故事这实际上影射了 CoqCoq 在法语中意为公鸡