ATS: A Language That Combines Programming with Theorem Proving. - Sa Cui; Kevin Donnelly; Hongwei Xi 001 (FroCoS, 2005)