Agda (programming language): Difference between revisions

Revision as of 06:13, 19 September 2023

Revision as of 11:43, 1 October 2023

Line 29:

Agda is also a [[proof assistant]] based on the [[propositions-as-types]] paradigm, but unlike [[Coq]], has no separate [[Tactic (computer science)|tactics]] language, and proofs are written in a functional programming style. The language has ordinary programming constructs such as [[data type]]s, [[pattern matching]], [[Record (computer science)|records]], [[let expression]]s and modules, and a [[Haskell (programming language)|Haskell]]-like syntax. The system has [[Emacs]], [[Atom (text editor)|Atom]], and [[VS Code]] interfaces<ref name="emacs-mode">{{cite conference |first1 = Catarina |last1 = Coquand |first2 = Dan |last2 = Synek |first3 = Makoto |last3 = Takeyama |title = An Emacs interface for type directed support constructing proofs and programs |conference = European Joint Conferences on Theory and Practice of Software 2005 |url = https://mailserver.di.unipi.it/ricerca/proceedings/ETAPS05/uitp/uitp_p05.pdf |archive-url = https://web.archive.org/web/20110722063632/https://mailserver.di.unipi.it/ricerca/proceedings/ETAPS05/uitp/uitp_p05.pdf |url-status = dead |archive-date = 2011-07-22 }}</ref><ref>{{cite web |title = agda-mode on Atom |url = https://atom.io/packages/agda-mode |access-date = 7 April 2017 }}</ref><ref>{{Cite web |title=agda-mode - Visual Studio Marketplace |url=https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode |access-date=2023-06-06 |website=marketplace.visualstudio.com |language=en-us}}</ref> but can also be run in batch mode from the command line.

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]], which was named after [[Thierry Coquand]], Catarina Coquand's husband.