Agda (programming language): Difference between revisions

Revision as of 11:33, 27 April 2020

Revision as of 13:39, 27 April 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]] ,{{citation needed|date=November 2019}}, thatwhich is about a [[Chicken#Terminology|hen]] named Agda. This alludes to the naming of [[Coq]].

== Features ==