En particular la cuarta semana, del 20 al 24 de Febrero, estará dedicada a "Enfoques Cuantitativos". Los organizadores de dicha semana son Michele Pagani, Simon Perdrix, Peter Selinger y Christine Tasson. Habrá cursos dictados por Thomas Ehrhard, Elham Kashefi, Prakash Panangaden y Christine Tasson. Además se contará con numerosos oradores invitados de renombre, y algunas contribuciones. Yo envié una contribución, la cual fue aceptada y la presentaré el martes 21 a las 15:30. Aquí dejo los datos de mi presentación (la versión en inglés la pueden consultar en la página):
Título:
Tipage vectorial
Resumen (traducción):
Tipage vectorial
Resumen (traducción):
Los cálculos lambda algebraicos son extensiones al cálculo lambda donde las combinaciones lineales de términos, son también términos. Estos cálculos pueden verse como un marco para expresar programas probabilísticos, baricéntricos, cuánticos y no-determinísticos. Más generalmente, operadores lineales y vectores pueden expresarse naturalmente en este entorno. El sistema de tipos Vectorial, en su variante à la Church, es un sistema que se ubica sobre el cálculo lambda algebraico lineal, poniendo en relieve esos operadores lineales y mostrando la estructura de los vectores formados por la forma normal de los términos. En este sistema se pueden expresar programas cuánticos. Aunque ya hemos encontrado la conexión de Curry-Howard de un fragmento del sistema con la lógica proposicional de segundo orden, aún queda un trabajo por hacer para encontrar la lógica detrás del sistema completo. En esta charla presentaré el sistema de tipos Vectorial (un trabajo en conjunto con B. Valiron y P. Arrighi), el isomorphismo de Curry-Howard de la parte aditiva (trabajos conjuntos, uno con B. Petit y otro con G. Dowek) y daré algunas pistas de direcciones futuras para encontrar la "lógica vectorial", una lógica que tendrá programas cuánticos, probabilísticos y no-determinísticos como pruebas.
Entradas
No hay comentarios:
Publicar un comentario