XLIII Curso de actualización en matemáticas. El glorioso Programa Univalente (in memoriam William Lawvere)

La disciplina de la verificación formal estudia tanto métodos matemáticos para comprobar el funcionamiento de algoritmos computacionales, cómo métodos computacionales para verificar la correctitud de desarrollos matemáticos.

Existe una gran cantidad de Matemáticas desarrolladas para la relación entre la Lógica, la programación, y otras tantas áreas; y es un campo de estudio con gran actualidad, sobre todo relacionada con el desarrollo de asistentes para la demostración de teoremas cada vez más potentes.

En las matemáticas en la base de estos desarrollos, encontramos la figura indeleble de William Lawvere (1937-2023), matemático fundamental en el desarrollo de innumerables subdisciplinas de la Teoría de Categorías, pero en concreto, la Teoría de Topos y la Lógica Categórica.

En esta charla, recordamos su obra, pero no afrontándola directamente, que sería imposible por la dificultad y duración del resultado. En su lugar, expondremos la historia y objetivos del Programa Univalente de Fundamentación, programa de investigación subyacente en lenguajes de programación como Agda, y que tanto debe a Lawvere.