Agda

呢篇文可能要清理或者重寫，令佢更符合維基百科嘅質素標準。 如果你有能力又咁啱得閒，可以改善吓呢篇文。

Agda 係一個依賴類型嘅純函數式程式語言。依家嘅版本，Agda 2，最初由瑞典查爾摩斯工學院嘅 Ulf Norell 作為博士論文課題設計同埋實現。先前的版本 Agda 1 由 Catarina Coquand 喺 1999 年開發，而依家嘅版本則係對佢嘅徹底重寫，所以可以睇做一個全新嘅語言，但係保留咗 Agda 嘅命名同埋傳統。

 Agda係電算楔位文，你可以編輯佢充實內容。