¡Esta página será actualizada continuamente durante el semestre!
Andrés Sicard
Ramírez <asr(at)eafit(dot)edu(dot)co>
Horario de atención: Martes, 2:30 p.m. – 3:30
p.m., oficina 19-409
Profesor del curso
Coordinador de la Línea de Lógica y Estructuras Discretas
Sergio Ramírez Rico
<ssramirezr(at)eafit(dot)edu(dot)co>
Jefe de la carrera de Ingeniería de Sistemas
Andrés
Sicard Ramírez <pregrado.is(at)eafit(dot)edu(dot)co>
Clase 5429, 3:00 p.m. – 4:30 p.m.
Miércoles, aula 33-401
Viernes, aula 35-402
Henk Barendregt (1992). Functional Programming and Lambda Calculus. En: Handbook of Theoretical Computer Science. Volume B. Formal Models and Semantics. Editado por Jan van Leeuwen, Second impression. MIT Press. Capítulo 7. DOI.
Susanna S. Epp (2011). Matemáticas Discretas con Aplicaciones. 4.ª edición. Cengage Learning. Correcciones [ pdf ].
Raúl Gómez Marín y Andrés Sicard Ramírez (2025) Informática Teórica: Elementos Propedéuticos. Reimpresión digital con algunas correcciones y modificaciones disponible aquí.
Winfried Karl Grassman y Jean-Paul Tremblay [1996] (2003). Matemáticas Discretas y Lógica. Una Perspectiva desde la Ciencia de la Computación. Traducido por Rafael García-Bermejo, María Luisa Díez Platas y Vivian de los Ángeles Fernández Vásquez. Última reimpresión. Prentice Hall. Correcciones [ pdf ].
| Actividad | % |
|---|---|
| Exámenes parciales | Primer parcial 20%, segundo parcial 25%, tercer parcial 25% |
| Otros actividades | Tres actividades cada una del 10% |
| Actividad | Semana | Fecha | Material y/o temas |
|---|---|---|---|
| Primer examen | 5.ª | Miércoles, agosto 13 | • Los temas presentados en clase y las lecturas asignadas.
• Historia de la computación. • Modelos de computación: Introducción. • Relaciones de equivalencia (secciones 8.1, 8.2 y 8.3 del texto guía). • Modelo de computación: Lambda cálculo (desde el comienzo hasta definición 2.1.6 (inclusive) del texto guía). |
| Primera actividad | 6.ª | Viernes, 29 de agosto, 11:59 p.m. | Church's Encoding for Booleans |
| Segundo examen | 10.ª | Miércoles, 17 de septiembre | • Los temas presentados en clase y las lecturas asignadas.
• Modelo de computación: Lambda cálculo (desde la definición 2.1.7 hasta la definición 2.2.5 (inclusive) del texto guía). • Verificación de programas: Introducción. • Verificación de programas: Lógica de Hoare (sección 9.1 del texto guía). |
| Segunda actividad | 12.ª | Martes, 14 de octubre, 11:59 p.m. | Automatic Theorem Provers |
| Tercera actividad | 16.ª | Lunes, 3 de noviembre, 11:59 p.m. | Frama-C |
| Tercer examen | 16.ª | Viernes, 7 de noviembre | • Los temas presentados en clase y las lecturas asignadas.
• Verificación de programas: Lógica de Hoare (secciones 9.2, 9.3, 9.4.1, 9.4.2 y 9.4.3 del texto guía). |
| Tema | Diapositivas |
|---|---|
| Introducción al curso | [ pdf ] |
| Historia de la computación | [ pdf ] |
| Modelos de computación: Introducción | [ pdf ] |
| Relaciones de equivalencia (preliminares) | [ pdf ] |
| Modelo de computación: Lambda cálculo | [ pdf ] |
| Verificación de programas: Introducción | [ pdf ] |
| Verificación de programas: Lógica de Hoare | [ pdf ] |
| Verificación de programas: Frama-C y su pluging WP | [ pdf ] |
| Cardinalidad (preliminares) | [ pdf ] |
| Modelo de computación: Funciones recursivas | [ pdf ] |
| Teoría de la información | En elaboración |
| Apéndice: Instrucciones repositorio | [ pdf ] |
| Apéndice: Testing con QuickCheck | [ pdf ] |
| Apéndice: Computer Assisted Proofs | [ pdf ] |