Back Agda Greek آگدا (زبان برنامهنویسی) Persian Agda Japanese Agda Korean Agda Dutch Agda Russian Agda Ukrainian Agda Chinese Agda ZH-YUE
&sq=XXXTENTACION&lang=en&file=File:Agda%27s_official_logo.svg){kind=logo} | |
| Paradigm | Functional |
|---|---|
| Designed by | Ulf Norell; Catarina Coquand (1.0) |
| Developer | Ulf Norell; Catarina Coquand (1.0) |
| First appeared | 2007 (1.0 in 1999) |
| Stable release | 2.6.3
/ January 30, 2023 |
| Typing discipline | strong, static, dependent, nominal, manifest, inferred |
| Implementation language | Haskell |
| OS | Cross-platform |
| License | BSD-like[1] |
| Filename extensions | .agda, .lagda, .lagda.md, .lagda.rst, .lagda.tex |
| Website | wiki |
| Influenced by | |
| Coq, Epigram, Haskell | |
| Influenced | |
| Idris | |
Agda is a dependently typed functional programming language originally developed by Ulf Norell at Chalmers University of Technology with implementation described in his PhD thesis.[2] The original Agda system was developed at Chalmers by Catarina Coquand in 1999.[3] 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 tactics language, and proofs are written in a functional programming style. The language has ordinary programming constructs such as data types, pattern matching, records, let expressions and modules, and a Haskell-like syntax. The system has Emacs, Atom, and VS Code interfaces[4][5][6] 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),[7] a type theory similar to Martin-Löf type theory.
Agda is named after the Swedish song "Hönan Agda", written by Cornelis Vreeswijk,[8] which is about a hen named Agda. This alludes to the name of the theorem prover Coq, which was named after Thierry Coquand.
- ^ Agda license file
- ^ Ulf Norell. Towards a practical programming language based on dependent type theory. PhD Thesis. Chalmers University of Technology, 2007. [1]
- ^ "Agda: An Interactive Proof Editor". Archived from the original on 2011-10-08. Retrieved 2014-10-20.
- ^ Coquand, Catarina; Synek, Dan; Takeyama, Makoto. An Emacs interface for type directed support constructing proofs and programs (PDF). European Joint Conferences on Theory and Practice of Software 2005. Archived from the original (PDF) on 2011-07-22.
- ^ "agda-mode on Atom". Retrieved 7 April 2017.
- ^ "agda-mode - Visual Studio Marketplace". marketplace.visualstudio.com. Retrieved 2023-06-06.
- ^ Luo, Zhaohui. Computation and reasoning: a type theory for computer science. Oxford University Press, Inc., 1994.
- ^ "[Agda] origin of "Agda"? (Agda mailing list)". Retrieved 24 Oct 2020.
© MMXXIII Rich X Search. We shall prevail. All rights reserved. Rich X Search