Esta teoría evita la paradoja de Russell creando una jerarquía de tipos, luego asignando cada entidad matemática a un tipo.
Objetos de un tipo dado son creados exclusivamente por objetos de un tipo anterior (aquellos más abajo en la jerarquía), por lo tanto evitando ciclos.
Alonzo Church, inventor del cálculo lambda, desarrolló una lógica de orden superior comúnmente llamada Teoría de Tipos de Church,[2] para evitar la paradoja de Kleen-Rosser que afectaba al cálculo lambda puro original.
La teoría de tipos de Church es una variante del cálculo lambda en el cual las expresiones (también llamadas fórmulas o términos lambda) son clasificadas en tipos, y los tipos de expresiones restringen las maneras en que pueden ser combinadas.
En el cálculo lambda tipado, los tipos juegan un papel similar al de los conjuntos en la teoría de conjuntos.