Dependently typed functional programming language and proof assistant, originally developed at Chalmers University of Technology. It is used for writing and verifying proofs using a functional style, and it uniquely integrates programming and proving without a separate tactic language. Agda employs rich type systems such as dependent types, supporting inductive families and parameterized modules.