====== 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. [[http://coq.inria.fr/|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 [[http://compcert.inria.fr/compcert-C.html|CompCert]], un compilador certificado para C usado por empresas de áreas críticas como Airbus, y la demostración verificada del [[https://en.wikipedia.org/wiki/Four_color_theorem|Four-Color Theorem]]. Este curso está basado en el novedoso currículo [[https://softwarefoundations.cis.upenn.edu/draft/index.html|Software Foundations]], usado en prestigiosas instituciones en todo el mundo. Ver el {{teaching:cc7125:programa-coq.pdf|programa del curso}}. ---- ====== Recursos ====== * Download {{teaching:cc7125:lf-full.zip|Volume 1: Logical foundations}}. * Download {{teaching:cc7125:plf-full.zip|Volume 2: Programming languages foundations}}. ---- **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 [[etanter@dcc.uchile.cl|É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.