A question aside: ATS and Computational Type Theory

Google Group
1

Out of curiosity and to a bit help browsing the (so much) wide area of
computation/proof/type theories, I wondered if there is a relation between
ATS and the so called CTT, Computational Type Theory? At least, the average
concept makes me feel this may not be far from the idea of “Applied Type
System” (that’s why I’m asking about it here).

Ex. if I read about CTT (what I feel I should start doing, while not sure),
will this in the while be useful to understand some aspects of ATS?

I wonder about it, since I asked about the location of ATS underlying
theory on the lambda‑cube (in a previous thread) and people told me it
can’t be located on the schema… so if it can be said to be close to
something I’m currently interested in, that would be nice.

I know ATS is very practicability oriented, but I’m still interested in
theoretical aspects too :-p .

By the way, if any one here know noticeable pointers on this topic, feel
free to tell (ex. I wonder if Computational Type Theory and Constructive
Type Theory, both referred to as CTT, are the same or not).

Thanks all, and have a nice day (or night).

2

Computational Type Theory usually refers to the Nuprl work by Constable et
al.

ATS is a layered system (sorts, statics and dynamics). I think it is a lot
much easier
to understand than either CTT or lambda-cube.

If your understand ML, then you should have no difficulty understanding DML:

http://www.ats-lang.org/PAPER/#DMLpaper

If you understand DML, then you should be able to understand ATS:

http://www.ats-lang.org/PAPER/#ATSpaper

ATS does not involve any kind of circularity that is present in
Martin-Loef’s constructive
type theory, which was invented in the first place for the purpose of
setting up a foundation
for mathematics.On Monday, September 29, 2014 5:43:19 PM UTC-4, Yannick Duchêne wrote:

Out of curiosity and to a bit help browsing the (so much) wide area of
computation/proof/type theories, I wondered if there is a relation between
ATS and the so called CTT, Computational Type Theory? At least, the average
concept makes me feel this may not be far from the idea of “Applied Type
System” (that’s why I’m asking about it here).

Ex. if I read about CTT (what I feel I should start doing, while not
sure), will this in the while be useful to understand some aspects of ATS?

I wonder about it, since I asked about the location of ATS underlying
theory on the lambda‑cube (in a previous thread) and people told me it
can’t be located on the schema… so if it can be said to be close to
something I’m currently interested in, that would be nice.

I know ATS is very practicability oriented, but I’m still interested in
theoretical aspects too :-p .

By the way, if any one here know noticeable pointers on this topic, feel
free to tell (ex. I wonder if Computational Type Theory and Constructive
Type Theory, both referred to as CTT, are the same or not).

Thanks all, and have a nice day (or night).