An extended type system with lambda-typed lambda-expressions (extended version)

Matthias Weber

We present the type system $\mathtt{d}$, an extended type system with lambda-typed lambda-expressions. It is related to type systems originating from the Automath project. $\mathtt…