@hackage / Agda

A dependently typed functional programming language and proof assistant