type theory (dependent, extensional, intensional type theory)
In modern logic, we understand that every variable should have a type, or domain of discourse. Untyped logic may be seen as simply a special case, in which there is only a single unique type. (Thus, untyped logic has one type, not no type.)
It is possible to build foundations of mathematics on type theory alone.
dependent type, dependent type theory, Martin-Löf dependent type theory
homotopy type, homotopy type theory