Grupo de lectura sobre cálculo-λ, reescritura, lógica, teoría de tipos, categorías, y todo lo demás.
Viernes 14:00-16:00 — Sala ex-infoteca. Pabellón I, Ciudad Universitaria Google Meet.
Viernes 16 de julio de 2021 CH§6 Correspondencia entre proposiciones y tipos para lógica clásica. Lambda-mu y operadores de control. Expositor: Pablo Barenbaum.
Viernes 25 de junio de 2021 CH§4,5 Correspondencia entre proposiciones y tipos. Sistemas à la Hilbert. Expositor: Pablo Barenbaum.
Viernes 18 de junio de 2021 Demostración de SN del cálculo-λ simplemente tipado basada en la interpretación de los términos con funcionales crecientes (de Vrijer, 1987). [Notas] Expositor: Pablo Barenbaum.
Viernes 11 de junio de 2021 CH§3 Propiedades básicas del cálculo-λ simplemente tipado, subject reduction, demostración de WN por grados decrecientes de radicales. [Notas] [Demostración de WN] Expositor: Pablo Barenbaum.
Viernes 4 de junio de 2021 CH§2 Modelos de Kripke. Teorema de Glivenko. [Notas] Expositor: Pablo Barenbaum.
Viernes 28 de mayo de 2021 CH§2 Semántica algebraica, álgebras de Heyting. [Notas] Expositor: Pablo Barenbaum.
Viernes 14 de mayo de 2021 CH§2 Deducción natural para lógica intuicionista. [Notas] Expositor: Pablo Barenbaum.
Viernes 30 de abril de 2021 HB§10. Técnica Böhm out. Separabilidad y teorema de Böhm. [Notas] Expositor: Pablo Barenbaum.
Viernes 23 de abril de 2021 HB§8,10. Solvability y árboles de Böhm. [Notas] Expositor: Pablo Barenbaum.
Viernes 16 de abril de 2021 CH§1.5. Normalización de la estrategia de reducción leftmost. [Notas] Expositor: Pablo Barenbaum.
Viernes 18 de diciembre de 2020 HB§6. Cálculo-λ clásico. Segundo teorema del punto fijo. Teorema de indecidibilidad "tipo Rice". [Notas] Expositor: Pablo Barenbaum.
Viernes 11 de diciembre de 2020 HB§6. Cálculo-λ clásico: codificación de datos en el cálculo-λ sin tipos (booleanos, pares, números, etc.). Funciones λ-definibles. Todas las funciones recursivas son λ-definibles. Teorema del punto fijo simple y múltiple. [Notas] Expositor: Pablo Barenbaum.
Viernes 4 de diciembre de 2020 HB§4. Teorías. Teorías sensatas y semi-sensatas. Equivalencia de principios de extensionalidad. Modelos de términos. [Notas] Expositor: Pablo Barenbaum.
Viernes 27 de noviembre de 2020 Repaso de reescritura abstracta (principios básicos de confluencia y normalización). Conversión y reducción en el cálculo-λ. [Notas] Expositor: Pablo Barenbaum.
Viernes 13 de noviembre de 2020 HB§3. Reducción en el cálculo-lambda: propiedad de Church–Rosser. Expositor: Guillermo Tochi.
Viernes 6 de noviembre de 2020 HB§2. Conversión en el cálculo-lambda. Expositor: Guillermo Tochi.
Viernes 17 de julio de 2020 Introducción a makam parte IV. Implementación (en conjunto) de Featherweight Go, sección 3 del paper. Código. Expositor: Teo Freund.
Viernes 3 de julio de 2020 Introducción a makam parte III. Implementación (en conjunto) de Featherweight Go, sección 3 del paper. Código. Expositor: Teo Freund.
Viernes 26 de junio de 2020 Introducción a makam parte II. Implementación (en conjunto) de Featherweight Go, sección 3 del paper. Código. Expositor: Teo Freund.
Viernes 19 de junio de 2020 Introducción a makam parte I. Implementación (en conjunto) de Featherweight Go, sección 3 del paper. Código. Expositor: Teo Freund.
Viernes 12 de junio de 2020 Discusión: Featherweight Go, Griesemer et al. Expositor: Teo Freund.
Viernes 29 de mayo de 2020 The duality of computation, Curien, Herbelin. Classical Proofs as Programs, M. Parigot. Expositor: Teo Freund.
Viernes 22 de mayo de 2020 lambdamu-calculus: an Algorithmic Interpretation of Classical Natural Deduction, M. Parigot. Expositor: Teo Freund.
Viernes 15 de mayo de 2020 Discusión: A Quick Look at Impredicativity, Serrano et al. Expositor: Teo Freund.
Viernes 8 de mayo de 2020 UF§3. Singletons, subsingletons and sets. Univalent excluded middle. The types of magmas and monoids. Expositor: Teo Freund.
Viernes 24 de abril de 2020 UF§2. Axiomas de Peano. Expositor: Teo Freund.
Viernes 17 de abril de 2020 UF§2. Producto dependiente, tipo identidad (definicíon y algunas propiedades). Expositor: Teo Freund.
Jueves 9 de abril de 2020 UF§2. Universos, tipo vacío, tipo unitario, naturales, sumas, principios de inducción. Expositor: Teo Freund.
Jueves 2 de abril de 2020 Implementación de intérpretes: store-passing, continuation-passing, scoping dinámico vs. léxico, call-by-value/name/need. Expositor: Pablo Barenbaum.
Jueves 26 de marzo de 2020 Presentación del trabajo Invertible Syntax Descriptions: Unifying Parsing and Pretty Printing de Tillmann Rendel y Klaus Ostermann. Expositor: Teo Freund.
Martes 10 de diciembre de 2019 Algunos avances en el diseño de un cálculo-lambda con características de programación lógica. Expositor: Pablo Barenbaum.
Martes 3 de diciembre de 2019 Programación de un SAT solver en Agda y demostración de correctitud. Expositor: Dylan Fridman.
Martes 26 de noviembre de 2019 Continuation-passing style: traducción CPS; simulación de call-by-value en call-by-name a través de la traducción; efecto de la traducción en los tipos (doble negación); operadores de control: abort, call/cc, continuaciones delimitadas. [pdf] Expositor: Pablo Barenbaum.
Martes 12 de noviembre de 2019 Estrategias de evaluación y useful sharing en el cálculo-λ. Expositor: Maico Leberle.
Martes 5 de noviembre de 2019 PLFA§2 Formalización del cálculo-λ simplemente tipado usando índices de de Bruijn y tipado intrínseco: evaluación y propiedades. Expositor: Brian Bokser.
Martes 29 de octubre de 2019 PLFA§2 Formalización del cálculo-λ simplemente tipado usando índices de de Bruijn y tipado intrínseco: sistema de tipos. Expositor: Brian Bokser.
Martes 22 de octubre de 2019 PLFA§2 Formalización del cálculo-λ simplemente tipado: preservación de tipos (continuación), progreso. Expositor: Pablo Barenbaum.
Martes 15 de octubre de 2019 PLFA§2 Formalización del cálculo-λ simplemente tipado: reglas de tipado, preservación de tipos. Expositor: Pablo Barenbaum.
Martes 8 de octubre de 2019 PLFA§2 Formalización del cálculo-λ simplemente tipado: sintaxis (representación con nombres explícitos). Reglas de evaluación small-step (call-by-value). Expositor: Pablo Barenbaum.
Martes 24 de septiembre de 2019 PLFA§1 Predicados decidibles, listas. Expositor: Pablo Barenbaum.
Martes 17 de septiembre de 2019 PLFA§1 Cuantificadores (funciones y pares dependientes). Expositor: Pablo Barenbaum.
Martes 10 de septiembre de 2019 PLFA§1 Equivalencia entre varios principios de razonamiento clásicos. Demostración de algunos isomorfismos de tipos. Expositor: Pablo Barenbaum.
Martes 3 de septiembre de 2019 PLFA§1 Proposiciones definidas inductivamente. Isomorfismos de tipos. Expositor: Pablo Barenbaum.
Martes 27 de agosto de 2019 PLFA§1 Recursión e inducción sobre números naturales (continuación). Expositor: Pablo Barenbaum.
Martes 20 de agosto de 2019 PLFA§1 Recursión e inducción sobre números naturales. Expositor: Pablo Barenbaum.
Martes 13 de agosto de 2019 PLFA§1. Introducción a la teoría de tipos de Martin-Löf y lógica en Agda. Expositor: Pablo Barenbaum.
Jueves 18 de julio de 2019. Introducción a Liquid Haskell. Expositor: Brian Bokser.
Jueves 11 de julio de 2019. HPT§2. Introducción a la aritmética de primer orden. Teorías débiles sin principio de inducción (Q, R). Jerarquía aritmética. Expositor: Pablo Barenbaum.
Jueves 13 de junio de 2019. HPT§1.2. Teorema de definibilidad de Beth. Cut elimination en cálculo de secuentes para lógica de primer orden. Expositor: Pablo Barenbaum.
Jueves 6 de junio de 2019. HPT§1.2. Teorema de Herbrand. Teorema de interpolación de Craig. Expositor: Pablo Barenbaum.
Jueves 30 de mayo de 2019. HPT§1.2. Completitud del cálculo de secuentes para lógica de primer orden. Expositor: Teo Freund.
Jueves 16 de mayo de 2019. HPT§1.2. Cálculo de secuentes para lógica de primer orden. Expositor: Teo Freund.
Jueves 9 de mayo de 2019. HPT§1.1. Cálculo de secuentes para lógica proposicional. Refutación por resolución proposicional. [pdf] Expositor: Pablo Barenbaum.
Miércoles 24 de abril de 2019. HPT§1.1. Repaso de lógica proposicional básica. Semántica. Sistema de demostración à la Hilbert. Compacidad, correctitud y completitud. [pdf]. Expositor: Pablo Barenbaum.
Martes 27 de noviembre de 2018. CMS§7. Introducción a la movilidad, reglas de transición para el π-cálculo. Expositor: Pablo Barenbaum.
Martes 20 de noviembre de 2018. CMS§6. Bisimulación y bisimilaridad débil. Propiedades algebraicas de la bisimilaridad débil. Bisimulación débil up to bisimilaridad fuerte. Teorema de unicidad de solución a sistemas de ecuaciones, módulo bisimilaridad débil. Expositor: Pablo Barenbaum.
Martes 30 de octubre de 2018. CMS§5. Ejemplos de bisimilaridad fuerte. Bisimulación fuerte up to equivalencia estructural. Propiedades algebraicas de la bisimilaridad fuerte. Expositor: Pablo Barenbaum.
Martes 23 de octubre de 2018. CMS§5. Equivalencia estructural. Reglas de transición (etiquetadas) y de reacción (interna). Equivalencia entre las dos formulaciones. Expositor: Pablo Barenbaum.
Martes 16 de octubre de 2018. CMS§3–4. Bisimulación fuerte. Bisimilaridad. Expresiones de procesos concurrentes. Expositor: Teo Freund.
Martes 9 de octubre de 2018. CMS§2. Autómatas finitos y conjuntos regulares. Regla de Arden. Descripción de sistemas usando LTSs (labeled transition systems). Simulación. Expositor: Teo Freund.
Martes 2 de octubre de 2018. Presentación de un cálculo de procesos basado en deducción natural clásica. Expositor: Pablo Barenbaum.
Martes 18 de septiembre de 2018. Bootstrapping en compiladores de Lisp. Trabajo en progreso sobre un port de SBCL para PowerPC de 64-bits. Expositor: Brian Bokser.
Martes 11 de septiembre de 2018. SPJ§14. Extensión de la técnica de supercombinadores para definiciones recursivas. Expositor: Gonzalo Ciruelos.
Martes 28 de agosto de 2018. SPJ§13. Compilación de programas funcionales usando supercombinadores y lambda-lifting. Expositor: Gonzalo Ciruelos.
Martes 21 de agosto de 2018. Bir87, Gib95. Homomorfismos de listas. Primer teorema de homomorfismo: todo homomorfismo de listas se escribe como un map seguido de un reduce. Segundo y tercer teorema de homomorfismo: los homomorfismos de listas son precisamente las funciones que se pueden escribir simultáneamente usando foldr y foldl. Expositor: Gonzalo Ciruelos.
Jueves 5 de julio de 2018. Discusión: definición de un cálculo-λ tipado con polimorfismo de usos. Expositor: Pablo Barenbaum.
Jueves 28 de junio de 2018. Defensa de tesis de licenciatura de Gonzalo Ciruelos: Factorización de derivaciones a través de tipos intersección.
Jueves 14 de junio de 2018. SPJ§12. Reducción de grafos para evaluación de λ-términos. Expositor: Andrés Radunsky.
Jueves 7 de junio de 2018. SPJ§10–11. Representación de grafos de términos. Representaciones boxed y unboxed. Noción de weak head normal form. Técnica de pointer reversal para recorrer la "columna vertebral" de un término sin almacenamiento auxiliar. Expositor: Andrés Radunsky.
Jueves 31 de mayo de 2018. Definición de System F. Codificación de tipos inductivos en System F. Terminación de System F con la técnica de candidatos de reducibilidad de Girard [PT, capítulos 11 y 14]. Expositor: Pablo Barenbaum.
Jueves 24 de mayo de 2018. SPJ§9. Algoritmo de inferencia de tipos con tipado polimórfico. Algoritmo de unificación de Robinson. Expositor: Gonzalo Ciruelos.
Jueves 17 de mayo de 2018. SPJ§8. Chequeo de tipos polimórficos. Expositor: Gonzalo Ciruelos.
Jueves 10 de mayo de 2018. Estrategias de evaluación en el cálculo-λ. [pdf] Expositor: Pablo Barenbaum.
Jueves 3 de mayo de 2018. SPJ§7. Compilación de listas por comprensión al cálculo-λ enriquecido. Expositor: Gonzalo Ciruelos.
Jueves 26 de abril de 2018. SPJ§6. Transformaciones sobre el cálculo-λ enriquecido: expresión de let, letrec y pattern matching en términos de lambdas. Expositor: Gonzalo Ciruelos.
Jueves 19 de abril de 2018. SPJ§4. Semántica de un cálculo-λ con pattern matching. Expositor: Gonzalo Ciruelos.
Jueves 12 de abril de 2018. SPJ§3–4.2. Traducción de un lenguaje funcional de alto nivel con pattern matching a un cálculo-λ enriquecido. Expositor: Gonzalo Ciruelos.
Jueves 5 de abril de 2018. Cálculo-λ sin tipos: codificación de funciones recursivas en cálculo-lambda. Máquina abstracta de Krivine para evaluación call-by-name. Expositor: Pablo Barenbaum.
Lunes 11 de diciembre de 2017. Simulación del λ-cálculo de matrices densidad en el λ-cálculo cuántico de Selinger-Valiron, y viceversa. Trabajo de tesis en progreso, supervisado por Alejandro Díaz-Caro. Expositor: Agustín Borgna.
Lunes 4 de diciembre de 2017. Notación à la Church para un sistema de tipos intersección no idempotente. Propiedades: subject reduction, confluencia, normalización fuerte, simulación. Sus derivaciones forman un reticulado distributivo. Trabajo de tesis en progreso, supervisado por Pablo Barenbaum. Expositor: Gonzalo Ciruelos.
Lunes 27 de noviembre de 2017. HoTT§7. Teorema de Hedberg: los tipos con igualdad decidible son conjuntos. Generalización del Axioma K para n-types. Expositor: Pablo Barenbaum.
Lunes 13 de noviembre de 2017. HoTT§7.1: Definición de n-types. Propiedades. Expositor: Pablo Barenbaum.
Lunes 6 de noviembre de 2017. HoTT§6: Higher inductive types: la esfera S2 es la suspensión del círculo S1 (incompleto). Expositor: Pablo Barenbaum.
Lunes 30 de octubre de 2017. HoTT§6: Cocientes expresados como HITs. Caracterizaciones alternativas usando clases de equivalencia y representantes canónicos. Expositor: Pablo Barenbaum.
Lunes 23 de octubre de 2017. HoTT§6: Higher inductive types. Esferas: aplicación dependiente de funciones a caminos de orden 2. Transporte de caminos de orden 2. Definición del toro canónica y usando radios. Coproductos. Truncamiento de un tipo a un conjunto. Expositor: Teo Freund.
Lunes 9 de octubre de 2017. HoTT§6: Higher inductive types. Definición del círculo: principio de inducción implica principio de recursión. Unicidad de definiciones recursivas. Tipo intervalo. Suspensiones. Expositor: Pablo Barenbaum.
Lunes 2 de octubre de 2017. HoTT§5. Tipos inductivos como F-álgebras iniciales. Expositor: Pablo Barenbaum.
Lunes 18 de septiembre de 2017. HoTT§5. Tipos de datos inductivos. Unicidad de los tipos inductivos. Árboles bien fundados de Martin-Löf. Tipos inductivos como F-álgebras iniciales. Expositor: Pablo Barenbaum.
Lunes 11 de septiembre de 2017. HoTT§4. Definición de equivalencia de tipos a través de funciones [con fibras] contráctiles. Equivalencia entre esta y otras nociones de equivalencia de tipos. Expositor: Gonzalo Ciruelos.
Lunes 28 de agosto de 2017. HoTT§4: qinv(f) no es contráctil; definición de equivalencia de tipos a través de funciones bi-invertibles y half adjoint equivalences. Equivalencia entre ambas definiciones. Expositor: Gonzalo Ciruelos.
Viernes 25 de agosto de 2017. Motivación para algunos conceptos de HoTT: algunas nociones que provienen de la topología algebraica (grupo fundamental e invariancia homotópica). Introducción a Cubical Type Theory. Expositor: Luis Scoccola (Universidad de Western Ontario).
Jueves 13 de julio de 2017. HoTT§3. Tipos contráctiles. Conclusión del capítulo 3. Expositor: Pablo Barenbaum.
Jueves 6 de julio de 2017. HoTT§3. Repaso de propiedades universales. Truncamientos. Axioma de elección clásico expresado usando truncamientos. Axioma de elección no vale para tipos en general. Expositor: Pablo Barenbaum.
Jueves 29 de junio de 2017. HoTT§3. Proposiciones: definición de isProp; isSet e isProp son proposiciones. Conjuntos, subconjuntos y subtipos. Axiomas del tercero excluido y propositional resizing. Expositor: Pablo Barenbaum.
Jueves 22 de junio de 2017. HoTT§3.1–3.2. Discusión sobre la técnica code/decode como mecanismo general para decidir un predicado proposicional (A → Type) si se cuenta con un procedimiento de decisión (A → 2). Definición de isSet y ejemplos. Jerarquía de n-types. Todos los conjuntos son 1-types. La doble negación no vale en general en HoTT. Expositor: Pablo Barenbaum.
Jueves 15 de junio de 2017. HoTT§2.10–2.13. Axioma de univalencia. Espacio de caminos del tipo identidad. Técnica code/decode para caracterizar el espacio de caminos del coproducto y los números naturales. Expositores: Agustín Borgna, Teo Freund.
Jueves 8 de junio de 2017. HoTT§2. Extensionalidad funcional (happly y funext).
Jueves 1 de junio de 2017. Repaso de HoTT§1-2.
Jueves 18 de mayo de 2017. Repaso de HoTT§1-2. Expositores: Gonzalo Ciruelos, Teo Freund.
Jueves 11 de mayo de 2017. HoTT§2. Equivalencia de tipos. Caracterización del espacio de caminos de como el producto de los espacios de caminos. Expositor: Pablo Barenbaum.
Jueves 4 de mayo de 2017. HoTT§2. Repaso de las operaciones ap, apd, transport y transportconst y relación entre ellas. Homotopías entre funciones. Expositor: Teo Freund.
Jueves 27 de abril de 2017. HoTT§2. Funciones dependientes como funtores. Transporte. Expositor: Teo Freund.
Jueves 20 de abril de 2017. HoTT§2.1–2.2. Propiedades de la igualdad: estructura de ω-grupoide. Teorema de Eckmann–Hilton. Funciones (no dependientes) como funtores entre ω-grupoides. Expositor: Teo Freund.
Jueves 30 de marzo de 2017. HoTT§1. Igualdad proposicional, inducción en caminos. Expositor: Pablo Barenbaum.
Jueves 23 de marzo de 2017. HoTT§1. Juicios y proposiciones. Funciones y funciones dependientes. Pares y pares dependientes. Expositor: Pablo Barenbaum.
Martes 1 de noviembre de 2016. TAPL§22–23. Let-Polymorphism. System F. Indecidibilidad de reconstrucción de tipos en System F; fragmentos decidibles. Expositor: Francisco Giordano.
Martes 11 de octubre de 2016. CH§10. Sistema T de Gödel. Expositor: Teo Freund.
Martes 27 de septiembre de 2016. CH§9. Aritmética de primer orden. Expositor: Teo Freund.
Martes 20 de septiembre de 2016. PAM§2. Definición del sistema de multipasos asociado a un sistema de reescritura axiomático. Residuos de derivaciones y propiedades. Expositor: Pablo Barenbaum. Pendiente: Join de derivaciones. Parallel moves lemma. Cube lemma. Confluencia algebraica.
Martes 13 de septiembre de 2016. Presentación del artículo Notions of computation and monads de E. Moggi. Expositor: Francisco Giordano.
Martes 6 de septiembre de 2016. PAM§2. Definición de sistema de reescritura axiomático de Melliès. Definición general de derivación y development. Creación de redexes en el cálculo-λ. Profundidad de un conjunto de pasos. Equivalencia por permutación. Todos los developments completos de un conjunto de pasos son equivalentes por permutación. Expositor: Pablo Barenbaum.
Martes 30 de agosto de 2016. Residuos en el cálculo-λ: definición usando descendientes de posiciones, y definición usando un cálculo con etiquetas. Developments y developments completos. Versión fuerte del teorema de finite developments. Expositor: Pablo Barenbaum.
Martes 23 de agosto de 2016. CH§8. Correspondencia entre proposiciones y tipos para la lógica de primer orden. Deducción natural para lógica de primer orden. Cálculo λP1. Tipos universales como funciones dependientes y tipos existenciales como pares dependientes o tipos abstractos. Expositor: Pablo Barenbaum.
Martes 16 de agosto de 2016. Repaso de categorías. Funtores, funtores aplicativos y mónadas para programación funcional. Fuente recomendada: Typeclassopedia. Expositor: Pablo Barenbaum.
Jueves 30 de junio de 2016. BS§11, IL. Lógica lineal: eliminación del corte en proof nets para los conectivos exponenciales. Codificación del cálculo-lambda simplemente tipado en MELL. Introducción a la expansión de Taylor de λ-términos [TE]. Expositores: Luis Scoccola, Pablo Barenbaum.
Jueves 23 de junio de 2016. BS§11, IL. Lógica lineal: conectivos exponenciales. Traducción de derivaciones secuenciales en proof nets. Eliminación del corte en proof nets para el fragmento multiplicativo. Criterio de corrección de Danos-Regnier. Expositor: Pablo Barenbaum.
Jueves 16 de junio de 2016. BS§9, IL. Lógica lineal: presentaciones bilateral vs. unilateral (two-sided vs. one-sided). Conectivos multiplicativos, aditivos y unidades (MLL, MALL). Expositor: Pablo Barenbaum.
Jueves 9 de junio de 2016. BS§8. Espacios de coherencia. Funciones estables y lineales. Categoría COH de los espacios de coherencia con funciones lineales. Implicación lineal como el Hom interno en COH. Expositor: Gonzalo Ciruelos.
Jueves 2 de junio de 2016. CH§7. Cálculo de secuentes. Eliminación del corte. Correspondencia de la variante minimal del cálculo de secuentes con un cálculo de sustituciones explícitas. Expositor: Teo Freund.
Jueves 26 de mayo de 2016. CH§6. Presentación de la lógica clásica con deducción natural y axiomatización à la Hilbert. Mención de la correctitud y completitud de la lógica con respecto a valuaciones binarias. Presentación del cálculo λμ. Motivación de sus reglas de reducción desde las perspectivas lógica y computacional. Correspondencia entre proposiciones y tipos, terminación y confluencia del cálculo λμ. Traducción de doble negación de Kolmogorov como conversión a Continuation-Passing Style. Expositor: Pablo Barenbaum.
Jueves 19 de mayo de 2016. CH§5. Axiomatización de la lógica minimal proposicional con axiomas à la Hilbert. Correspondencia con la lógica combinatoria simplemente tipada. Traducciones entre la lógica combinatoria y el cálculo-lambda simplemente tipado. Expositor: Gonzalo Ciruelos.
Jueves 12 de mayo de 2016. CH§4.4‒4.6. Normalización de pruebas, diálogos prover-skeptic. Expositor: Pablo Barenbaum.
Jueves 5 de mayo de 2016. PT§6. Demostración de la terminación fuerte del cálculo-λ simplemente tipado, basada en la técnica de candidatos de reducibilidad de Girard. CH§4.1-4.3. correspondencia entre el fragmento implicacional de la lógica intuicionista y el cálculo-lambda simplemente tipado, comentario sobre la complejidad PSPACE de decidir si un tipo está habitado. Expositor: Pablo Barenbaum.
Jueves 28 de abril de 2016. CH§3. Cálculo-λ simplemente tipado. Equivalencia entre tipado y unificación. Algoritmo de reconstrucción de tipos (§3.2); demostración de weak normalization (WN) usando el orden lexicográfico sobre el grado de los tipos y strong normalization (SN) pasando por el cálculo lambda-I (§3.5). Expositor: Francisco Giordano.
Jueves 21 de abril de 2016. CH§2.5‒2.6. Modelos de Kripke. Filtros y filtros primos en un álgebra de Heyting. Completitud y correctitud de los modelos de Kripke para la lógica intuicionista, usando el modelo de Kripke cuyos elementos son los filtros primos de un álgebra de Heyting. Expositor: Gonzalo Ciruelos.
Jueves 14 de abril de 2016. CC. Introducción a la teoría de categorías con varios ejemplos que provienen de la computación. La teoría de categorías permite abstraer muchas nociones que se repiten en la matemática. Gracias a esta abstracción podemos probar equivalencias entre teorías de forma concreta. Por ejemplo veremos que el estudio de cálculos lambda simplemente tipados es equivalente al estudio de las categorías cartesianamente cerradas. También existen equivalencias similares para cálculos lambda más complejos. Una referencia bastante completa de estos y muchos más temas es. Expositor: Luis Scoccola.
Jueves 7 de abril de 2016. CH§2.1‒2.4. Introducción a la lógica intuicionista: fórmulas, interpretación BHK, deducción natural proposicional/intuicionista. Definición de álgebra de Heyting. Construccion del álgebra de Lindenbaum asociada a un contexto. Completitud y corrección de las álgebras de Heyting para la lógica intuicionista. Expositor: Pablo Barenbaum.
Jueves 31 de marzo de 2016. CH§1.5. Caracterización de las formas normales en el cálculo-λ sin tipos. Redexes leftmost, head, e internos. Reducción paralela interna. Permutación de los redexes head vs. internos. Normalización de la estrategia leftmost. Expositor: Pablo Barenbaum.
Jueves 10 de marzo de 2016. CH§1.1‒1.4. Introducción al cálculo-λ sin tipos: definición de los términos como clases de α-equivalencia, β-reducción, confluencia del cálculo-λ sin tipos por medio de la técnica de Tait y Martin-Löf, usando reduccion paralela y la noción de development completo de Takahashi. Expositor: Pablo Barenbaum.
Jueves 30 de octubre de 2014. HoTT§3. Resolución de ejercicios del libro y otros. Tipos contráctiles, truncación de tipos. Definición de conjunto y, más generalmente, n-tipo. Expositor: Luis Scoccola.
Jueves 25 de septiembre de 2014. HoTT§1. Repaso del capítulo 1. Discusión de un ejemplo particular de la técnica de coding-decoding (demostración de ~par(1)). Codificación de deducción natural con proof terms. Expositor: Pablo Barenbaum.
Jueves 18 de septiembre de 2014. HoTT§2.1–2.3. Estructura de weak ∞-groupoid: composición e inversa de caminos. Teorema de Eckmann-Hilton. Funciones son funtores. Operador de transporte. Expositor: Pablo Barenbaum.
Jueves 4 de septiembre de 2014. HoTT§1.7–1.12,2. Proposiciones como tipos. Igualdad proposicional. Inducción sobre caminos e inducción "basada" sobre caminos (based path induction). Resolución de algunos ejercicios: 1.10 (función de Ackermann), 1.13 (¬¬(p v ¬p)). Introducción informal a la interpretación de la igualdad proposicional como caminos con estructura de weak ∞-groupoid. Pentágono de Mac Lane. Expositor: Luis Scoccola.
Jueves 21 de agosto de 2014. Cuestiones básicas sobre la teoría de tipos de HoTT. Juicios y proposiciones. Igualdad definicional y proposicional. Universos y familias. Reglas de formación, introducción, eliminación y cómputo: funciones dependientes, productos, pares dependientes, coproductos. Expositor: Pablo Barenbaum.
Jueves 3 de julio de 2014. Cómo funciona un asistente de demostración. Los asistentes de demostración ayudan a verificar formalmente la corrección de definiciones, teoremas y sus demostraciones. Hay decenas de asistentes, basados en distintos fundamentos (Coq, Isabelle, HOL Light, PVS, ACL2, Mizar, Metamath, Agda, etc.). En esta charla se hizo una introducción rudimentaria a Coq, un asistente basado en teoría de tipos. Expositor: Pablo Barenbaum.
Jueves 19 de junio de 2014. Theorems for free. El tipo de una expresión provee mucha información sobre su valor. Por ejemplo, la única función posible de tipo a → a es la identidad. En esta charla se presentó el artículo Theorems for free de Philip Wadler, donde para cada tipo polimórfico se deriva un teorema que cumplen todas las expresiones de ese tipo. Expositor: Federico Lebrón.
Jueves 5 de junio de 2014. Zippers y derivadas de tipos. Introducción a la noción de isomorfismo de tipos. Análisis de la estructura de datos conocida como zipper, utilizada para "iterar" y "modificar" estructuras de datos de manera puramente funcional. Relación entre el tipo de los zippers y la derivada formal de un tipo. Expositor: Pablo Barenbaum.
Jueves 22 de mayo de 2014. Estructuras de datos funcionales. Colas puramente funcionales en O(1) amortizado y peor caso. Análisis de complejidad amortizada usando técnicas del físico y del banquero. Implementación de streams usando memoización. Evaluación lazy como requisito para lograr estructuras de datos persistentes eficientes. Vectores persistentes de Clojure (hashed array mapped tries). Finger trees. Expositor: Juan Pablo Darago.
Jueves 8 de mayo de 2014. Tipos dependientes en Haskell y Agda. Presentación de la noción de tipos dependientes en Haskell y Agda. Se ilustraron maneras interesantes de aprovechar el sistema de tipos para garantizar invariantes complejos estáticamente (en tiempo de compilación). Ejemplo interesante: tipo de datos para árboles que sólo admite instancias balanceadas (p.ej. que cumplan el invariante de un AVL). Expositor: Federico Lebrón.
Jueves 24 de abril de 2014. Continuaciones y call/cc. Introducción a las continuaciones first-class y el operador de control call/cc. Codificación de estructuras de control basadas en el manejo de continuaciones: excepciones, iteradores, co-rutinas. Dos maneras de implementar call/cc: reificación de la pila de llamadas y conversión a Continuation-Passing Style. Expositor: Pablo Barenbaum.
Jueves 3 de abril de 2014. Funtores y mónadas. Introducción a algunos conceptos modernos de programación funcional desde una perspectiva teórica: funtores, mónadas y funtores aplicativos. La charla se basó en las primeras secciones de la Typeclassopedia de Brent Yorgey. Expositor: Federico Lebrón.
Jueves 20 de marzo de 2014. Introducción al cálculo lambda sin tipos. Términos, alfa equivalencia, beta conversión. Codificación de tipos de datos y funciones recursivas usando únicamente lambdas. Expositor: Pablo Barenbaum.