De Wikipedia, la enciclopedia libre
Saltar a navegación Saltar a búsqueda

En matemáticas , lógica e informática , un sistema de tipos es un sistema formal en el que cada término tiene un "tipo" que define su significado y las operaciones que se pueden realizar en él. La teoría de tipos es el estudio académico de los sistemas de tipos.

Algunas teorías de tipos sirven como alternativas a la teoría de conjuntos como base de las matemáticas . Dos conocidos tales teorías son Alonzo Church 's mecanografiada λ-cálculo y por Martin-Löf ' s teoría de tipos intuicionista .

La teoría de tipos se creó para evitar paradojas en fundamentos anteriores como la teoría de conjuntos ingenua , la lógica formal y los sistemas de reescritura .

La teoría de tipos está estrechamente relacionada y, en algunos casos, se superpone con los sistemas de tipo computacional , que son una característica del lenguaje de programación que se utiliza para reducir errores .

Historia [ editar ]

Entre 1902 y 1908 Bertrand Russell propuso varias "teorías de tipo" en respuesta a su descubrimiento de que la versión de Gottlob Frege de la teoría de conjuntos ingenua estaba afligida por la paradoja de Russell . En 1908, Russell llegó a una teoría de tipos "ramificada" junto con un " axioma de reducibilidad " que figuraban de manera prominente en los Principia Mathematica de Whitehead y Russell .publicado entre 1910 y 1913. Intentaron resolver la paradoja de Russell creando primero una jerarquía de tipos y luego asignando cada entidad matemática concreta (y posiblemente otra) a un tipo. Las entidades de un tipo determinado se construyen exclusivamente a partir de entidades de aquellos tipos que son inferiores en su jerarquía, evitando así que una entidad se asigne a sí misma.

En la década de 1920, Leon Chwistek y Frank P. Ramsey propusieron una teoría de tipos no ramificada, ahora conocida como la "teoría de tipos simples" o teoría de tipos simples , que colapsó la jerarquía de tipos en la teoría ramificada anterior y, como tal, no requirió el axioma de reducibilidad.

El uso común de la "teoría de tipos" es cuando esos tipos se utilizan con un sistema de reescritura de términos . El primer ejemplo más famoso es Alonzo Church 's cálculo lambda simplemente mecanografiado . La teoría de tipos de Church [1] ayudó al sistema formal a evitar la paradoja de Kleene-Rosser que afligía al cálculo lambda original no tipificado. Church demostró que podía servir como base de las matemáticas y se la denominó lógica de orden superior .

Algunas otras teorías de tipo incluyen por Martin-Löf 's teoría de tipos intuicionista , que ha sido la base utilizada en algunas áreas de las matemáticas constructivas . El cálculo de construcciones de Thierry Coquand y sus derivados son la base utilizada por Coq , Lean y otros. El campo es un área de investigación activa, como lo demuestra la teoría de tipos de homotopía .

Conceptos básicos [ editar ]

La presentación contemporánea de los sistemas de tipos en el contexto de la teoría de tipos se ha sistematizado mediante un marco conceptual introducido por Henk Barendregt . [2]

Tipo, término, valor [ editar ]

En un sistema de teoría de tipos, un término se opone a un tipo . Por ejemplo, 4 , 2 + 2 y son términos separados con el tipo nat para números naturales. Tradicionalmente, el término va seguido de dos puntos y su tipo, como 2: nat ; esto significa que el número 2 es de tipo nat . Más allá de esta oposición y sintaxis, poco se puede decir sobre los tipos en esta generalidad, pero a menudo, se interpretan como una especie de colección (no necesariamente conjuntos) de los valores que el término podría evaluar. Es habitual denotar los términos con e y los tipos con τ. La forma en que se dan forma a los términos y tipos depende del sistema de tipos particular y se precisa mediante alguna sintaxis y restricciones adicionales de forma correcta .

Entorno de escritura, asignación de tipo, juicio de tipo [ editar ]

La escritura suele tener lugar en algún contexto o entorno indicado por el símbolo . A menudo, un entorno es una lista de pares . Este par a veces se denomina asignación . El contexto completa la oposición anterior. Juntos forman un juicio denotado .

Reescritura de reglas, conversión, reducción [ editar ]

Las teorías de tipos tienen cálculo explícito y están codificadas en reglas para reescribir términos. Se denominan reglas de conversión o, si la regla solo funciona en una dirección, una regla de reducción . Por ejemplo, y son términos sintácticamente diferentes, pero el primero se reduce al segundo. Esta reducción está escrita . Estas reglas también establecen equivalencias correspondientes entre los términos, escritos .

El término se reduce a . Dado que no se puede reducir más, se llama forma normal . Varios sistemas de cálculo lambda tipificado, incluido el cálculo lambda simplemente tipificado , el sistema F de Jean-Yves Girard y el cálculo de construcciones de Thierry Coquand, se están normalizando fuertemente . En tales sistemas, una verificación de tipo exitosa implica una prueba de terminación del término.

Reglas de tipo [ editar ]

Basándose en los juicios y equivalencias, las reglas de inferencia de tipos se pueden usar para describir cómo un sistema de tipos asigna un tipo a construcciones sintácticas (términos), al igual que en la deducción natural . Para que sean significativas, las reglas de conversión y de tipos suelen estar estrechamente relacionadas, por ejemplo, mediante una propiedad de reducción del sujeto , que podría establecer una parte de la solidez de un sistema de tipos.

Problemas de decisión [ editar ]

Un sistema de tipos está naturalmente asociado con los problemas de decisión de verificación de tipos , tipificabilidad y ocupación de tipos . [3]

Comprobación de tipo [ editar ]

El problema de decisión de la verificación de tipos (abreviado por ) es:

Dado un entorno de tipo , un término y un tipo , decida si al término se le puede asignar el tipo en el entorno de tipo .

La confiabilidad de la verificación de tipos significa que se puede verificar la seguridad de los tipos de cualquier texto de programa dado (código fuente).

Mecanografía [ editar ]

El problema de decisión de la tipificación (abreviado por ) es:

Dado un término , decida si existe un entorno de tipo y un tipo tal que al término se le pueda asignar el tipo en el entorno de tipo .

Una variante de la tipificabilidad es la tipificabilidad wrt. un entorno de tipos (abreviado por ), para el cual un entorno de tipos es parte de la entrada. Si el término dado no contiene referencias externas (como variables de término libre), la tipificabilidad coincide con la tipificabilidad wrt. el entorno de tipo vacío.

La tipificabilidad está estrechamente relacionada con la inferencia de tipos . Mientras que la tipificación (como un problema de decisión) aborda la existencia de un tipo para un término dado, la inferencia de tipos (como un problema de cálculo) requiere que se calcule un tipo real.

Tipo de habitación [ editar ]

El problema de decisión del tipo de habitación (abreviado por ) es:

Dado un entorno de tipos y un tipo , decida si existe un término al que se pueda asignar el tipo en el entorno de tipos .

La paradoja de Girard muestra que la ocupación de tipos está fuertemente relacionada con la consistencia de un sistema de tipos con la correspondencia Curry-Howard. Para ser sólido, tal sistema debe tener tipos deshabitados.

La oposición de términos y tipos también puede verse como una de implementación y especificación . Mediante síntesis de programa (la contraparte computacional de), la habitación de tipo (ver más abajo) se puede usar para construir (todos o parte de) programas a partir de la especificación dada en forma de información de tipo. [4]

Interpretaciones de la teoría de tipos [ editar ]

La teoría de tipos está estrechamente vinculada a muchos campos de investigación activa. Más en particular, la correspondencia Curry-Howard proporciona un isomorfismo profundo entre la lógica intuicionista, el cálculo lambda tipificado y las categorías cerradas cartesianas.

Lógica intuicionista [ editar ]

Además de la visión de los tipos como colección de valores de un término, la teoría de tipos ofrece una segunda interpretación de la oposición de término y tipos. Los tipos pueden verse como proposiciones y los términos como pruebas . En esta forma de leer una tipificación, un tipo de función se ve como una implicación , es decir, como la proposición, que se sigue de .

Teoría de categorías [ editar ]

El lenguaje interno de la categoría cerrada cartesiana es el cálculo lambda simplemente tipeado . Esta vista se puede extender a otros cálculos lambda tipificados. Ciertas categorías cerradas cartesianas, los topoi, se han propuesto como un escenario general para las matemáticas, en lugar de la teoría de conjuntos tradicional.

Diferencia de la teoría de conjuntos [ editar ]

Hay muchas teorías de conjuntos diferentes y muchos sistemas diferentes de teoría de tipos, por lo que lo que sigue son generalizaciones.

  • La teoría de conjuntos se basa en la lógica. Requiere un sistema separado como la lógica de predicados debajo de él. En la teoría de tipos, conceptos como "y" y "o" se pueden codificar como tipos en la propia teoría de tipos.
  • En la teoría de conjuntos, un elemento no está restringido a un conjunto. En la teoría de tipos, los términos (generalmente) pertenecen a un solo tipo. (Cuando se usaría un subconjunto, la teoría de tipos tiende a usar una función de predicado que devuelve verdadero si el término está en el subconjunto y devuelve falso si el valor no lo está. La unión de dos tipos se puede definir como un nuevo tipo llamado suma type , que contiene nuevos términos).
  • La teoría de conjuntos generalmente codifica números como conjuntos. (0 es el conjunto vacío, 1 es un conjunto que contiene el conjunto vacío, etc. Consulte la definición de números naturales de la teoría de conjuntos). La teoría de tipos puede codificar números como funciones usando la codificación Church o, más naturalmente, como tipos inductivos . Los tipos inductivos crean nuevas constantes para la función sucesora y el cero, que se asemejan mucho a los axiomas de Peano .
  • La teoría de tipos tiene una conexión simple con las matemáticas constructivas a través de la interpretación BHK . Puede conectarse con la lógica mediante el isomorfismo de Curry-Howard . Y algunas teorías de tipos están estrechamente relacionadas con la teoría de categorías .

Funciones opcionales [ editar ]

Tipos dependientes [ editar ]

Un tipo dependiente es un tipo que depende de un término u otro tipo. Por tanto, el tipo devuelto por una función puede depender del argumento de la función.

Por ejemplo, una lista de s de longitud 4 puede ser de un tipo diferente a una lista de s de longitud 5. En una teoría de tipos con tipos dependientes, es posible definir una función que toma un parámetro "n" y devuelve una lista. que contiene "n" ceros. Llamar a la función con 4 produciría un término con un tipo diferente que si la función se llamara con 5.

Otro ejemplo es el tipo que consiste en las pruebas de que el término del argumento tiene cierta propiedad, como el término del tipo, por ejemplo, un número natural dado, es primo. Ver correspondencia Curry-Howard .

Los tipos dependientes juegan un papel central en la teoría de tipos intuicionistas y en el diseño de lenguajes de programación funcionales como Idris , ATS , Agda y Epigram .

Tipos de igualdad [ editar ]

Muchos sistemas de teoría de tipos tienen un tipo que representa la igualdad de tipos y términos. Este tipo es diferente de la convertibilidad y, a menudo, se denota igualdad proposicional .

En la teoría de tipos intuicionistas, el tipo de igualdad (también llamado tipo de identidad) se conoce como identidad. Hay un tipo when es un tipo y y son términos de tipo . Un término de tipo se interpreta como un significado que es igual a .

En la práctica, es posible construir un tipo pero no existirá un término de ese tipo. En la teoría de tipos intuicionistas, los nuevos términos de igualdad comienzan con la reflexividad. Si es un término de tipo , entonces existe un término de tipo . Se pueden crear igualdades más complicadas creando un término reflexivo y luego haciendo una reducción en un lado. Entonces, si es un término de tipo , entonces hay un término de tipo y, por reducción, genera un término de tipo . Por tanto, en este sistema, el tipo de igualdad denota que dos valores del mismo tipo son convertibles mediante reducciones.

Tener un tipo de igualdad es importante porque se puede manipular dentro del sistema. Por lo general, no hay juicio para decir que dos términos no son iguales; en cambio, como en la interpretación de Brouwer-Heyting-Kolmogorov , asignamos a , donde es el tipo de fondo que no tiene valores. Existe un término con tipo , pero no uno de tipo .

La teoría de tipos de homotopía se diferencia de la teoría de tipos intuicionista principalmente por su manejo del tipo de igualdad.

Tipos inductivos [ editar ]

Un sistema de teoría de tipos requiere algunos términos y tipos básicos para operar. Algunos sistemas los construyen a partir de funciones que utilizan codificación Church . Otros sistemas tienen tipos inductivos : un conjunto de tipos base y un conjunto de constructores de tipos que generan tipos con propiedades de buen comportamiento. Por ejemplo, se garantiza la terminación de ciertas funciones recursivas llamadas en tipos inductivos.

Los tipos coinductivos son tipos de datos infinitos creados al dar una función que genera los siguientes elementos. Consulte Coinducción y Corecursion .

Inducción-inducción es una característica para declarar un tipo inductivo y una familia de tipos que depende del tipo inductivo.

La recursividad de inducción permite una gama más amplia de tipos con buen comportamiento, lo que permite definir al mismo tiempo el tipo y las funciones recursivas que operan en él.

Tipos de universo [ editar ]

Los tipos se crearon para evitar paradojas, como la paradoja de Russell . Sin embargo, los motivos que conducen a esas paradojas —poder decir cosas sobre todos los tipos— aún existen. Entonces, muchas teorías de tipos tienen un "tipo de universo", que contiene todos los demás tipos (y no a sí mismo).

En los sistemas en los que es posible que desee decir algo sobre los tipos de universo, existe una jerarquía de tipos de universo, cada uno de los cuales contiene el que está debajo en la jerarquía. La jerarquía se define como infinita, pero las declaraciones solo deben referirse a un número finito de niveles del universo.

Los universos de tipos son particularmente complicados en la teoría de tipos. La propuesta inicial de la teoría del tipo intuicionista adolecía de la paradoja de Girard .

Componente computacional [ editar ]

Muchos sistemas de teoría de tipos, como el cálculo lambda de tipo simple , la teoría de tipos intuicionista y el cálculo de construcciones , también son lenguajes de programación. Es decir, se dice que tienen un "componente computacional". El cálculo es la reducción de términos del lenguaje usando reglas de reescritura .

Un sistema de teoría de tipos que tiene un componente computacional de buen comportamiento también tiene una conexión simple con las matemáticas constructivas a través de la interpretación BHK .

Las matemáticas no constructivas en estos sistemas son posibles agregando operadores en continuaciones, como llamar con continuación actual . Sin embargo, estos operadores tienden a romper propiedades deseables como canonicidad y parametricidad .

Teorías de tipo [ editar ]

Mayor [ editar ]

  • Cálculo lambda simplemente mecanografiado que es una lógica de orden superior ;
  • teoría de tipos intuicionistas ;
  • sistema F ;
  • LF se utiliza a menudo para definir otras teorías de tipos;
  • cálculo de construcciones y sus derivadas.

Menor [ editar ]

  • Automath ;
  • Teoría del tipo ST ;
  • UTT (Teoría unificada de tipos dependientes de Luo)
  • algunas formas de lógica combinatoria ;
  • otros definidos en el cubo lambda ;
  • otros bajo el nombre de cálculo lambda mecanografiado ;
  • otros bajo el nombre de pure type system .

Activo [ editar ]

  • Se está investigando la teoría de tipos de homotopía .

Impacto práctico [ editar ]

Lenguajes de programación [ editar ]

Existe una gran superposición e interacción entre los campos de la teoría de tipos y los sistemas de tipos. Los sistemas de tipos son una característica del lenguaje de programación diseñada para identificar errores. Cualquier análisis de programa estático, como los algoritmos de verificación de tipos en la fase de análisis semántico del compilador , tiene una conexión con la teoría de tipos.

Un buen ejemplo es Agda , un lenguaje de programación que utiliza UTT (Teoría unificada de tipos dependientes de Luo) para su sistema de tipos. El lenguaje de programación ML fue desarrollado para manipular las teorías de tipos (ver LCF ) y su propio sistema de tipos fue fuertemente influenciado por ellos.

Fundamentos matemáticos [ editar ]

El primer asistente de pruebas informáticas, llamado Automath , utilizó la teoría de tipos para codificar matemáticas en una computadora. Martin-Löf desarrolló específicamente la teoría de tipos intuicionistas para codificar todas las matemáticas para que sirvan como una nueva base para las matemáticas. Existe una investigación en curso sobre los fundamentos matemáticos utilizando la teoría de tipos de homotopía .

Los matemáticos que trabajaban en la teoría de categorías ya tenían dificultades para trabajar con la base ampliamente aceptada de la teoría de conjuntos de Zermelo-Fraenkel . Esto llevó a propuestas como la Teoría elemental de la categoría de conjuntos de Lawvere (ETCS). [5] La teoría de tipos de homotopía continúa en esta línea utilizando la teoría de tipos. Los investigadores están explorando las conexiones entre los tipos dependientes (especialmente el tipo de identidad) y la topología algebraica (específicamente la homotopía ).

Ayudantes de pruebas [ editar ]

Gran parte de la investigación actual sobre la teoría de tipos está impulsada por verificadores de pruebas , asistentes de prueba interactivos y probadores de teoremas automatizados . La mayoría de estos sistemas utilizan una teoría de tipos como base matemática para codificar pruebas, lo que no es sorprendente, dada la estrecha conexión entre la teoría de tipos y los lenguajes de programación:

  • LF es utilizado por Twelf , a menudo para definir otras teorías de tipos;
  • muchas teorías de tipos que caen bajo la lógica de orden superior son utilizadas por la familia de probadores HOL y PVS ;
  • NuPRL utiliza la teoría de tipos computacionales ;
  • el cálculo de construcciones y sus derivados son utilizados por Coq , Matita y Lean ;
  • UTT (Teoría unificada de tipos dependientes de Luo) es utilizada por Agda, que es tanto un lenguaje de programación como un asistente de pruebas.

Muchas teorías de tipos están respaldadas por LEGO e Isabelle . Isabelle también apoya fundamentos además de las teorías de tipos, como ZFC . Mizar es un ejemplo de un sistema de prueba que solo admite la teoría de conjuntos.

Lingüística [ editar ]

La teoría de tipos también se usa ampliamente en teorías formales de semántica de lenguajes naturales , especialmente en la gramática de Montague y sus descendientes. En particular, las gramáticas categóricas y las gramáticas de pregrupo utilizan ampliamente constructores de tipos para definir los tipos ( sustantivo , verbo , etc.) de palabras.

La construcción más común toma los tipos básicos y para individuos y valores de verdad , respectivamente, y define el conjunto de tipos de forma recursiva de la siguiente manera:

  • si y son tipos, entonces también lo es ;
  • nada excepto los tipos básicos, y lo que se puede construir a partir de ellos mediante la cláusula anterior son tipos.

Un tipo complejo es el tipo de funciones desde entidades de tipo a entidades de tipo . Así, uno tiene tipos como los que se interpretan como elementos del conjunto de funciones desde entidades hasta valores de verdad, es decir, funciones indicadoras de conjuntos de entidades. Una expresión de tipo es una función desde conjuntos de entidades hasta valores de verdad, es decir, una (función indicadora de a) conjunto de conjuntos. Este último tipo se considera estándar como el tipo de cuantificadores del lenguaje natural , como todo el mundo o nadie ( Montague 1973, Barwise y Cooper 1981).

Ciencias sociales [ editar ]

Gregory Bateson introdujo una teoría de tipos lógicos en las ciencias sociales; sus nociones de doble vínculo y niveles lógicos se basan en la teoría de tipos de Russell.

Relación con la teoría de categorías [ editar ]

Aunque la motivación inicial de la teoría de categorías estaba muy alejada del fundacionalismo, los dos campos resultaron tener conexiones profundas. Como escribe John Lane Bell : "De hecho, las categorías pueden considerarse en sí mismas como teorías de tipos de cierto tipo; este solo hecho indica que la teoría de tipos está mucho más relacionada con la teoría de categorías que con la teoría de conjuntos". En resumen, una categoría puede verse como una teoría de tipos al considerar sus objetos como tipos (o géneros), es decir, "En términos generales, una categoría puede considerarse como una teoría de tipos despojada de su sintaxis". A continuación se presentan varios resultados importantes: [6]

  • las categorías cerradas cartesianas corresponden al cálculo λ tipificado ( Lambek , 1970);
  • C-monoides (categorías con productos y exponenciales y un objeto no terminal) corresponden al cálculo λ no tipificado (observado independientemente por Lambek y Dana Scott alrededor de 1980);
  • Las categorías cerradas cartesianas locales corresponden a las teorías de tipo Martin-Löf (Seely, 1984).

La interacción, conocida como lógica categórica , ha sido un tema de investigación activa desde entonces; ver la monografía de Jacobs (1999) por ejemplo.

Ver también [ editar ]

  • Tipo de datos para tipos concretos de datos en programación
  • Teoría del dominio
  • Tipo (teoría del modelo)
  • Sistema de tipos para una discusión más práctica de los sistemas de tipos para lenguajes de programación
  • Fundaciones univalentes

Notas [ editar ]

  1. ^ Iglesia, Alonzo (1940). "Una formulación de la sencilla teoría de tipos". El diario de la lógica simbólica . 5 (2): 56–68. doi : 10.2307 / 2266170 . JSTOR  2266170 .
  2. ^ Barendregt, Henk (1991). "Introducción a los sistemas de tipos generalizados". Revista de programación funcional . 1 (2): 125-154. doi : 10.1017 / s0956796800020025 . hdl : 2066/17240 . ISSN 0956-7968 . 
  3. ^ Henk Barendregt; Wil Dekkers; Richard Statman (20 de junio de 2013). Cálculo lambda con tipos . Prensa de la Universidad de Cambridge. pag. 66. ISBN 978-0-521-76614-2.
  4. ^ Heineman, George T .; Bessai, Jan; Düdder, Boris; Rehof, Jakob (2016). "Un camino largo y tortuoso hacia la síntesis modular". Aprovechamiento de las aplicaciones de métodos formales, verificación y validación: técnicas fundamentales . ISoLA 2016. Apuntes de la cátedra en Informática. 9952 . Saltador. págs. 303–317. doi : 10.1007 / 978-3-319-47166-2_21 .
  5. ^ ETCS en nLab
  6. ^ Bell, John L. (2012). "Tipos, conjuntos y categorías" (PDF) . En Kanamory, Akihiro (ed.). Conjuntos y ampliaciones en el siglo XX . Manual de Historia de la Lógica. 6 . Elsevier. ISBN  978-0-08-093066-4.

Referencias [ editar ]

  • Granjero, William M. (2008). "Las siete virtudes de la teoría de tipos simples". Revista de lógica aplicada . 6 (3): 267–286. doi : 10.1016 / j.jal.2007.11.001 .

Lectura adicional [ editar ]

  • Aarts, C .; Backhouse, R .; Hoogendijk, P .; Voermans, E .; van der Woude, J. (diciembre de 1992). "Una teoría relacional de tipos de datos" . Technische Universiteit Eindhoven.
  • Andrews B., Peter (2002). Una introducción a la lógica matemática y la teoría de tipos: a la verdad a través de la prueba (2ª ed.). Kluwer. ISBN 978-1-4020-0763-7.
  • Jacobs, Bart (1999). Lógica categórica y teoría de tipos . Estudios de Lógica y Fundamentos de las Matemáticas. 141 . Elsevier. ISBN 978-0-444-50170-7.Cubre la teoría de tipos en profundidad, incluidas las extensiones de tipos polimórficos y dependientes. Da semántica categórica .
  • Cardelli, Luca (1996). "Type Systems" . En Tucker, Allen B. (ed.). El Manual de Ingeniería y Ciencias de la Computación . Prensa CRC. págs. 2208–36. ISBN 9780849329098.
  • Collins, Jordan E. (2012). Una historia de la teoría de tipos: desarrollos posteriores a la segunda edición de 'Principia Mathematica'. Publicaciones académicas de Lambert. hdl : 11375/12315 . ISBN 978-3-8473-2963-3. Proporciona un estudio histórico de los desarrollos de la teoría de tipos con un enfoque en el declive de la teoría como base de las matemáticas durante las cuatro décadas posteriores a la publicación de la segunda edición de 'Principia Mathematica'.
  • Constable, Robert L. (2012) [2002]. "Teoría ingenua de tipos computacionales" (PDF) . En Schwichtenberg, H .; Steinbruggen, R. (eds.). Prueba y confiabilidad del sistema . Serie de Ciencias de la OTAN II. 62 . Saltador. págs. 213-259. ISBN 9789401004138.Concebido como una contraparte tipo teoría de Paul Halmos 's (1960) Naïve teoría de conjuntos
  • Coquand, Thierry (2018) [2006]. "Teoría de tipos" . Enciclopedia de Filosofía de Stanford .
  • Thompson, Simon (1991). Teoría de tipos y programación funcional . Addison – Wesley. ISBN 0-201-41667-0.
  • Hindley, J. Roger (2008) [1995]. Teoría básica de tipos simples . Prensa de la Universidad de Cambridge. ISBN 978-0-521-05422-5.Una buena introducción a la teoría de tipos simple para científicos informáticos; Sin embargo, el sistema descrito no es exactamente el STT de Church. Reseña del libro
  • Kamareddine, Fairouz D .; Laan, Twan; Nederpelt, Rob P. (2004). Una perspectiva moderna de la teoría de tipos: desde sus orígenes hasta la actualidad . Saltador. ISBN 1-4020-2334-0.
  • Ferreirós, José; Domínguez, José Ferreirós (2007). "X. Lógica y teoría de tipos en el período de entreguerras". Laberinto del pensamiento: una historia de la teoría de conjuntos y su papel en las matemáticas modernas (2ª ed.). Saltador. ISBN 978-3-7643-8349-7.
  • Laan, TDL (1997). La evolución de la teoría de tipos en lógica y matemáticas (PDF) (PhD). Universidad Tecnológica de Eindhoven. doi : 10.6100 / IR498552 . ISBN 90-386-0531-5.

Enlaces externos [ editar ]

  • Robert L. Constable (ed.). "Teoría de tipos computacionales" . Scholarpedia .
  • The TYPES Forum : foro de correo electrónico moderado que se centra en la teoría de tipos en informática, que funciona desde 1987.
  • El libro Nuprl : " Introducción a la teoría de tipos " .
  • Tipos Notas de conferencias del proyecto de las escuelas de verano 2005-2008
    • La escuela de verano de 2005 tiene conferencias introductorias
  • Teoría de tipos en nLab , que tiene artículos sobre muchos temas relacionados.
  • Escuela de Verano de Lenguajes de Programación de Oregon , muchas conferencias y algunas notas.
    • Verano de 2015 Tipos, lógica, semántica y verificación