Agda est un langage de programmation fonctionnel typé de manière dépendante, développé à l'origine par Ulf Norell à l'Université de technologie de Chalmers avec l'aide de Catarina Coquand, Thorsten Altenkirch et Andrea Vezzosi. Il est basé sur la théorie des types intuitionniste, une forme de théorie des types constructive, et présente de nombreuses similitudes avec Coq, un autre assistant de preuve bien connu. Agda est développé en utilisant une approche interactive de démonstration de théorèmes.
Agda est un langage typé dépendant, ce qui signifie que les types peuvent dépendre des valeurs. Cela permet des spécifications plus précises des programmes et peut conduire à des programmes plus robustes. Il permet également une inférence de type plus puissante, ce qui signifie que le vérificateur de type peut souvent déduire le type d'un programme sans que le programmeur ait à l'annoter explicitement.
Agda possède un vérificateur de terminaison automatique, ce qui signifie qu'il peut détecter si un programme se terminera ou non. C'est une propriété précieuse, car de nombreux programmes qui ne se terminent pas peuvent causer des problèmes lorsqu'ils sont exécutés sur un ordinateur.
Agda est un langage de programmation fonctionnel, ce qui signifie que les programmes sont écrits comme une série d'appels de fonctions. Cela présente un certain nombre d'avantages, notamment celui de rendre les programmes plus faciles à raisonner et plus faciles à paralléliser.
Agda est également un langage à typage statique, ce qui signifie que le type d'un programme est vérifié avant son exécution. Cela permet de détecter les erreurs à un stade précoce, avant qu'elles ne causent des problèmes.
Agda est un projet open source, publié sous la licence publique GNU. La dernière version, 2.5.3, a été publiée le 24 mai 2016.