Agda je závislostně typovaný funkcionální programovací jazyk, který původně vyvinul Ulf Norell na Chalmers University of Technology s pomocí Catariny Coquand, Thorstena Altenkircha a Andrey Vezzosi. Je založen na intuicionistické teorii typů, což je forma konstruktivní teorie typů, a má mnoho podobností s Coqem, dalším známým pomocníkem pro dokazování. Agda je vyvinuta s využitím interaktivního přístupu k dokazování tvrzení.
Agda je závislostně typovaný jazyk, což znamená, že typy mohou záviset na hodnotách. To umožňuje přesnější specifikace programů a může vést k robustnějším programům. Umožňuje také výkonnější odvozování typů, což znamená, že kontrolor typů může často odvodit typ programu, aniž by jej programátor musel explicitně anotovat.
Agda má automatickou kontrolu ukončení, což znamená, že dokáže zjistit, zda se program ukončí, nebo ne. To je cenná vlastnost, protože mnoho programů, které se neukončí, může při spuštění na počítači způsobit problémy.
Agda je funkcionální programovací jazyk, což znamená, že programy jsou psány jako série volání funkcí. To má řadu výhod, například se programy snáze odůvodňují a snadněji paralelizují.
Agda je také staticky typovaný jazyk, což znamená, že typ programu se kontroluje před jeho spuštěním. Díky tomu lze včas zachytit chyby dříve, než způsobí problémy.
Agda je projekt s otevřeným zdrojovým kódem vydaný pod licencí GNU Public License. Nejnovější verze 2.5.3 byla vydána 24. května 2016.