Agda es un lenguaje de programación funcional de tipo dependiente.Tiene familias inductivas, es decir, tipos de datos que dependen de valores, como el tipo de vectores de una longitud dada.También tiene módulos parametrizados, operadores mixfix, caracteres Unicode y una interfaz interactiva Emacs que puede ayudar al programador a escribir el programa.Agda es una asistente de pruebas.Es un sistema interactivo para escribir y verificar pruebas.Agda se basa en la teoría de tipo intuicionista, un sistema fundamental para las matemáticas constructivas desarrollado por el lógico sueco Per Martin-Löf.Tiene muchas similitudes con otros asistentes de prueba basados ​​en tipos dependientes, como Coq, Epigram, Matita y NuPRL.