Herramientas y conceptos modernos de programación funcional.
Mónadas, funtores, funtores aplicativos, F-álgebras, catamorfismos, zippers, derivadas de tipos, functional reactive programming, arrows, lenses.
¿Cómo se compila un lenguaje funcional?
Desugaring, lambda lifting, supercombinadores, concepto de whnf, reescritura de grafos, máquinas abstractas.
Continuaciones.
Call/cc, CPS-conversion, continuaciones delimitadas, implementación de estructuras de control con call/cc: excepciones, backtracking, iteradores.
Extensiones a sistemas de tipos.
Typeclasses, tipos existenciales, GADTs, rank-N types, type families, tipos dependientes.
Usos interesantes de sistemas de tipos.
Phantom types, QuickCheck, garantía estática de invariantes no triviales.
Estructuras de datos funcionales.
Difference lists, random-access lists, binomial heaps, treaps, finger trees.
Asistentes de demostración.
Correspondencia entre proposiciones y tipos, tipos dependientes como logical frameworks, ejemplos interactivos con asistententes de demostración puntuales (Coq, Agda, otros).
Parsers combinatorios / monádicos.
Homotopy type theory.
Un desarrollo reciente que propone fundamentos para la matemática basados en teoría de tipos.
Ver http://homotopytypetheory.org/book/
Algunos resultados clásicos del cálculo lambda.
Combinadores de punto fijo, representación de tipos de datos algebraicos con lambda-términos, traducción a lógica combinatoria, estrategias de evaluación
call-by-value vs. call-by-name. Otros resultados teóricos.