Jump to content

Agda (programming language)

From Wikipedia, the free encyclopedia

This is an old revision of this page, as edited by Patrikj (talk | contribs) at 23:27, 17 March 2006 (Created stub for the Agda prover). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

(diff) ← Previous revision | Latest revision (diff) | Newer revision → (diff)

Agda is an interactive system for developing constructive proofs in a variant of Martin Löf's type theory.

Agda can also be seen as a functional language with dependent types.

See also

Intuitionistic Type Theory

External links

Agda project home page

References

C. Coquand et al. An emacs-interface for type directed support constructing proofs and programs. ENTCS 2006.

A. Abel, et al. Verifying {Haskell} Programs Using Constructive Type Theory, ACM SIGPLAN Workshop Haskell'05, Tallinn, Estonia, 30 September, 2005

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

T. Coquand et al. Connecting a Logical Framework to a First-Order Logic Prover. FroCos 2005, pp. 285-301.

This mathematics-related article is a stub. You can help Wikipedia by expanding it.

Retrieved from "https://en.wikipedia.org/w/index.php?title=Agda_(programming_language)&oldid=44278230"

Hidden category:

All stub articles