Agda (programming language): Difference between revisions

Revision as of 03:00, 13 December 2023

Revision as of 08:01, 16 May 2024

Line 24:

| website = {{URL|wiki.portal.chalmers.se/agda}}

}}

'''<span lang="Ru">Agda</span>''' is a [[Dependent type|dependently typed]] [[functional programming]] language originally developed by Ulf Norell at [[Chalmers University of Technology]] with implementation described in his PhD thesis.<ref>Ulf Norell. Towards a practical programming language based on dependent type theory. PhD Thesis. Chalmers University of Technology, 2007. [http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf]

</ref> The original Agda system was developed at Chalmers by Catarina Coquand in 1999.<ref>{{Cite web |url = http://ocvs.cfv.jp/Agda/index.html |title = Agda: An Interactive Proof Editor |access-date = 2014-10-20 |archive-url = https://web.archive.org/web/20111008115843/http://ocvs.cfv.jp/Agda/index.html |archive-date = 2011-10-08 |url-status = dead }}</ref> The current version, originally known as Agda 2, is a full rewrite, which should be considered a new language that shares a name and tradition.