Agda es un lenguaje de programación funcional dependiente tipado desarrollado originalmente por Ulf Norell en la Universidad Tecnológica de Chalmers con la ayuda de Catarina Coquand, Thorsten Altenkirch y Andrea Vezzosi. Se basa en la teoría de tipos intuicionista, una forma de teoría de tipos constructiva, y tiene muchas similitudes con Coq, otro conocido asistente de pruebas. Agda se desarrolla utilizando un enfoque de demostración interactiva de teoremas.
Agda es un lenguaje de tipado dependiente, lo que significa que los tipos pueden depender de los valores. Esto permite especificaciones más precisas de los programas y puede conducir a programas más robustos. También permite una inferencia de tipos más potente, lo que significa que el comprobador de tipos a menudo puede inferir el tipo de un programa sin que el programador tenga que anotarlo explícitamente.
Agda tiene un comprobador automático de terminación, lo que significa que puede detectar si un programa terminará o no. Esta es una propiedad valiosa, ya que muchos programas que no terminan pueden causar problemas cuando se ejecutan en un ordenador.
Agda es un lenguaje de programación funcional, lo que significa que los programas se escriben como una serie de llamadas a funciones. Esto tiene una serie de ventajas, como hacer que los programas sean más fáciles de razonar y más fáciles de paralelizar.
Agda es también un lenguaje de tipado estático, lo que significa que el tipo de un programa se comprueba antes de que se ejecute. Esto puede detectar errores antes de que causen problemas.
Agda es un proyecto de código abierto, publicado bajo la Licencia Pública GNU. La última versión, 2.5.3, se publicó el 24 de mayo de 2016.