- Este evento ha pasado.
El Glorioso Programa Univalente: Topología, Lógica y Computación para unas nuevas Matemáticas | Ciclo de Charlas
14 de marzo @ 16:00 - 17:00
La segunda charla de nuestro ciclo será impartida por Javier Villar, quien nos presenta su charla El Glorioso Programa Univalente: Topología, Lógica y Computación para unas nuevas Matemáticas como sigue:
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.
Directo en YouTube ↗
Colabora
