Mis sugerencias personales son las siguientes:
- Teoría de tipos -> Teoría de tipos y pruebas formales: una introducción: Rob Nederpelt, Herman Geuvers: 9781107036505: Amazon.com: Libros
- El libro mencionado anteriormente presenta varios tipos de Cálculos de Lambada sin tipo y tipificados antes de exponer finalmente el Cálculo de construcciones (Sin tipo -> Tipo de primer orden -> Tipo de segundo orden -> Tipo dependiente -> Cubo Lambda -> Calc. De construcciones). Una cosa buena es que este libro cubre los juicios. También me gustaría decir que los Ejercicios son realmente buenos. Por ejemplo, uno de los ejercicios del Capítulo 3 (para [math] \ lambda 2 [/ math]) le pide a uno que construya un Tipo de árbol y que demuestre cosas al respecto. Lo he usado como primer libro en Type Theory & Lambda Calculus, y es realmente bueno. Sin embargo, tenga en cuenta que es un libro teórico y supone madurez matemática y buena capacidad para usar la inducción y la abstracción.
- Tipos y lenguajes de programación -> Tipos y lenguajes de programación (MIT Press): Benjamin C. Pierce: 9780262162098: Amazon.com: Libros
- Este libro es el libro _classic_ y utiliza SML para la exposición de conceptos. Introduce semántica formal, tipos, tipos inductivos, tipos co-inductivos, inferencia de tipos, la cantidad requerida de cálculo Lambda. Es una buena combinación de teoría y práctica, y tiene una buena cantidad de pruebas. Sin embargo, hay una exposición de código en todo momento para complementar la Teoría. Yo diría que es uno de los mejores libros que he leído sobre TCS, junto con Automata, Idiomas y Computación y Algoritmos CLRS de Ullman.
- De acuerdo, una vez que se hayan completado los 2 anteriores, estará en un lugar con una combinación suficientemente sólida de Fundamentos teóricos y exposiciones de Programación funcional de conceptos básicos. Entonces, esta sección está sesgada en función de los intereses, pero dado que tengo una mentalidad teórica, estos son los que he estado usando:
- HoTT (Teoría del tipo de homotopía) -> Teoría del tipo de homotopía: Fundamentos univalentes de las matemáticas: Programa de fundamentos univalentes: Amazon.com: Libros
- Este libro es básicamente un libro bastante accesible, pero riguroso y profundo (con Ejercicios) que introduce la extensión de la Teoría de tipo intuitiva usando la Teoría de la homotopía. Sorprendentemente, esta es una base alternativa de Matemáticas a la teoría de conjuntos ZFK. Es intelectualmente rico, estimulante e introduce también la teoría de la categoría y la teoría de la homotopía necesarias. Un buen libro de texto.
- Teoría de la prueba -> Teoría de la prueba: Cálculos secuenciales y formalismos relacionados (Matemática discreta y sus aplicaciones): Katalin Bimbo: 9781466564664: Amazon.com: Libros
- Un excelente libro, presenta los conceptos básicos de la teoría de la prueba y sus interacciones con la lógica combinatoria.
- Temas avanzados en tipos y lenguajes de programación -> Temas avanzados en tipos y lenguajes de programación (MIT Press): 9780262162289: Computer Science Books @ Amazon.com
- Como su nombre lo indica, este libro es una continuación del libro anterior de Pierce e introduce Conceptos avanzados en tipos y lenguajes de programación, incluidas las relaciones entre asignación de memoria y tipos dependientes de seguridad de tipo.
- Estructuras de datos funcionales -> Estructuras de datos puramente funcionales: Chris Okasaki: 9780521663502: Amazon.com: Libros
- Este libro presenta la implementación de estructuras de datos funcionales en SML / Haskell, y es un buen puente entre los algoritmos tradicionales y las estructuras de datos implementadas con respecto a los fundamentos teóricos de tipo, como la inmutabilidad y la apatridia.
- Buena suerte en la búsqueda!
