Types versus kinds and sorts In the context of logic, especially Higher‑Order‑Logic and Calculus‑of‑Construction, what is a kind and how does it relates to and differs from a type?
My raw guess if that a kind is the higher level type of a type. Is that it? If not, so what's a kind? If yes, is this as simple as it looks or are there more elaborated things to know about the relation between both?
Update: same question with sorts (or may be they are synonymous?).
 A: Will try to answer my own question (to be updated a future day).
Words in ML programmer's guide to ATS (cs.likai.org), suggests a sort is indeed a category above types:

Type definition assigns a static identifier
  to a static expression with the sort "type"
  […] The only difference is that typedef ensures
  that t will end up having the "type" sort, and
  stadef doesn't particularly care.

Since ATS is entirely based on an advanced type theory (close to CoC) and the author of the page is a CS professor, I believe the wording used in this document is meaningful.
Then later he adds more:

A type is one of the many sorts that a static
  expression or static identifier can be. Other
  sorts are:
  
  
*
  
*Ground sorts: int, bool, char, addr. They 
  form the basis of dependent type indices.
  
*View, which are linear (in the sense of linear
  logic) propositions.
  
*Prop, which are classical propositions.
  
*Viewtype, which are linear types. It can be
  seen as a type combined with a view.
  

After this, I guess it's either an higher object level type (object type of an object type), or a meta‑language level type of an object level term. Discriminating between both, may be for a future day.
Update #1:
From the same source, later:

Notice that t@ype is a subsort of viewt@ype

As what's referred to as viewt@ype is at the object language level, sort is probably at object level too and is an object level category, above type, after the previous notes.
Confirmations from other sources would be nice. And this still do not answer the question about kinds.
Update #2:
During a talk in a mailing list, I get an answer, where there's a part relevant for this matter:

  
*
  
*Applied Type System enforces a separation between
  the term, type, kind (sort) levels (in ATS2, there
  are only three such levels).
  

This suggests kind and sort are synonymous.
A: Yes, your guess about kinds is correct. According to Types and Programming Languages, kinds are "the types of types". 
From the same source:

[...] we introduce a system of kinds that classify type expressions
  according to their arity, just as arrow types tell us about the arities of terms. Kinds, then, are “the types of types.” In essence, the system of kinds is a copy
  of the simply typed lambda-calculus, “one level up.”

