Blaisorblade
commented
10 years ago Maybe they only refer to the property that Sage has a common syntactic entity for terms and types as being similar to PTS (?).
The home page suggests (to me) you are likely right:
In addition to featuring these predicates upon types, Sage merges the syntactic categories of types and terms, in the spirit of Pure Type Systems, to express dependent types such as that of the infamous printf function.
Their paper seems more specific — they seem to use in fact λ*:
First-Class Types. Sage eschews the term/type/kind hierarchy common in type systems and instead unifies the syntactic categories of terms, types, and kinds. This unification is inspired by prior work on pure type systems (Cardelli 1986; Barendregt 1991; Roorda 2000). As an example, the term 3 has type the type Int. Since types are integrated into the term language, Int is also a term, and hence has a type, namely the type “”, which is the “type of types”. Thus, in Sage, types are simply terms of type . The type * is also a term, and itself has type *.1
1 Although * : * makes for inconsistent logics (Girard 1972), it does not detract from the soundness or usefulness of a type system for a programming language (Cardelli 1986).
Just stumbled upon this: https://sage.soe.ucsc.edu/
In the tutorial they claim that Sage supports Pure Type Systems. I'm not sure whether this is actually true, since they don't show how a PTS specification can be expressed in Sage. Maybe they only refer to the property that Sage has a common syntactic entity for terms and types as being similar to PTS (?).