FYI.
I wrote a paper on the type-theoretical foundation of ATS:
http://www.ats-lang.org/Papers.html#ATSfound
In this paper, programming with theorem-proving (PwTP) is
presented as a programming paradigm where constraint-solving
is internalized.
Cheers,
–Hongwei