System F à la Curry y Grupo de trabajo

Buenas!

Les cuento que ya estoy instaladísimo en Grenoble. Lo que he hecho en estos días es adaptar un sistema de tipos polomórficos (System F à la Curry, ver [1], [3] o [4] para más detalles) al Linear-Algebraic Lambda-Calculus de Arrighi y Dowek [2], además hice una prueba de strong normalization (ver [1] o [3]) para este «Linear-Algebraic System F» y algunos comentarios respecto a que este sistema se corresponde de acuerdo al Isomorfismo de Curry-Howard (ver [4]) con la misma lógica (Lógica Proposicional de Segundo Orden) que el System F original. La idea ahora es empezar a jugar con reglas de tipos más complejas, hacer alguna clase de álgebra de tipos, para obtener alguna lógica un poco más loca. Ya les comentaré cuando tenga algo más armado :)

Este próximo jueves nos juntamos con el grupo de trabajo que estamos más o menos en los mismos temas, en lo que le hemos dado a llamar WHOCAS: «(informal) Workshop on Higer-Order Calculi and Algebraic Structures», seremos sólo 5 personas, ya que es un grupo de trabajo más que un workshop: Lionel Vaux, Benoît Valiron, Gilles Dowek, Pablo Arrighi y yo. La idea es que cada uno dará una pequeña charla de 40 minutos contando en qué está trabajando, así vemos qué colaboraciones pueden salir de allí. Luego del WHOCAS publicaré aquí las transparencias que use.

Referencias
[1] Jean-Yves Girard, Yves Lafont, Paul Taylor. Proofs and types. Cambridge University Press, 1989.
[2] Pablo Arrighi, Gilles Dowek. Linear-algebraic lambda-calculus: higher-order, encodings, and confluence. Lecture Notes in Computer Science: (RTA'08), 5117:17-31, 2008. (preprint en arXiv:quant-ph/0612199)
[3] Henk Barendregt. Lambda calculi with types, volume 2 of Handbook of Logic in Computer Science. Clarendon Press, Oxford, 1992.
[4] Morten Sørensen, Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2006. (disponible para bajar en CiteSeer)

Preparando las valijas

Los últimos posts de este blog han sido demasiado personales para mi gusto (comentando en qué ando). Pero bueno, lo voy a cambiar dentro de poco cuando empieze el doctorado.

Por ahora les comento, el Jueves 9 de Octubre llego a Grenoble, al grupo Quantum Computation in Grenoble, donde iniciaré mi doctorado bajo la dirección de Pablo Arrighi. La idea es que el doctorado dure tres años, espero terminarlo a tiempo :)

El trabajo será en lógica cuántica y teoría de tipos para la computación cuántica, e iré contando detalles a medida que vayamos obteniendo resultados. Mi idea es continuar este blog como un "diario de doctorado", donde iré contando los avances que vayamos teniendo.

Charla de Julia Kempe en la UBA

Dia y hora:

MIERCOLES 13/8, 14hs

Lugar:

AULA FEDERMAN, PRIMER PISO, PABELLON 1
Facultad de Ciencias Exactas y Naturales, UBA

Titulo:

From Bell's inequalities to computational complexity

por Julia Kempe
Department of Computer Science, University of Tel Aviv, Israel

Resumen: Since the seminal work of John Bell it has been known that quantum entanglement between two parties can produce correlations that are not possible in a classical world, even with hidden variables. This has been one of the most remarkable discoveries and a formidable tool to prove the validity of quantum mechanics in the lab.

Computer scientists have long since appropriated Bell's inequalities. Perhaps the most prominent "application" is in unconditionally secure quantum cryptography. But among the most important challenges in the field currently is to understand the computational complexity of computing the violation of Bell's inequalities, or, in computer science lingo, the hardness of entangled multi-prover interactive proofs. Surprisingly, one of the most important approaches currently in this area builds on the work of Tsirelson who gave upper bounds on the maximal violation of Bell inequalities using semidefinite programming. I will explain the connection and the questions in this area and give an overview of some recent results, which, surprisingly, also give rise to new Bell inequalities.