Content deleted Content added
m image |
Extension of the Agda article, including Agda2 precisions, AIM meetings and a link to the wiki |
||
Line 5:
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]]-interface and a [[graphical interface]], Alfa.
==Agda 2==
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. Agda2 also makes an intensive use of [[Unicode]] as a way to obtain easily-readable proofs.
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.
==External links==
* [http://unit.aist.go.jp/cvs/Agda/ Agda project home page]
* [http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php The Agda wiki], including some documentation and a bugreport tool
==References==
| |||