Effective ATS: An array-based stack implementation

Google Group
1

I wrote up an example showing how C code can be directly combined with ATS
code
to circumvent (part of) the need for proofs and proof manipulation:

http://www.ats-lang.org/EXAMPLE/EFFECTIVATS/stack-array/

Cheers!