Existen diversas técnicas para la verificación formal del software. Una de ellas es programar en un lenguaje – por ejemplo, Coq, Agda y Lean – basado en la teoría de tipos de Martin-Löf. Esto ofrece la posibilidad de incluir pruebas de corrección en los programas. Tales lenguajes también se utilizan para verificar pruebas complejas de importantes teoremas matemáticos.
En este curso, proporcionaremos a los estudiantes una introducción a la teoría de tipos de Martin-Löf y sus implementaciones, en particular Coq. Exploraremos la expresividad de esta teoría y cómo los distintos asistentes de prueba y sus bibliotecas limitan esta expresividad al imponer axiomas adicionales, lo que lleva a una teoría de tipos extensional o a una teoría de tipos de homotopías (o algo intermedio). Veremos cuándo es apropiado imponer tales axiomas; por ejemplo, veremos que la teoría de tipos de homotopías proporciona un entorno para la verdadera independencia de representación de los tipos de datos.
Teoría de tipos de Martin-Löf (MLTT): tipos dependientes, tipos inductivos
Programación en Coq
Uso de la biblioteca UniMath
Axiomas en MLTT: K, univalencia
Semántica de MLTT: lógica (correspondencia Curry-Howard), conjuntos, espacios
Aspectos extensionales y de homotopía de MLTT: transporte, functorialidad del tipo identidad, grupoide de tipos
Verificación formal de las matemáticas en MLTT, utilizando diferentes axiomas
Independencia de representación mediante univalencia
Biblioteca UniMath
Experiencia en programación funcional.
Bengt Nordström, Kent Petersson, Jan M. Smith, Programming in Martin-Löf ’s Type Theory, available from https://www.cse.chalmers.se/research/group/logic/book/.
Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, available from https://homotopytypetheory.org/book
Carlo Angiuli, Evan Cavallo, Anders Mörtberg, Max Zeuner, Internalizing Representation Independence with Univalence, available from https://arxiv.org/abs/2009.05547
Desarrollado por el Departamento de Computación, FCEyN, UBA