math/hs-Agda/pkg-descr

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