18 de octubre de 2013

Identificando proposiciones isomorfas... en China

(English below)
Del 3 al 7 de Noviembre, se realizará en el State Key Laboratory del Institute for Software de la Chinese Academy of Science, en Beijing, un workshop del projecto Franco-Chino LOCALI. Allí voy a presentar una charla. Les dejo aquí abajo el título y resumen.

Título: Identificando proposiciones isomorfas

Resumen:
En lambda-cálculo tipado, en lenguajes de programación y en teoría de la prueba, dos tipos A y B se dicen isomorfos, si existen dos funciones \phi:A\Rightarrow B y \psi:B\Rightarrow A tales que \phi\circ\psi=Id_A, y \psi\circ\phi=Id_B. En algunos casos, los tipos isomorfos son considerados iguales. Por ejemplo en teoría de tipos de Martin-Löf, en Cálculo de Construcciones y en Deducción módulo, tipos iguales por definición son identificados. Sin embargo, igualdad por definición es mas débil que isomorfismo y, por ejemplo, los tipos isomorfos A\wedge B y B\wedge A usualmente no son identificados: un término de tipo A\wedge B no tiene tipo B\wedge A.
No identificar esos tipos tiene muchos  inconvenientes, por ejemplo si una biblioteca contiene una prueba de B\wedge A, una llamada a una prueba de A\wedge B no podrá encontrarla, si r y s son pruebas de (A\wedge B)\Rightarrow C y B\wedge A respectivamente, no es posible aplicar r a s para obtener una prueba de C, necesitamos explícitamente aplicar una función de tipo(B\wedge A)\Rightarrow (A\wedge B) a s antes de aplicar r a este término. Esto ha llevado a un auge de proyectosde investigación con el objetivo de identificar de una forma u otra tipos isomorfos en teoría de tipos, por ejemplo con el axioma de univalencia.
Aquí introducimos una extensión de lambda cálculo simplemente tipado con pares, donde tipos isomorfos son identificados. En este cálculo nos enfocamos en tres isomorfismos: conmutatividad y asociatividad de la conjunción, y distributividad de la implicación sobre la conjunción. Identificar tipos requiere también identificar términos via una relación de equivalencia, lo cual deriva en un cálculo interesante, relacionado con varios cálculos algebraicos y no deterministas conocidos. En esta charla voy a presentar el sistema y una prueba de normalización basada en una adaptación no trivial de  la técnica de candidatos de reducibilidad. Además, voy a mostrar algunas ideas en progreso para intruducir la currificación: (A\wedge B)\Rightarrow C \equiv A\Rightarrow B\Rightarrow C.


From the 3rd to the 7th of November, a workshop of the ANRI LOCALI Project will take place at the State Key Laboratory of the Institute for Software of the Chinese Academy of Science, in Beijing. I will give a talk there. Below you will find the title and abstract of it.

Title: Identifying isomorphic propositions

Abstract:
In typed lambda-calculus, in programming languages, and in proof theory, two types A and B are said to be isomorphic, if there exists two functions \phi:A\Rightarrow B and \psi:B\Rightarrow A such that \phi\circ\psi=Id_A, and \psi\circ\phi=Id_B. In some cases, isomorphic types are identified. For instance, in Martin-Löf's type theory, in the Calculus of Constructions, and in Deduction modulo, definitionally equivalent types are identified. However, definitional equality is weaker than isomorphism and, for example, the isomorphic types A\wedge B and B\wedge A are not usually identified: a term of type A\wedge B does not have type B\wedge A.
Not identifying such types has many drawbacks, for example if a library contains a proof of B\wedge A, a request on a proof of A\wedge B fails to find it, if r and s are proofs of (A\wedge B)\Rightarrow C and B\wedge A respectively, it is not possible to apply r to s to get a proof of C, but we need to explicitly apply a function of type (B\wedge A)\Rightarrow (A\wedge B) to s before we can apply r to this term. This has lead to several projects aiming to identify in a way or another isomorphic types in type theory, for example with the univalence axiom.
We introduce an extension of simply typed lambda calculus with pairs where isomorphic types are identified. In this calculus we have focused on three isomorphisms: associativity and commutativity of conjunction, and the distributivity of implication over conjunction. Identifying some types requires to also identify some terms via an equivalence relation on terms, leading to an interesting calculus, which is related to several known algebraic and non-deterministic calculi. In this talk I will present the system and a proof of normalisation based on a non-trivial adaptation of the reducibility candidates technique. Also I will show some ongoing ideas to introduce the curryfication: (A\wedge B)\Rightarrow C \equiv A\Rightarrow B\Rightarrow C.


Update: The slides

12 de septiembre de 2013

Estrenándome en Criptografía

Estoy terminando de escribir mi primer paper en criptografía. Aún no lo voy a hacer público (vía arXiv). Primero lo voy a mandar a una conferencia en formato de Resumen Extendido. Después voy a preparar un versión larga para revista, y ahí recién lo voy a hacer público.

Pero ya que ahora estoy como que me puedo tomar un respiro, luego de estar un par de meses totalmente estancado, quiero explicar un poco sobre mi nueva área de investigación.

En concreto, estoy estudiando Protocolos de Cero Conocimiento (Zero-Knowledge Proof). En términos simples, es un juego. Hay dos jugadores, Alice y Bob, y Alice quiere convencer a Bob de que ella sabe algo, e.g., la demostración del Teorema X. Pero Alice le quiere convencer a Bob de que X es correcto sin mostrarle la demostración. La pregunta es ¿Cómo lo hace? ¿Cuál es la estrategia que Alice tiene usar para convencer a Bob?

A primeras, no parece cierto de que algo así sea posible. ¿Cómo voy a convencer a alguien de que algo es cierto, sin siquiera mostrarle que ese algo es cierto? Bueno, de hecho, es posible, y es posible hacerlo para cualquier conjunto en NP (asumiendo ciertas conjeturas de complejidad computacional). También, mostrar que esto es posible y de que es la definición correcta de seguridad, fue lo que valió para otorgar el premio Turing a Shaffi Goldwasser y Silvio Micali este año.

Estos protocolos de cero conocimiento lo que logran es que cualquier adversario, que trate de salirse del protocolo, no lo pueda hacer. Sus aplicaciones están principalmente en el diseño de protocolos criptográficos entre dos o más agentes, e.g., secure multiparty communication.


12 de agosto de 2013

IX Escuela de Verano en Matemáticas Discretas en Valparaíso

Escuela de verano en Matemáticas Discretas en Valparaíso. ¡Para no perderse!

http://discretas2014.cmm.uchile.cl

8 de agosto de 2013

9 de agosto en Rosario: seminario y charla-debate

Mañana 9 de agosto voy a estar dando una charla en la Facultad de Ciencias Exactas, Ingeniería y Agrimensura de la UNR (Aula 27, Pellegrini 250, Rosario). Acá les dejo el título y resumen de la charla:

16hs

Título: Hacia una lógica computacional cuántica
Resumen: El objetivo a largo plazo de esta línea de investigación es definir una lógica computacional cuántica, en el paradigma de pruebas-como-programas. Es decir, queremos una lógica tal que sus pruebas sean programas cuánticos. Con ese propósito, estudiamos varias extensiones al cálculo lambda resaltando diferentes aspectos como la superposición de programas, el no-clonado y las proyecciones no-determinísticas y probabilísticas.


Luego, a las 17hs, tendremos una charla-debate acerca del doctorado y, sobre todo, el después. El título del evento es: ¿Me voy a hacer un doctorado afuera? ¿Y después qué?. Del panel participaremos varios recibidos de la carrera de Ciencias de la Computación de Rosario. Aquí les dejo el link al evento anunciado en Facebook: https://www.facebook.com/events/565382713508343/

23 de julio de 2013

LATIN 2014

La conferencia LATIN toca este año en Montevideo, Uruguay. Esta es la única conferencia en Teoría de la Computación en Latinoamérica, o mejor dicho, la única que se realiza "exclusivamente" en Latinoamérica. Hay otras conferencia que de tanto en tanto se hacen en Latinoamérica como WoLLIC. Además, LATIN abarca todas las áreas de la teoría de la computación.

Siempre LATIN tiene muy buen nivel de presentaciones. Así que es para no perderse. Sin embargo, lastimosamente este año no viene acompañado de una escuela de computación como fue en la edición anterior en Perú.

19 de julio de 2013

Autor se presenta


Hola estimados lectores de Computación cuántica. Es probable que desde un tiempo a esta parte hayan notado mi nombre en la lista de autores.
Con este post quiero develar el misterio y contarles las áreas y los temas de investigación en los cuales trabajo para darles una idea de cuales serán los tópicos que trataré en futuros posts.

Soy doctorando en el Grupo de Lógica y Teoría de la Computabilidad del Dpto. de Computación de la FCEyN-UBA. El objetivo de mi tesis es estudiar aspectos de la computación cuántica y de fundamentos de la física cuántica, desde el punto de vista de la teoría de la computabilidad y la teoría de la aleatoriedad algorítmica.

Mucho más concretamente, actualmente estoy trabajando en dos temas. El primero consiste en la aplicación de la complejidad de Kolmogorov (tanto la clásica como algunas de sus definiciones usando formalismos cuánticos) a la búsqueda de cotas inferiores en query complexity (tanto quantum como randomized).
El segundo tiene que ver con estudiar algunos de los No-go theorems de la cuántica (principalmente Bell y Kochen-Specker) y ver que se puede decir, en términos de computabilidad o de algunas de las nociones de aleatoriedad algorítmica, de la secuencia de resultados de mediciones (codificados apropiadamente con bits) en experimentos certificados por estos teoremas.

En futuros posts daré breves introducciones a estos temas y citare las referencias que acá omití.

¡Saludos!

18 de julio de 2013

A long time ago in a galaxy far far away....

Mi última entrada fue enero. No me gusta dar excusas pero si tengo unas muy buenas.

Primero, mas o menos desde Diciembre 2012 hasta finales de Febrero 2013 estuve exclusivamente trabajando en mi tesis. Para los que ya pasaron por esta etapa conocen bien lo que involucra. Bueno, al final entregué mi tesis y defendí en Marzo de 2013 (aunque ya no recuerdo la fecha exacta). El enlace de descarga lo pueden encontrar aquí. Me gusta decir que mi tesis (o disertación para algunos) está divida en dos partes: 1) Algoritmos y 2) cotas inferiores. Esas son las dos grandes partes en que podríamos dividir el área de circuit complexity. En la primera parte estudié una técnica de construcción de algoritmo llamada quantum walks, tema sobre el cual discutí aquí. La segunda parte consistió en un estudio sobre una técnica muy común para probar cotas inferiores de algoritmos llamada communication complexity el cual también lo discutí aquí. La tesis también tiene un conjunto de apéndices que se puede utilizar para empezar a estudiar estos temas, por si a alguien le interesa. En particular, hay una demostración del Yao's Minimax Lemma para algoritmos Montecarlo que no aparece en ningún otro lado. En el paper original de Yao, no aparece tal demostración, aunque el autor dice que no es difícil. Aunque es cierto que no es, me hizo pensar bastante para poder demostrar.

Segundo, después de mi graduación, empecé inmediatamente a trabajar de postdoc en la Universidad de Fukui bajo la supervisión de Tomoyuki Yamakami. Mi proyecto de investigación está principalmente en Teoría de Complejidad Computacional Estructural, con énfasis en sistemas de pruebas interactivos y criptografía que toca aspectos de computación clásica y cuántica. Este es un proyecto financiado por la Japan Society for the Promotion of Science (JSPS) del cual yo soy actualmente fellow. Apenas llegué en Abril estoy trabajando en este proyecto y al mismo tiempo empezando a manejar estudiantes y organizar seminarios.

Algo muy cierto que uno no se da cuenta cuando es estudiante es que todo lo que tus profesores te cuentan que sucederá una vez te gradúes es cierto. Ahora estoy mucho más ocupado que antes y como estoy en un proyecto de investigación tengo que si o sí tener resultados en forma periódica y en corto plazo. Esto pone bastante presión, algo que tenía muy poco cuando era estudiante. En particular, ahora que soy un investigador independiente, tengo que manejar mi propio presupuesto, lo cual implicar escribir propuestas de investigación para pedir financiamiento. Porque sin eso, literalmente , no se puede hacer nada, nada de viajes, nada de libros, etc. Ahora tengo que pensar en todo eso, lo cual no me preocupaba en mi época de estudiante. Por suerte no tengo que estar dando clases, lo cual también puede cambiar en cualquier momento. Por lo tanto, voy a aprovechar el tiempo que tengo ahora.

Pero en síntesis, es un buen cambio, y es un tipo de vida al que todos los que pretendemos hacer la carrera de científicos deberíamos saber manejar.

Bueno, voy a empezar a ponerme las pilas para mantener el ritmo de publicación que tenía en el blog. Tengo un paper que estoy por subir al arXiv y de a poco voy a ir contando sobre mis proyectos de investigación actuales apenas empiece a tener cosas sobre las que pueda compartir en público.

9 de julio de 2013

La probabilidad de los sistemas no-confluentes

El paper que comenté en el post "Escapando al no-determinismo" fue aceptado en el 9no workshop internacional "Developments in computational models", un workshop de un día que este año se hace por primera vez en Argentina (primera vez fuera de Europa!).

El programa del workshop ya está publicado online.

Los detalles del paper lo pueden ver en el post anterior, donde también dejé un link al paper, y la versión completa con todas las pruebas.

Nos vemos en Buenos Aires.

9 de junio de 2013

¿Cómo hacer un máster o un doctorado en Europa?

Introducción
En realidad el título de este post es demasiado abarcativo, y me lo permito ya que este post no es un texto científico y creo que este título atraerá a más gente, a quienes también les puede ser útil. Si quisiera ser más preciso, debería titularlo así: "Algunos consejos sobre como conseguir hacer un máster o doctorado en Francia, habiendo cursado la licenciatura en Argentina". Por supuesto pretendo que estos consejos le sirvan más que sólo a los argentinos (la mayoría de los países latinoamericanos tienen sistemas educativos más o menos similares (más allá de la cuestión de gratuidad de la educación, condiciones de ingreso y demás)), y más que sólo para venir a Francia (Europa tiene un estandar en educación superior por lo que el sistema es similar en muchos países). De todas maneras, estas notas salen de mi experiencia personal y por eso puedo hablar sólo de ella. Invito a todo el que quiera a dejar comentarios para ampliar, corregir o mejorar esta guía. Es más, si alguien quiere publicar algo similar, pero más orientado a su país de residencia, les agradecería mucho y podemos poner un "post invitado".

Bueno, hechas las introducciones, comencemos.

Qué es un máster y qué es un doctorado en Europa?
En Argentina, el modelo tradicional es la licenciatura de 5 años con posibilidad luego de hacer un máster de uno o dos años o se puede comenzar directamente el doctorado después de la licenciatura, sin necesidad de máster. Hay algunas excepciones como las licenciaturas en matemática de 4 años, que necesitan uno o dos años de máster antes de acceder al doctorado.

En Europa, en cambio, el sistema es así: licenciatura de 3 años (se les suele llamar licencia 1, 2 y 3), máster 1 y máster 2, y luego el doctorado. Para hacer el doctorado en general es indispensable haber terminado el máster 2 (se pueden dar excepciones con una autorización especial, pero vamos a lo que es más común).

En particular, en Francia, hay un sistema paralelo al de L1L2L3M1M2 que es el de las escuelas de ingenieros (que no necesariamente tiene relación con lo que se entiende por "ingeniería" en el resto del mundo). En una escuela de ingenieros, uno accede si tiene muy buen resultado en el "Bac" (examen nacional que se toma al finalizar el secundario para poder ir a la universidad) y luego de dos años de preparación, tienen que pasar un examen para hacer los 3 años restantes en la escuela de ingenieros (total: 5 años como en Argentina). Quienes no pasen ese examen, son admitidos en L3 en una universidad (las universidades, contrariamente a las escuelas de ingenieros, son de libre acceso (o casi, también hay una postulación a hacer, pero no viene al caso)).

A la escuela de ingenieros sólo se puede acceder de esa manera. Por el contrario, para el máster 1 o 2, se puede acceder de muchas formas, incluso habiendo realizado la licenciatura en otro lugar del mundo. Normalmente debería bastar con tener hasta 3er año aprobado, ya que es el equivalente a L3 aquí, el único problema es que en Argentina en general no tenemos un diploma hasta finalizar el 5to año (con algunas excepciones de títulos intermedios que pueden ser muy útiles a la hora de postular en Europa).

Durante el máster en Europa se hace un período de pasantía: si es un máster "pro" (profesional), será una pasantía en alguna empresa, si es un máster "recherche" (investigación), será en un grupo de investigación. En ambos, M1 y M2, se escribe una tesis o informe final. En el M2 (al menos el de investigación) se debe defender la tesis frente a un jurado de profesores. Es el equivalente de nuestras tesis de licenciatura.

Dicho esto, al doctorado se puede acceder habiendo completado una licenciatura de 5 años con tesis, no es necesario un máster para acceder, ya que la licenciatura de 5 años con tesis es completamente equivalente al máster 2 en investigación. Este es un punto que mucha gente no sabe, y vienen de latinoamérica con una licenciatura terminada, y creen que es equivalente a una licence francesa, por lo que arrancan con el máster en lugar de apuntar al doctorado. No es que esté mal: un máster se hace en uno o dos años, y da un título más que puede ser muy valorado a la hora de buscar un trabajo... es sólo que no es necesario si se quiere seguir en la academia.

Comparación entre el sistema argentino y el francés

También se puede venir aquí a hacer una pasantía (donde se escriba la tesis de licenciatura argentina por ejemplo). La elección está en uno. Sabiendo a qué corresponde la licenciatura argentina, uno puede elegir dónde quiere arrancar en el sistema francés, de acuerdo al título obtenido.

Dónde buscar
Las listas de correo son una fuente infinita de ofertas de pasantía y doctorados. Si les interesa un tema en particular, traten de buscar una lista de correo internacional sobre dicho tema, y seguro habrá ofertas cada tanto.

Otra manera de conseguir dónde hacer un doctorado o pasantía, es enviar emails a grupos de investigación que estén trabajando en los temas de sus intereses (Google is your friend!). De hecho, de esa manera obtuve yo mi posibilidad para hacer el doctorado en Francia. Estaba interesado por la computación cuántica desde hacía tiempo, así que empecé a enviar mails (formales), con mi CV y mis intenciones de hacer doctorado a varios investigadores y grupos del mundo entero. Así uno me recomendó a otro, y luego a otro, hasta que finalmente fui a dar con quien luego fue mi director de tesis.

En los dos párrafos anteriores no mencioné el máster, porque en general para el máster la cosa es un poco diferente. Recuerden que un máster no es otra cosa que los últimos años del equivalente a la licenciatura argentina. Una manera de buscar másters para hacer en Francia, es el sitio de Campus France. Allí encontrarán información sobre todas las ofertas educativas en Francia. El sitio puede marear un poco, pero toda la info necesaria está allí.

Idioma
Para un doctorado en Francia (y generalmente lo mismo sucede con las pasantías), no es necesario conocer francés, aunque van a terminar aprendiéndolo luego de 3 años de doctorado, claro está. Lo que sí es indispensable es saber inglés. Un nivel de inglés que les permita comunicarse en el día a día. Para los másters en cambio, depende de la universidad. Algunas piden certificación de idioma francés. Otras piden al menos inglés, y otras no piden nada directamente. Esa información deberían buscarla en la página de la universidad a la que estén postulando.

CV
No voy a hacer aquí una guía de cómo hacer un CV, sólo quiero dar un consejo. Argentina y Francia entienden de manera completamente diferente lo que es un CV. En Argentina el CV lleva información de TODO, incluyendo cursos a los que se han asistido, seminarios, incluso congresos, aunque no se haya presentado trabajos, sino sólo como oyente. En Francia eso no existe. Un CV francés tiene típicamente una sola página, donde se detalla la formación académica y los títulos obtenidos (no hay necesidad de mencionar el jardín de infantes, con los títulos universitarios es suficiente), si hicieron tareas docente, pasantías, visitas académicas, también está bien ponerlo. Sólo será bien visto que pase de una página, si tienen muchas publicaciones o participación en congresos (presentando trabajos) que lo justifiquen, lo cual no es muy común al finalizar una licenciatura, ni nadie estará esperando algo así, por lo que las eventuales publicaciones que tengan deberían encajar bien en esa página. Si les cuesta mucho resumir el CV, pueden llegar a considerar pasar a dos páginas, pero absolutamente nunca más que eso. Busquen en google CVs franceses y verán lo que les estoy diciendo.

Carta de motivación y recomendación
Algo importante en Francia son las cartas de motivación y de recomendación. La carta de motivación es simplemente una presentación personal, diciendo qué es lo que estás pidiendo (hacer un doctorado con ellos por ejemplo), porqué te interesa ese grupo en particular, y qué creés que podés aportar vos a ese grupo. Traten de no hacer una oda a ustedes mismos, ni una oda al grupo. Tiene que tener un buen balance. Hay cientos de sitios con consejos de cómo escribir una carta de motivación. Tengan en cuenta que una carta de motivación para Estados Unidos no es necesariamente lo mismo que una carta en Europa. Aquí no se estila poner muchas cosas personales de tipo emotivo, en cambio en Estados Unidos he visto cartas de ese tipo.

Carta(s) de recomendación. La idea es que algún profesor que los conozca bien, pueda escribir una carta diciendo cómo los conoció, y la opinión que tiene de ustedes. Eso viene un poco a suplir la falta de espacio en el CV. Yo creo que la idea es que el CV sea conciso, y luego tener la opinión de alguien que los conoce, en lugar de tener que leer un CV de 100 páginas. Por supuesto, mientras más conocida en el ámbito académico sea la persona que escribe la carta, mejor. Un detalle. En Francia se estila lo siguiente: si un profesor no quiere escribirte una carta, en general no va a decir que no, pero te va a escribir una carta de recomendación de una página. Se considera normalmente que una carta debería tener dos páginas. Tan es así, que a veces lo que escribieron no sobrepasa la página, y entonces hacen cosas como poner un encabezado muy grande y comenzar la carta a mitad de la página, para que termine en la segunda. Así que si le piden una carta de recomendación a un profe conocido de la facu, y él no sabe esta "regla" tácita, coméntensela. Otra cosa que se estila mucho es en lugar de enviar la carta, dar los datos de contacto de esa persona para que ellos, si están interesados, les pidan una carta de recomendación. En cualquier caso, los datos de contacto de la persona que recomienda, deben estar disponibles.

Para finalizar
En Europa siempre se está buscando buenos estudiantes. No hay que ser tímidos, las universidades argentinas preparan a los estudiantes de una forma excelente, la única falla es que nos falta saber cómo conseguir para hacer un doctorado en el exterior (cosa que los hindúes y chinos saben muy bien hacer).

La oportunidad de hacer un doctorado, pasantía o máster en el exterior es algo que todos deberían considerar. No porque en Argentina no sean buenos los programas (al contrario, son excelentes), sino porque salir a ver cómo se hacen esas cosas en otros lugares, enriquece no sólo a la persona que tiene la experiencia, sino también a la comunidad a la que esa persona vuelva luego de sus estudios. Aquí en Francia tienen eso muy presente, y es por eso que es muy difícil conseguir un puesto permanente en una universidad sin haber hecho al menos un postdoc en el extranjero.

Espero les sirva, y dejen comentarios con cualquier duda que con gusto responderé lo que esté a mi alcance.

31 de mayo de 2013

Juan Pablo Paz en "Desde la ciencia"

Les dejo una entrevista a Juan Pablo Paz, un físico de la Universidad de Buenos Aires, reconocido mundialmente por sus trabajos en el fenómeno de la decoherencia.

24 de mayo de 2013

Escapando al no-determinismo

Mis disculpas por el "silencio de radio" que se ha visto últimamente en este blog. He estado terminando con los cursos donde debía dar clases, postulando para obtener financiación para el año próximo, y terminando algunas investigaciones.

Hoy enviamos con Gilles Dowek un resumen extendido a un workshop. Desde que me doctoré he estado trabajando en cálculos y lógicas no-deterministas, pero el objetivo siempre fue, y sigue siendo, no perder de vista la computación cuántica. Un primer paso, es pasar del no-determinismo a algo un poco más controlado: probabilístico (ya habrá tiempo más adelante para ir hacia un paso superior que es el caso cuántico).

En este trabajo mostramos una forma genérica de convertir un sistema de reescritura no-determinístico abstracto en un sistema probabilístico, y luego lo aplicamos a λ+, un cálculo lambda no-determinístico que desarrollamos anteriormente.

Lo que hacemos aquí es definir una medida de Lebesgue en el espacio de trazas de ejecución del sistema. La idea es definir cajas (boxes) que determinan ciertas trazas, y dejan las otras libres. De esa manera podemos definir fácilmente una medida sobre esas cajas, y luego extenderlo a cualquier ejecución mediante un recubrimiento por cajas.

El preprint puede descargarse de aquí: probas.pdf

Update: El paper fue aceptado en DCM. Más info aquí.

22 de marzo de 2013

Tipos vectoriales, no-determinismo y sistemas probabilísticos: Hacia una lógica cuántica computacional

Les dejo los slides de una charla que di ayer en una jornada de cuántica en Nancy. Lo que presento es en general mi tema de investigación, la diferencia con mi charla anterior, es que el público aquí eran mayormente informáticos especialistas en computación cuántica, mientras la charla anterior estaba destinada a matemáticos sin conocimientos en computación cuántica. Por lo tanto, aquí doy algunos detalles más (ya que no tuve que introducir el tema, ni explicar qué es lambda-cálculo).


Aquí les dejo también el link directo al PDF

4 de febrero de 2013

Computación cuántica, lambda-cálculo, lógica... y todo eso

Este año estoy trabajando en un centro INRIA y dando clases en la Universidad Paris-Ouest, integrando un grupo de matemáticos. Yo soy informático teórico, no matemático, y es por eso que la investigación la hago en el INRIA.

La semana pasada, dí una charla para el grupo de la universidad. La idea era dar un panorama general de qué es lo que investigo. Dado que el público no conocía computación cuántica, lambda-cálculo, ni nada de los temas que yo trabajo en general, la charla se trató de hacer una introducción a todos esos temas y luego contar un poco, de forma bastante genérica, dónde entrarían mis temas de investigación actuales.

Este post es simplemente para dejarles los slides por si a alguno le interesa. Claro que arriba de los post también hablé, por lo que faltarán detalles. Pero si alguno de los lectores de este blog está interesado en saber un poco de qué se trata todo eso de cuántica, lambda-cálculo y lógica, pues aquí va.


Aquí les dejo también el link directo al PDF

29 de enero de 2013

Emalca Salta 2013

Saliendo un poco del letargo de los últimos meses donde he estado inmerso en escribir mi tesis, esta entrada la escribo para promocionar la escuela EMALCA 2013 en Salta, Argentina.


Yo he participado en la edición 2005 que se llevó a cabo en Paraguay. Los cursos son de diferentes niveles y para todos los gustos. En esta edición me llama la atención el curso sobre Cadenas de Markov, uno de mis eternos temas favoritos.

Espero que a algún lector le parezca interesante y decida ir.

3 de enero de 2013

LFCS @ San Diego

Este sábado salgo para San Diego, California, EE.UU. para participar del Simposio sobre Fundamentos Lógicos de las Ciencias de la Computación (Symposium on Logical Foundations of Computer Science, LFCS). Allí fue aceptado el paper que escribimos con Giulio Manzonetto y Michele Pagani y que comenté rápidamente en este post. A la vuelta les comento sobre el simposio y dejo mis slides de la presentación. El paper saldrá salió publicado en el volume 7734 de LNCS, y, como siempre, pueden también bajarlo libremente desde mi página web. Les dejo el título y abstract en inglés:
Call-by-value non-determinism in a linear logic type discipline
We consider the call-by-value λ-calculus extended with a may-convergent non-deterministic choice and a must-convergent parallel composition. Inspired by recent works on the relational semantics of linear logic and non-idempotent intersection types, we endow this calculus with a type system based on the so-called Girard's second translation of intuitionistic logic into linear logic. We prove that a term is typable if and only if is converging, and that its typing tree carries enough information to give a bound on the length of its lazy call-by-value reduction. Moreover, when the typing tree is minimal, such a bound becomes the exact length of the reduction. 
Update: Aquí les dejo los slides que usé en la presentación, y el link al paper en la página de Springer (y les repito el link al PDF que se puede descargar desde mi página web sin necesidad de pagarle a Springer).
El simposio estuvo interesante en general, aunque quizá demasiado orientado hacia justification logic para mi gusto.