Talk @ Paris 13

(English version below)

El próximo 17 de enero daré una charla sobre los sistemas de tipos algebraicos en Paris 13 (Lab LIPN) en las series "Sémiraires LCR". Aquí está la información y aquí reproduzco el resumen:

En esta charla voy a presentar varias extensiones a System F, para tipar el lambda-cálculo lineal-algebraico, un lambda-cálculo enriquecido con una estructura vectorial. El primer sistema de tipos es una extensión directa de System F, el cual sólo tipa el cálculo sin más adorno. El segundo es un sistema de tipos que tiene en cuenta escalares, el cual puede servir como una garantía de que la forma normal de un término tiene forma con . El siguiente sistema incluye "suma de tipos" reflejando los de los términos -- mostrando que las sumas en el cálculo algebraico se comportan como una clase particular de pares. Finalmente el último sistema de tipos combina los dos anteriores. Damos contraejemplos de porqué este tipo de sistema de tipos vectorial no se puede hacer en estilo Curry y mostramos algunas pistas de un futuro sistema de tipos vectorial en estilo Church, adecuado para especializarlo en un cálculo cuántico.

Edit: Aquí dejo los slides.

---

Next January 17th I will give a talk about the algebraic type systems at Paris 13 (LIPN Lab) in the series "Sémiraires LCR". Here it is the information and I reproduce here the abstract:

In this talk I will present several extensions to the System F, for the sake of type the linear-algebraic lambda-calculus, a lambda-calculus enriched with a vectorial structure. The first type system is a straightforward extension of System F, which just types the calculus without any further adornment. The second one is a type system accounting for scalars, which can serve as a guarantee that the normal form of a term is of the form with . The following system includes "sums of types" reflecting that of the terms--showing that sums in the algebraic calculus behaves as a special kind of pairs. Eventually the last type system combines the previous two. We give counterexamples of why this kind of vectorial type system cannot be made in Curry style and show the clues of a future vectorial type system in Church style suitable to specialize the calculus into a quantum calculus.

Edit: Here are the slides.

Slides Types 2010

Como ya había adelantado, la semana pasada estuve en Varsovia participando del workshop Types 2010. Los slides de mis presentaciones están disponibles a través de mi página web: Sums in algebraic lambda-calculi y A vectorial type system (work-in-progress).

Hubo en general muy buenas charlas. En particular, les recomiendo ver los slides de la excelente charla de Henk Barendregt: Lambda calculus with types.

Oxford → Marsella → Turín

Las últimas semanas he estado viajando un poco:

• Del 24 al 30 de Mayo fui a Oxford donde se llevó a cabo la spring school foundational structures in quantum computation and information (escuela de primavera estructuras fundamentales en computación e información cuántica), seguida del workshop quantum physics and logic (Física y Lógica Cuánticas). Los videos de todas las charlas de la escuela están acá y del workshop acá. Allí mismo tienen videos de eventos anteriores ordenados por evento o por speaker.
• El 8 de Junio fui a Marsella al primer encuentro del proyecto QuAND a presentar el "additive type system" (próximamente en arXiv), trabajo realizado con Barbara Petit, y la traducción del Linear-Algebraic Lambda-Calculus al Algebraic Lambda-Calculus (y viceversa), trabajo realizado con Simon Perdrix, Christine Tasson y Benoît Valiron que ya fue aceptado para el workshop higher-order rewriting que se realizará en Edimburgo el 14 de Julio próximo.
• Finalmente, del 9 al 11 de Junio estuve en Turin en el encuentro CONCERTO-PICS donde presenté el mismo trabajo con Barbara. Proximamente van a poner los slides de todas las charlas en esa página.

Algunas novedades

Bueno, hace mucho que no escribo nada por acá, así que comentaré un poco en qué ando.

• El paper del Scalar Type System lo ampliamos bastante con todas las demostraciones y detalles y estamos a punto de enviarlo a la revista Theoretical Computer Science. Pronto subiré la versión extendida. Aquí está.
• Estuve trabajando en agregar subtyping al Vectorial Type System con Barbara Petit a quién visité hace unos meses y también haciendo muchos cambios a ese sistema de tipos.
• El 18 de Mayo fui a visitar al grupo LAMA en Chambéry, donde dí una charla acerca de este sistema de tipos.
• En agosto voy a Toronto, Canadá a una escuela de verano: Canadian Quantum Information Summer School, lo cual me genera muchas expectativas ya que espero poder ampliar un poco el panorama y tomar algún otro tema en paralelo con el que estoy desarrollando (para no quedarme estancado sólo con esto).

Bueno, esto es un resumen de los últimos meses, ya que he tenido bastante abandonado el blog. Dentro de poco estaré subiendo la versión extendida de Scalar al arXiv (ni bien la enviemos al journal) y pondré un link por aquí (arxiv:0903.3741), y a mi vuelta de Canadá, comentaré un poco de la escuela.

Visita al TypiCal

Los días lunes y martes pasados estuve visitando a Benoît Valiron del proyecto TypiCal en la École Polytechnique de París. Allí dí un seminario (abstract y transparencias aquí) y estuvimos debatiendo con Benoît sobre el trabajo que estoy haciendo.

Fue una muy productiva visita!

Estación de RER donde está la École

Mi hotel estaba a sólo unas cuadras de la torre, así que el martes a la mañana aproveché para ir hasta allí y tomar algunas fotos antes de ir al Laboratorio.

Vectorial, Lógica Lineal y Ortogonalidad

El miércoles y jueves pasados estuve en Lyon, invitado por Barbara Petit del grupo PLUME de la École Normale Supérieure de Lyon. Allí di un seminario sobre los sistemas de tipos que he desarrollado: Scalar, Additive y Vectorial, y algunos de los problemas sobre cómo chequear ortogonalidad entre términos y algunas pistas para resolverlo.

Olivier Laurent se dio cuenta de simplemente ver la presentación, la conexión entre Additive y Intuitionistic Multiplicative Exponential Linear Logic.

Pronto estaré publicando un nuevo paper sobre Additive (con esa conexión a la lógica lineal) y Vectorial. Además, hemos empezado a trabajar juntos con Barbara en el problema de la ortogonalidad, usando subtyping.

Próximos viajes:
Los días 4 y 5 de Mayo voy a París a visitar a Benoît Valiron y Gilles Dowek del proyecto TypiCal, en la École Polytechnique de París, donde daré otro seminario. Luego, el 18 de Mayo estaré en Chambery, donde iremos con mi director, Pablo Arrighi, a participar de una serie de seminarios organizados por Lionel Vaux del grupo LAMA.

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.

Categories, Logic and Foundations of Physics: Los videos

Copio (y traduzco) un post de Bob Coecke en el blog The n-Category Café:

Los videos del 2do workshop Categories, Logic and the Foundations of Physics que se realizó en Londres están disponibles aquí. También hay allí algunas charlas del workshop Logic, Physics and Quantum Information Theory organizado por Prakash Panagaden en Barbados. Desafortunadamente algunas de las charlas no salieron muy bien, por ejemplo la de Peter Selinger "completeness result for dagger compact categories". Esperamos poder compensar esto en el workshop Quantum Physics and Logic que se hará en julio en Islandia. Todos los créditos para Ben Jackson y Jamie Vicary por realizar esta filmación y ponerla online.

La fecha para el próximo workshop "Categories, Logic and the Foundations of Physics", el cual será en Oxford, es el 23 y 24 de agosto - dos días esta vez.

Ese congreso en Islandia es donde presentamos y nos fue aceptado el paper sobre medición y confluencia en lambdas cálculos cuánticos. Lamentablemente por razones económicas no podré ir, así que al menos espero poder ver los videos.

Video de la presentación de Tesis

Lo prometido: el video de la presentación "Agregando Medición al Cálculo de van Tonder". Los créditos para mi hermana y mi novia por la excelente filmación :).

Los slides los pueden bajar de aquí (versión para imprimir), y en unos días subiré el informe de tesis completo (le estoy arreglando algunos detalles que no me gustaron). Dejo un draft.

Obteniendo mi título

Después de una larga ausencia por este blog, paso a contar la causa: Estuve estudiando a full para llegar a recibirme antes de terminar el año.

Y llegó el momento de presentar mi Tesis de Licenciatura en Ciencias de la Computación:

Día y Hora:

Viernes 21 de Diciembre de 2007, 10:45hs

Lugar:

Aula 23, Pellegrini 250, Rosario.
Facultad de Ciencias Exactas, Ingeniería y Agrimensura
Universidad Nacional de Rosario

Título de la tesis:

Agregando medición al Cálculo de van Tonder

Tesista:

Alejandro Díaz-Caro

Director:

Dr. Manuel Gadella

Co-Director:

Dr. Pablo Martínez López

Resumen:

El área de los lenguajes de programación cuánticos se está desarrollando a una gran velocidad. En particular, se han definido varias extensiones al Lambda Cálculo que proveen la sintaxis y semántica necesarias para modelar algoritmos cuánticos.
Uno de los trabajos más influyentes en este sentido es el \lambda_q de André van Tonder[1]. Este es un Lambda Cálculo, definido mediante su semántica operacional, para cómputos puramente cuánticos: la medición no es parte del cálculo.
La intención de este trabajo es agregar medición al \lambda_q, para lo cual nos valemos de algunas herramientas del Lambda Cálculo probabilístico definido por Di Pierro, Hanking y Wiklicky en [2]. Además, siguiendo la línea de trabajo de van Tonder, también hacemos uso de la la sintaxis para la lógica lineal de Philip Wadler[3].

Ref:
[1] A. van Tonder, "A Lambda Calculus for Quantum Computation", SIAM J. Comput. 33(5), Society for Industrial and Applied Mathematics, 1109–1135, 2004
[2] A. Di Pierro, C. Hankin y H. Wiklicky, "Probabilistic Lambda-calculus and Quantitative Program Analysis", Journal of Logic and Computation 15(2), 159–179, 2005
[3] P. Wadler, "A Syntax for Linear Logic", Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics, Springer-Verlag, 513–529, 1994


En algunos días subiré el PDF completo de la tesis y el PDF de la presentación (En otro post).

---

Update: Ya soy licenciado! Dejo algunas fotos (hay más en mi album picasa) y en unos días subiré el video de la presentación en otro post está el video de la presentación.

Antes de empezar, esperando a que llegue el director de escuela.

Abrazos y felicitaciones luego de la presentación.

Una vieja tradición argentina: Los compañeros y amigos ensucian a los egresados con huevos, harina, yerba mate, gaseosa y todo lo que se encuentre a la mano.

La foto de grupo, luego de los huevos. Por algún motivo nadie me quiso abrazar :P

Lambda Cálculo Cuántico

El viernes pasado dí una charla sobre el Lambda Cálculo Cuántico definido por André van Tonder[1] como parte de un ciclo de charlas sobre programación funcional organizadas por el Dr. Pablo E. Martínez López (a.k.a. Fidel).

Dejo las transparencias para quien quiera ver un poco de qué se trata (y también la versión para imprimir), aunque por supuesto, recomiendo recurrir a la fuente.

Ref.
[1] André van Tonder, "A Lambda Calculus for Quantum Computation". SIAM J. Comput. 33, 5 (May. 2004), 1109-1135. (preprint en arXiv)

Video de David DiVincenzo

Acá dejo un video de una charla de David DiVincenzo en el "International Workshop on Measurement-Based Quantum Computing" que se realizó en Oxford entre el 18 y 21 de Marzo pasados. La Charla se titula "The Pioneers of Quantum Computing" (Los Pioneros de la Computación Cuántica) y acá dejo el abstract.

Que lo disfruten.

JAI v.2.0

El día 5 de diciembre próximo, en el Hotel Ariston (Córdoba 2554, Rosario), se realizará la JAI v 2.0 (Segunda Jornada Abierta de Informática) organizada por Sadio Rosario.

«La JAI, en su segunda versión, busca generar un ámbito de exposición académica, y al mismo tiempo, un espacio que reuna inquietudes que incentiven la actualización de los profesionales del sector.»

Junto con Julián Samborski Forlese daremos una charla titulada "Brevísima Introducción a la Computación Cuántica" a las 14:30hs en la Sala Orión. (es la misma charla que dimos hace unos días en las JCC).

Están todos invitados, la entrada es libre y gratuita pero requiere registración previa ya que tienen cupos limitados: http://rosario.sadio.org.ar/jai2.

Edit: Las transparencias de la charla se pueden bajar de aquí.

Charlas Introductorias a la Computación Cuántica

Terminaron las charlas, quería agradecer a Federico Bergero, Mariano Salvetti y Rafael Namías por la ayuda en la organización (y por haber sido los que propusieron el curso), a Guido Macchi, Claudio Gazza y Ariel Dobry por todo el apoyo y a Lucas Minuto por ser el conejito de indias escuchando cada charla antes de que la dicte.

Se puede bajar los apuntes completos de las charlas desde eXactas.org haciendo click acá.