Agda ist eine abhängig typisierte funktionale Programmiersprache, die ursprünglich von Ulf Norell an der Chalmers University of Technology mit Hilfe von Catarina Coquand, Thorsten Altenkirch und Andrea Vezzosi entwickelt wurde. Sie basiert auf der intuitionistischen Typentheorie, einer Form der konstruktiven Typentheorie, und hat viele Ähnlichkeiten mit Coq, einem anderen bekannten Beweisassistenten. Agda wird mit Hilfe eines interaktiven Theorem-Proving-Ansatzes entwickelt.
Agda ist eine abhängige typisierte Sprache, was bedeutet, dass Typen von Werten abhängen können. Dies ermöglicht eine präzisere Spezifikation von Programmen und kann zu robusteren Programmen führen. Das bedeutet, dass der Typprüfer oft den Typ eines Programms ableiten kann, ohne dass der Programmierer es explizit annotieren muss.
Die Agda verfügt über eine automatische Abbruchprüfung, d.h. sie kann erkennen, ob ein Programm abbricht oder nicht. Dies ist eine wertvolle Eigenschaft, da viele Programme, die nicht beendet werden, Probleme verursachen können, wenn sie auf einem Computer ausgeführt werden.
Agda ist eine funktionale Programmiersprache, was bedeutet, dass Programme als eine Reihe von Funktionsaufrufen geschrieben werden. Dies hat eine Reihe von Vorteilen, wie z.B. dass Programme leichter zu verstehen sind und leichter parallelisiert werden können.
Agda ist auch eine statisch typisierte Sprache, was bedeutet, dass der Typ eines Programms vor der Ausführung überprüft wird. Dadurch können Fehler frühzeitig erkannt werden, bevor sie Probleme verursachen.
Agda ist ein Open-Source-Projekt, das unter der GNU Public License veröffentlicht wird. Die neueste Version, 2.5.3, wurde am 24. Mai 2016 veröffentlicht.