Re: Theoretical underpinnings for ATS's type system

2018-03-07 Thread Steinway Wu
Hi Brandon, ATS, as formulated in http://www.ats-lang.org/MYDATA/ATSfoundation.pdf, is proven sound. See Section 3. ATS with theorem-proving is proven sound by proof erasure, in Section 4. As far as I know, the soundness is proven directly, following the traditional approach of Progress + Pre

Theoretical underpinnings for ATS's type system

2018-03-07 Thread Brandon Barker
Hi All, I just realized that I hadn't been seeing many ATS messages recently (really, none for months), so I'm sad that I missed them but excited to see that I have a lot to go through (to start, I may take a half vacation day ...), and will try to get my e-mail sorted out... I'm trying to lea