[burakemir]

I remember a Luca Cardelli paper that explores a language with "type:type" and it contains a sentence roughly expressing: "even if the type system is not satisfying as a logic, it offers interesting possibilities for programming"

[randomNumber7]

I will implement that in my pension if no one else does it in the next 30 years.

[burakemir]

"A Polymorphic λ-calculus with Type:Type"