14 lines
745 B
Text
14 lines
745 B
Text
|
Agda is a dependently typed functional programming language: It has inductive
|
||
|
|
families, which are similar to Haskell's GADTs, but they can be indexed by
|
||
|
|
values and not just types. It also has parameterised modules, mixfix operators,
|
||
|
|
Unicode characters, and an interactive Emacs interface (the type checker can
|
||
|
|
assist in the development of your code).
|
||
|
|
|
||
|
|
Agda is also a proof assistant: It is an interactive system for writing and
|
||
|
|
checking proofs. Agda is based on intuitionistic type theory, a foundational
|
||
|
|
system for constructive mathematics developed by the Swedish logician Per
|
||
|
|
Martin-Lof. It has many similarities with other proof assistants based on
|
||
|
|
dependent types, such as Coq, Epigram and NuPRL.
|
||
|
|
|
||
|
|
WWW: http://wiki.portal.chalmers.se/agda/
|