CC7125 / MA7125 - Introducción a Coq: Lógica, Tipos, y Verificación


Este curso introduce los fundamentos matemáticos de la construcción de software confiable. Esto incluye conceptos básicos de lógica, demostraciones de teoremas asistidas por computador, el asistente de pruebas Coq, programación funcional, semántica operacional, lógica de Hoare, y sistemas de tipos estáticos.

El contenido del curso es 100% formalizado y verificado en Coq. Coq es a la vez un lenguaje de programación y un asistente de pruebas formales. En Coq se pueden definir programas (y lenguajes), enunciar propiedades formales precisas al respecto, y producir demostraciones rigurosas—automáticamente verificadas—de dichas propiedades. Podemos, por ejemplo, construir un programa que implemente el algoritmo de Dijkstra sobre grafos, y probar–formalmente–que es correcto.

Coq es el asistente de prueba más usado en el mundo, tanto por matemáticos como informáticos. Exitosos casos de uso de Coq incluyen CompCert, un compilador certificado para C usado por empresas de áreas críticas como Airbus, y la demostración verificada del Four-Color Theorem.

Este curso está basado en el novedoso currículo Software Foundations, usado en prestigiosas instituciones en todo el mundo.

Ver el programa del curso.


Recursos


Curso válido para carreras del DCC: Doctorado en Computación, Magíster en Ciencias de la Computación, Ingeniería Civil en Computación
y carreras del DIM: Doctorado en Ciencias de la Ingeniería, mención Modelación Matemática; Magíster en Ciencias de la Ingeniería, mención Matemáticas Aplicadas; Ingeniería Civil Matemática

Requisitos: DCC: CC4101 / DIM: MA3705 o MA4702 / autorización (contactar Éric)

El curso no presume ningún conocimiento previo en lógica o lenguajes de programación, aunque un cierto grado de madurez matemática y/o de exposición a lenguajes será de ayuda.