Content deleted Content added
Hatnote to distinguish from Ada |
add link |
||
Line 27:
</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.
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]] and [[Atom (text editor)|Atom]] 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> 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]].
| |||