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