Agda is a dependently typed functional programming language.