Package: wnpp Severity: wishlist Owner: Iain Lane <la...@ubuntu.com> * Package name : agda Version : 2.2.0 Upstream Author : Ulf Norell <u...@chalmers.se> * URL : http://wiki.portal.chalmers.se/agda/ * License : MIT/X11 Programming Lang: Haskell Description : a dependently typed functional programming language and proof assistant
Agda is a dependently typed functional programming language: It has inductive families, which are like 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 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-Lf. It has many similarities with other proof assistants based on dependent types, such as Coq, Epigram and NuPRL. -- System Information: Debian Release: 5.0 APT prefers jaunty-updates APT policy: (500, 'jaunty-updates'), (500, 'jaunty-security'), (500, 'jaunty-backports'), (500, 'jaunty') Architecture: i386 (i686) This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation. -- To UNSUBSCRIBE, email to debian-devel-requ...@lists.debian.org with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org
