Continuamos el Ciclo de Charlas este Jueves 14 por la tarde con una ponencia de un estudiante de máster y divulgador Javier Villar, parte del grupo de divulgación Vaya Primos.
Su charla se titula El Glorioso Programa Univalente: Topología, Lógica y Computación para unas nuevas Matemáticas y él nos la resume de la siguiente manera:
La disciplina de la verificación formal estudia los diálogos que se pueden establecer entre el lenguaje matemático, propio de la demostración de teoremas; y el de los lenguajes de programación, que describe a un ordenador los cómputos a realizar. Así, permite emplear lenguajes de programación, denominados asistentes de prueba, en la tarea de verificar que ciertas demostraciones son correctas; y a su vez, generar teoremas en torno a la corrección de un algoritmo, y emplear demostraciones Matemáticas para asegurar la robustez del código.
En esta charla, hablaremos del Programa Univalente, una iniciativa de investigación internacional que explora un subcampo de la verificación formal, la llamada Teoría Homotópica de Tipos. A través de exponer sus objetivos, realizaremos un viaje histórico en torno a una sorprendente colección de puentes entre disciplinas muy dispares (Topología, Lógica, Álgebra, Teoría de Conjuntos, etc), que amenazan con cambiar cómo nos relacionamos matemáticos y computadoras para siempre.
