Escuelas, conferencias, y otras cosas

Hace mucho que debería haber escrito esta entrada, pero simplemente luego de mi viaje a Canadá se me acumuló un montón de trabajo.

Primero, la escuela canadiense en computación cuántica: 11th Summer School on Quantum Information. En general, estuvo  genial! Los profesores eran todos investigadores reconocidos en su especialidad. En el área de ciencias de la computación cuántica tengo que destacar a Michele Mosca, Andrew Childs, Gilles Brassard, Renato Renner, y Daniel Gottesman. Todas sus clases estuvieron fabulosas. Las otras clases eran en teoría de la información, las cuales entendí regularmente bien, y en física, esto último más o menos. Fueron 2 semanas muy buenas en donde pude conocer gente de todo el mundo, y con quien pude hablar sobre computación cuántica con libertad, sin tener que explicar los porques ni dar razones de su estudio. Simplemente directo al asunto. En este enlace se pueden encontrar las notas de curso de todas las clases. El próximo año va a ser en IQC, uno de los mejores lugares del mundo para estudiar la materia.

Segundo, en agosto 23-27 se realiza AQIS 2011 en Busan, Korea. Voy a estar dando una presentación allí sobre el mismo tema que presenté en la escuela. El título del trabajo es: Quantum Query Complexity of Hamming Distance Estimation. Ya estaré subiendo una versión del paper en mi página web personal y arXiv.

Por último, estuve colaborando con Stasys Jukna en la correción (proofread) de su último libro que estará publicándose muy pronto. Solo leí 4 capítulos, pero está increíble! Sin duda será un éxito. Stasys tiene otro libro que es una joya en combinatorica: Extremal Combinatorics with Applications in Computer Science. Lo tengo aquí mismo, y siempre lo estoy consultando para cualquier problema que tenga. Recomiendo ese libro a cualquiera que esté interesado en cotas inferiores para algoritmos.

Mi interés está principalmente en técnicas de cotas inferiores para dos modelos de computación cuántica: árboles de decisión y protocolos de comunicación. Mis últimos trabajos estuvieron básicamente en la aplicación de técnicas conocidas a problemas específicos. Pero ahora quisiera realmente intentar desarrollar una técnica nueva en communication complexity. Para ello, estoy estudiando tensor rank. Quiesiera hacer mención de un muy lindo paper sobre esto que aparareció en el último CCC 2011: Tensor Rank Some Lower and Upper Bounds (arXiv:1102.0072). Además tiene un apéndice que explica muy bien varias propiedades de los tensores.

Postdoc: Proyecto ALAL

Como anuncié en un post anterior, se aproxima mi defensa de tesis: el 23 de Setiembre. A partir de Octubre comenzaré un postdoc en la Université de Paris-Nord (Paris XIII), un proyecto financiado por DIGITEO y la región Île-de-France. El responsable del proyecto de Michele Pagani, del Laboratoire d'Informatique de Paris Nord y el socio Gilles Dowek, director de uno de los 5 dominios de investigación del INRIA.

Título del proyecto: 

ALAL: Algebraic approaches to lambda calculi

(Métodos algebraicos para cálculos lambda)

No voy a poner el proyecto entero acá, pero dejo el resumen corto (abajo la traducción al español)

The project focuses on formal foundations for language-based (especially static) techniques guaranteeing resource-related runtime properties of programs. The project belongs to the research area whose aim is to associate to a program a certification assuring some specific properties. We will derive the tools and techniques for our investigation from the field of logical proof-theory and semantics, with special interest in linear logic and λ-calculus. In particular, we will explore the new interactions between linear algebra and the formal methods approach to computation, recently arisen from the differential extension of linear logic and the algebraic λ-calculi. The expected result is a robust theoretical framework in which to develop static analysis and verification tools for non-deterministic paradigms, such as stochastic systems, concurrent computation, quantum programming, etc.

Y aquí una traducción:

El proyecto se centra en los fundamentos formales de las técnicas basadas en lenguaje (sobre todo estáticas) que garantizan propiedades de ejecución de los programas relacionadas con recursos. Este proyecto pertenece al área de investigación cuyo objetivo es asociar a un programa una certificación que garantice ciertas propiedades. Vamos a derivar las herramientas y técnicas de nuestra investigación del campo de la teoría de la demostración lógica y de la semántica, con especial interés en lógica lineal y cálculo lambda. En particular, vamos a explorar las nuevas interacciones entre álgebra lineal y enfoques de métodos formales recientemente surgidos a partir de la extensión diferencial de lógica lineal y de los cálculos lambda algebraicos. El resultado esperado es un framework sólido en el cual desarrollar herramientas de análisis estático y verificación para paradigmas no-determinísticos como sistemas estocásticos, computación concurrente, computación cuántica, etc.

LSFA (y QuAND!)

Con Pablo Buiras, a quien estoy dirigiendo en su tesis de licenciatura (el equivalente a la tesis de master en el sistema de la Unión Europea) y Mauro Jaskelioff, su codirector, hemos escrito un paper basado en la tesis de Pablo, que fue aceptado en LSFA 2011. Será Pablo quien lo presente allí.

El paper aborda el problema de la confluencia del lambda cálculo algebraico lineal por medio de un sistema de tipos (el cual permite sólo términos fuertemente normalizables, lo que en conjunto con la confluencia local, nos da la confluencia del lenguaje). Este sistema de tipos puede verse como una extensión de Additive al cálculo completo o como una simplificación de Vectorial. Tiene la ventaja de que, al igual que Additive, sólo introduce sumas en los tipos, y no escalares como lo hace Vectorial, lo cual lo haría mucho más complejo y difícil de interpretar en otros sistemas conocidos. Además, da información aproximada de qué es lo que está pasando en el término: por ejemplo, si tenemos un término 2.1 M + 1.5 N donde M tiene tipo T y N tipo R, el tipo de esta combinación lineal de términos será T+T+R, dicho de otro modo, el tipo "aproxima las cantidades" de términos de cada tipo que están presentes en la combinación, tomando su parte entera.

El paper completo (el borrador, claro, aún tenemos tiempo para enviar la versión definitiva) lo pueden bajar de acá. Y el lunes pasado presenté el trabajo (con un cambio, ya que en mi presentación la normalización fuerte la derivo a partir de la normalización fuerte de Vectorial) en el encuentro del proyecto QuAND. Los slides de esa presentación están acá.

La versión definitiva del paper será publicada en el Electronic Proceedings in Theoretical Computer Science, una revista científica electrónica que suele publicar los anales de workshops y conferencias, y que tiene la particularidad de ser abierta: cualquiera puede descargarse sus artículos, no hace falta pagar por ello.

Update 25/03/12: Los proceedings del workshop han aparecido. Pueden bajar la versión publicada del paper desde aquí.