Agda est un langage de programmation fonctionnel typé de manière dépendante.Il a des familles inductives, c'est-à-dire des types de données qui dépendent de valeurs, comme le type de vecteurs d'une longueur donnée.Il dispose également de modules paramétrés, d'opérateurs de mixfix, de caractères Unicode et d'une interface Emacs interactive qui peut aider le programmeur à écrire le programme.Agda est assistante de preuve.Il s'agit d'un système interactif de rédaction et de vérification d'épreuves.Agda est basé sur la théorie du type intuitionniste, un système fondamental pour les mathématiques constructives développé par le logicien suédois Per Martin-Löf.Il présente de nombreuses similitudes avec d'autres assistants de preuve basés sur des types dépendants, tels que Coq, Epigram, Matita et NuPRL.