O Agda é uma linguagem de programação funcional de tipo dependente.Possui famílias indutivas, ou seja, tipos de dados que dependem de valores, como o tipo de vetores de um determinado comprimento.Ele também possui módulos parametrizados, operadores mixfix, caracteres Unicode e uma interface interativa do Emacs, que pode ajudar o programador a escrever o programa.Agda é assistente de prova.É um sistema interativo para escrever e verificar provas.A Agda é baseada na teoria do tipo intuicionista, um sistema básico para matemática construtiva desenvolvido pelo lógico sueco Per Martin-Löf.Tem muitas semelhanças com outros assistentes de prova baseados em tipos dependentes, como Coq, Epigram, Matita e NuPRL.