Agda

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