Content deleted Content added
No edit summary Tags: Reverted Mobile edit Mobile web edit |
MaybeitsMir (talk | contribs) m Reverted 1 edit by 41.36.135.172 (talk) to last revision by 2A02:8308:101:CA00:359B:CE83:9C13:1DEC |
||
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 name of the theorem prover [[Coq (software)|Coq]], which was named after [[Thierry Coquand]].
== Features ==
| |||