ATS

ATS is a multi-paradigm, general-purpose, high-level functional programming language designed by Hongwei Xi as a dialect of ML. It combines theorem proving with practical programming through advanced type systems.