Dependent Type Theory - Una Introducción

Abstract: Estos sistemas utilizan la correspondencia Curry-Howard para integrar la computación y la lógica. Sirven para fundamentar la matemática y son utilizados como base por proof assitants como, por ejemplo Nuprl, Coq, Lean o Agda.

En esta charla mostraremos los mecanismos básicos de este tipo de lógicas.

Spanishlogic in computer sciencelogic

Audience: researchers in the topic

( slides | video )

---

Seminario de álgebra, combinatoria y teoría de Lie

Series comments: The talks are usually in Spanish. Las instrucciones para recibir el link de zoom están en la página web del seminario: sites.google.com/view/semact-uns/.

---