Agda is a dependently typed programming language / interactive theorem prover.
The Agda standard library
Interactive and object-oriented programming in Agda using coinductive types
An implementation of Functional Reactive Programming
Library for proving propositions quantified over finite sets
ECMAScript back end for Functional Reactive Programming in Agda
An implementation of "Associativity for Free"
Simple bindings for parsing, processing and serializing XML
Simple bindings for parsing, processing and serializing URIs
Agda bindings for low-level datatypes such as raw naturals and bytestrings
An makefile with lightweight dependency management
Agda libraries for the semantic web
Bindings to Haskell's IO monad which respect Agda's semantics