Agda (programming language): Difference between revisions

Revision as of 23:00, 14 April 2023

Revision as of 09:07, 18 April 2023

Line 31:

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>{{cite web |title = [Agda] origin of "Agda"? (Agda mailing list)|url = https://lists.chalmers.se/pipermail/agda/2016/008867.html |access-date = 24 Oct 2020}}</ref> which is about a [[Chicken#Terminology|hen]] named Agda. This alludes to the namingname of the theorem prover [[Coq]], which was named after [[Thierry Coquand]], Catarina Coquand's husband.

== Features ==