Agda (programming language): Difference between revisions

Revision as of 00:50, 17 September 2024

Revision as of 14:12, 17 September 2024

Line 8:

| paradigm = [[Functional programming|Functional]]

| designer = Ulf Norell; Catarina Coquand (1.0)

| developer = Ulf[[Chalmers Norell;University Catarinaof Coquand (1.0)Technology]]

| released = 1.0 – {{Start date and age|1999}}<br/>2.0 – {{Start date and age|2007}}

| latest release version = 2.7.0

| latest release date = {{Start date and age|2024|08|16}}

Line 26:

}}

'''Agda''' is a [[Dependent type|dependently typed]] [[Functional programming|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/ |title=Agda: An Interactive Proof Editor |access-date=2014-10-20 |archive-url=https://web.archive.org/web/20111008115843/http://ocvs.cfv.jp/Agda/ |archive-date=2011-10-08 |url-status=dead}}</ref> The current version, originally known asnamed Agda 2, is a full rewrite, which should be considered a new language that shares a name and tradition.

Agda is also a [[proof assistant]] based on the [[''propositions-as-types]]'' paradigm ([[Curry–Howard correspondence]]), but unlike [[Coq (software)|Coq]], has no separate ''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]]-like [[Syntax (programming languages)|syntax]]. The system has [[Emacs]], [[Atom (text editor)|Atom]], and [[VS Code]] interfaces<ref name="emacs-mode">{{cite conference |last1=Coquand |first1=Catarina |last2=Synek |first2=Dan |last3=Takeyama |first3=Makoto |date=2005 |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 processing]] mode from thea [[command -line interface]].

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]].