Revision as of 08:32, 21 June 2007 edit UlfNorell (talk \| contribs) 1 edit →Agda 2: added Makoto as emacs mode developer ← Previous edit		Revision as of 14:29, 25 July 2007 edit undo Hairy Dude (talk \| contribs) Extended confirmed users 91,285 edits "Emacs" is a proper noun, so needs capitalising Next edit →
Line 3: '''Agda''' is a theorem prover, i.e. a computer program that can check mathematical proofs. More specifically, it is an [[Interactive theorem proving\|interactive system]] for developing [[constructive proof]]s in a variant of [[Per Martin-Löf]]'s [[Intuitionistic Type Theory\|Type Theory]]. It can also be seen as a [[functional programming language]] with [[dependent type]]s and was developed at [[Chalmers University of Technology]]. Agda is based on the idea of direct manipulation of proof-term and not on tactics. The proof is a term, not a script. The language has ordinary programming constructs such as data-types and case-expressions, signatures and records, let-expressions and modules. The system has an [[~~emacs~~Emacs]]- interface and a [[graphical interface]], Alfa. ==Agda 2== Line 9: The second version of Agda, Agda 2, is currently being developed at [[Chalmers_University_of_Technology\|Chalmers]] by Ulf Norell. The syntax has completely changed from Agda 1 (though some conversion tools are being developed as well), introducing for instance implicit variables, that can be omitted when deduceable from the context. Agda 2 also makes an intensive use of [[Unicode]] as a way to obtain easily-readable proofs. Agda 2 provides either a commandline tool or a powerful [[~~emacs~~Emacs]] mode, developed by Makoto Takeyama and Nils Anders Danielsson. The 6th Agda Implementor's Meeting was held in [[Göteborg]] in May 2007. AIM7 is scheduled for november in [[Osaka]] and should focus on the transition from Agda 1 to Agda 2. Line 20: ==References== * C. Coquand et al. An ~~emacs-~~Emacs interface for type directed support constructing proofs and programs. ENTCS 2006. * A. Abel, et al. Verifying [[Haskell (programming language)\|Haskell]] Programs Using Constructive Type Theory, ACM SIGPLAN Workshop Haskell'05, Tallinn, Estonia, 30 September, 2005 http://www.tcs.informatik.uni-muenchen.de/~abel/haskell05.pdf * M. Benke et al. Universes for generic programs and proofs in dependent type theory. Nordic Journal of Computing, 10(4):265-289, 2003. http://www.cs.chalmers.se/~marcin/Papers/universes.pdf

Agda (programming language): Difference between revisions