Agda
Dependently typed proof assistant and programming language — used for formalising mathematics and verifying software correctness.
static
compiled
since 2007
functionaldependent-types
Agda is both a proof assistant and a programming language — proofs are programs and programs are proofs. It is used in academic research to formalise mathematics (the HoTT book was typeset using Agda proofs) and to verify correctness of algorithms and protocols. Its interactive editor mode in Emacs allows filling in proof holes incrementally.