Breve resumen de la materia

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.

Abstract

There are various techniques for formal verification of software. One technique is to program in a language – e.g. Coq, Agda, and Lean – based on Martin-Löf type theory. This offers the ability to include proofs of correctness in one’s programs. Such languages are also used to check complex proofs of important mathematical theorems.

In this course, we will provide students with an introduction to Martin-Löf type theory and implementations, in particular Coq. We will explore the expressiveness of this theory, and how the various proof assistants and their libraries limit this expresiveness by imposing additional axioms, leading to either extensional type theory or homotopy type theory (or something in between). We will see when it is appropriate to impose such axioms; for instance, we will see that homotopy type theory provides a setting for true representation independence of data types.

Objetivos del curso

Los objetivos de aprendizaje de este curso son los siguientes:

1. Conocer qué es la teoría de tipos dependientes y cuándo es útil.
2. Familiarizarse con la programación en Coq y la biblioteca UniMath.
3. Comprender las diferencias entre las distintas implementaciones de la teoría de tipos dependientes (es decir, Lean, Coq, Agda, Cubical Agda).
4. Saber cuándo se pueden o deben aplicar axiomas como el Axioma K o el Axioma de Univalencia.
5. Comprender y programar con tipos inductivos y tipos inductivos superiores.

Objectives of the Course

The learning objectives for this course are the following.

1. Know what dependent type theory is and when it is useful
2. Become familiar with programming in Coq and the UniMath library
3. Understand the differences between different implementations of dependent type theory (i.e. Lean, Coq, Agda, Cubical Agda)
4. Know when one can or should apply axioms such as Axiom K or the Univalence Axiom
5. Understand and program with inductive types and higher inductive types

Programa

• 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

Brief Index

• Martin-Löf type theory (MLTT): dependent types, inductive types
• Programming in Coq
• Using the UniMath library
• Axioms in MLTT: K, univalence
• Semantics of MLTT: logic (Curry-Howard correspondence), sets, spaces
• Extensional and homotopy aspects of MLTT: transport, functoriality of identity type, groupoid of types
• Formal verification of mathematics in MLTT, using different axioms
• Representation independence using univalence
• UniMath library

Prerrequisitos

Experiencia en programación funcional

Preferred Background

Experience in functional programming

Bibliografía/Bibliography

• 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