{{language|Agda
|site=http://wiki.portal.chalmers.se/agda/pmwiki.php}}{{implementation|Agda}}{{stub}}
Agda is a dependently typed functional programming language.