Ciencias de la Computación (plan 2013) 2024-1

Optativas, Seminario de Ciencias de la Computación B

El objetivo de este curso es dar una introducción a la teoría estructural de la prueba, haciendo énfasis en sus aplicaciones en Ciencia de la Computación Teórica, en específico estudiando los procesos de normalización y búsqueda de pruebas como nociones de cómputo así como la correspondencia de Curry-Howard y sus aplicaciones en los sistemas de tipos para lenguajes de programación.

Prerrequisitos: Si bien el curso será autocontenido es deseable haber llevado Lógica Computacional o bien algún curso de Lógica Matemática. Una ventaja adicional es haber llevado Lenguajes de Programación.

Forma de evaluación: mediante ejercicios semanales, tareas mensuales y una exposición al final del semestre (calificando documento escrito y presentación ante el grupo)

Temario

1. Introducción: lógica proposicional y de predicados, sistemas deductivos axiomáticos.

2. Deducción natural: sistemas minimal, intuicionista y clásico. Búsqueda de pruebas, normalización. sistemas con reglas generalizadas.

3. Cálculo de secuentes: sistemas minimal, intuicionista y clásico, Eliminación de corte y sus aplicaciones. Búsqueda de pruebas. La relación entre normalización y eliminación de corte.

4. La Correspondencia de Curry-Howard: cálculo lambda con tipos simples, sistemas de tipos, normalización fuerte para deducción natural.

5. Lógicas no clásicas: sistemas duales para lógica modal y lógica lineal.

6. Tópicos avanzados (sujeto al tiempo): lógicas de segundo orden (PROP2, AF2), semántica mediante teoría de la prueba, realizabilidad, focusing, tipos dependientes.

Bibliografía

Gilles Dowek. Proofs and Algorithms. An Introduction to Logic and Computability. Undergraduate Topics in Computer Science. Springer 2011.

Paolo Mancosu, Sergio Galvan, Richard Zach. An Introduction to Proof Theory Normalization, Cut-Elimination, and Consistency Proofs. Oxford University Press 2021.

Sara Negri, Jan von Plato. Structural Proof Theory. Cambridge University Press 2001.

Jan von Plato. Elements of Logical Reasoning. Cambridge University Press 2013.

Harold Simmons. Derivation and Computation: Taking the Curry-Howard Correspondence seriously. Cambridge Tracts in Theoretical Computer Science Vol. 51. Cambridge University Press. 2000.

Morten H. Sorensen, Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism. Studies in Logic and the Foundations of Mathematics. Vol. 149. Elsevier 2006.

Anne S. Troelstra, Helmut Schwichtenberg. Basic Proof Theory. 2nd Edition. Cambridge University Press 2000.