Agda (programming language): Difference between revisions

Revision as of 23:34, 11 June 2020

Revision as of 18:50, 24 October 2020

Line 30:

Agda is based on Zhaohui Luo's [[unified theory of dependent types]] (UTT),<ref>Luo, Zhaohui. ''Computation and reasoning: a type theory for computer science''. Oxford University Press, Inc., 1994.</ref> a type theory similar to [[Intuitionistic type theory|Martin-Löf type theory]].

Agda is named after the [[Swedish language|Swedish]] song "Hönan Agda", written by [[Cornelis Vreeswijk]],<ref>{{citationcite web needed|title = [Agda] origin of "Agda"? (Agda mailing list)|url = https://lists.chalmers.se/pipermail/agda/2016/008867.html |access-date =November 201924 Oct 2020}}</ref> which is about a [[Chicken#Terminology|hen]] named Agda. This alludes to the naming of [[Coq]].

== Features ==