This is an old revision of the document!


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

Trail 2017/2

  • Jul 31: slides “certified software”, primer contact con Coq (primeras definiciones de Basics.v)
  • Aug 2: Basics.v (ver últimos ejercicios en auxiliar)
  • Aug 7: Induction.v, Lists.v (hasta antes de options)
  • Aug 9: Lists.v (final), Poly.v (dejando higher-order/anonymous functions para trabajo casa/auxiliar)
  • Aug 14: Tactics.v
  • Aug 16: Logic.v (hasta True)
  • Aug 21: Logic.v (hasta fun_ext)
  • Aug 23: Logic.v (clase corta por paro)
  • Aug 28-30: no hay clases
  • Sep 4: IndProp.v (hasta regexp - el resto queda para auxiliar)
  • Sep 6: ProofObjects.v
  • Sep 11: IndPrinciples.v (rápido) e introducción a programación con tipos dependientes (deptypes.v)
  • Sep 13: Imp.v (hasta antes de “Evaluation as a Relation”)
  • <vacaciones 18 / semana olimpica>
  • Oct 2: Imp.v (hasta ceval_example2)
  • Oct 5: Imp.v / ImpCEvalFun.v / Extraction.v
  • Oct 9: feriado
  • Oct 11: Auto.v / inicio de Equiv.v (definición de nociones de equivalencia)
  • Oct 16: Equiv.v
  • Oct 18: Hoare.v (hasta proof rule de SKIP)
  • Oct 23: Hoare.v
  • Oct 25: Hoare2.v (hasta Example: Parity)
  • Oct 30: Hoare2.v
  • Nov 1: feriado
  • Nov 6: Smallstep.v (hasta normalizing)
  • Nov 8: Smallstep.v
  • Nov 13:
  • Nov 15: JSCert (M. Bodin)
  • Nov 20: JSCert (M. Bodin)
  • Nov 22: Verificación de Programas Probabilísticos (F. Olmedo)

Proyectos-2017


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.