Teoría de tipos

En matemáticas, lógica y ciencias de la computación, la teoría de tipos es cualquiera de varios sistemas formales que pueden servir como alternativas a la teoría informal de conjuntos, o al estudio de tales formalismos en general. En la teoría de lenguajes de programación, una rama de las ciencias de la computación, la teoría de tipos puede referirse al diseño, análisis y estudio de los sistemas de tipos, aunque algunos científicos de la computación limitan el significado del término al estudio de formalismos abstractos como el cálculo lambda tipado.