Look up
Charts
Prints
dependently typed programming language
Agda
ATS
Cayenne
Epigram
F*
Idris
Rocq