Agda é uma linguagem de programação funcional de tipo dependente. Tem famílias indutivas, ou seja, tipos de dados que dependem de valores, como o tipo de vetores de um determinado comprimento. Ele também tem módulos parametrised, operadores de mixfix, caracteres Unicode, e uma interface Emacs interativa que pode ajudar o programador na escrita do programa. Agda é um assistente de prova. É um sistema interativo para escrever e verificar provas. Agda é baseado na teoria do tipo intuicionista, um sistema fundamental para a matemática construtiva desenvolvida 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.