Agda

correspon Martin matchin

Agda是一個依賴類型函式式程式語言，同時亦是一個用於構建構造性證明的證明輔助器。它建立在柯里-霍華德同構（Curry-Howardcorrespondence）的基礎上，踐行了PerMartin-Löf的直覺類型論。Agda的現行版本，Agda2，系由瑞典查爾摩斯工學院的研究工程師烏爾夫·諾雷爾在原有的基礎上完全重寫。
Agda不同於Coq之處在於，它包含了有限的對tactics的支持，而證明全部以函式式程式的方式書寫。語言本身吸收了常規的程式語言構造，諸如：數據類型、模式匹配（patternmatching）、記錄類型（records）、let表達式和模組（modules）等，而其語法則高度類仿Haskell。Agda系統一般通過其提供的Emacs界面進行互動，亦可藉由命令行方式執行。
目前Agda擁有三個編譯器後端的實現：目標為Haskell平台的MAlonzo；一個編譯到JavaScript的後端；以及Epic後端。