A System F accounting for scalars @ LMCS

(Abajo en Español)

My first journal paper has been finally published. It is entitled A System F accounting for scalars and co-authored with Pablo Arrighi.

Before commenting about the paper itself, I want to highlight that it has been published by the journal Logical Methods in Computer Science, a high-class, peer-reviewed, open-access, free journal, published under the Creative Commons licence. This journal is managed by leader researchers in theoretical computer science (in particular, in logic), without any private editorial intervening. Why I want to point out these details? Because it is a living proof that researchers can do a pretty good job, without the need of enterprises such as Elsevier. And more importantly, it is a proof that science can be open!

Regarding to the paper, I have commented about it in this blog several times. The journal version of it, means that it has been extended to all its details, improved the motivations of it, and the reviewers have carefully read and made suggestions of how to improve the proofs and the text in general. This paper presents a type system for the linear-algebraic lambda-calculus, an extension of lambda-calculus that considers linear combination of terms, as terms. Such type system keep track of the amplitudes of the linear combination, to the point that it can be used to define a probabilistic type system.

---

Mi primer artículo en revista ha sido finalmente publicado. Se titula A System F accounting for scalars (Un Sistema F que considera escalares) y lo escribimos en conjunto con Pablo Arrighi.

Antes de comentar sobre el paper en sí, quiero resaltar que ha sido publicado por la revista Logical Methods in Computer Science (Métodos Lógicos en Ciencias de la Computación), una revista de alta calidad, con revisión por pares, la cual es gratis y de acceso libre, publicada bajo licencia Creative Commons. Esta revista es llevada a cabo por investigadores líderes en ciencias de la computación (en particular, en lógica), sin la intervención de ninguna editorial privada. Porqué quiero resaltar esos detalles? Porque es una prueba viviente de que los investigadores pueden hacer un muy buen trabajo, sin necesidad de empresas como Elsevier. Y más importante, es una prueba de que la ciencia puede ser abierta!

Con respecto al paper, he comentado sobre él en este blog varias veces. La versión para revista del mismo, significa que ha sido extendido a todos sus detalles, justificado mejor, y los revisores de la revista lo han leído cuidadosamente y marcado sugerencias de cómo mejorar las pruebas y el texto en general. El paper presenta un sistema de tipos para el cálculo lambda algebraico lineal, una extensión al cálculo lambda que considera la combinación lineal de términos, como términos. Tal sistema de tipos lleva un seguimiento de las amplitudes de las combinaciones lineal, al punto de poder ser usado para definir un sistema de tipos probabilístico.

TAMC 2012

La conferencia Theory and Applications of Models of Computation (TAMC'12) de este año ya publicó su lista de papers aceptados. Solo hay un paper en algo cuántico, y resulta que es mi paper que ya había explicado aquí.

Esta es una conferencia general de teoría, y abarca todas las áreas de ciencias de la computación (teórica). La conferencia va estar muy interesante, ya que forma parte de los festejos por los 100 años de Alan Turing. La lista de conferencistas para esta celebración incluye a Andrew Yao, John Hopcroft, Richard Karp, Jon Kleinberg, Butler Lampson, y otros. Todos son respetados científicos del área y varios de ellos poseedores del premio Turing. Así que, la conferencia va a estar muy linda. Y Beijing será un lugar muy interesante para visitar.

Sin embargo, primero tengo que ir a Beijing en marzo. Voy a darme un paseo por la Universidad de Tsinghua (la universidad más grande e importante de China), y la Academia de Ciencias de China.

12th Canadian Summer School on Quantum Information

De vuelta este año se hace la escuela canadiense en información cuántica. Quienes estén interesados, tienen tiempo hasta el 14 de mayo para registrarse. También hay apoyo financiero para participantes.

Alejandro y yo ya estuvimos en otras ediciones como lo pueden ver aquí y aquí.

Carta de John Nash

John Nash es uno de los matemáticos más importantes en nuestros días. Su principal contribución fue el descubrimiento del teorema del equilibrio para juegos de suma-cero allá por los años 50. Ese trabajo le valió el premio Nobel en economía en 1994.

Sus trabajos tienen mucha influencia hoy en día en ciencias de la computación por sus aplicaciones en un área relativamente nueva, Teoría de Juegos Computacional. En esta área Noam Nisan es uno de los principales científicos. En realidad Nisan hizo contribuciones seminales en varias áreas de ciencias de la computación.

Sucede que Noam Nisan tiene un blog, y allí hizo un anuncio bastante sorprendente. John Nash había enviado una carta a la NSA (National Security Agency) de USA en 1955 con la intención de que se interesen en una máquina de encriptación que había diseñado. En esa carta, Nash, escribió sobre sus trabajos en teoría de juegos, y mencionó también sus ideas sobre como construir protocolos criptográficos basados en la dificultad de problemas computacionales. Nash había anticipado, en 1955, ideas que recién se realizarían más o menos 20 años después, en lo que conocemos como criptografía moderna. También había anticipado en 1 año la pregunta que hizo Gödel a Von Neumman en otra famosa carta.

Nash básicamente ya estuvo pensando en preguntas que hoy corresponden a la teoría de complejidad computacional antes de su establecimiento, más o menos unos 10 años antes. Simplemente me parece increíble. Nash siempre fue considerado un matemático extraordinario, pero esto es realmente sorprendente. Cuando uno lee un libro de complejidad computacional, siempre los autores hacen referencia a la carta de Gödel. Pero ahora creo que vamos a tener que agregar a otro personaje en esta historia.

Quantum Programming Languages in South Brazil

The main focus of our work is the development of high-level quantum programming languages. More specifically, we work with the design and semantics of functional quantum programming languages. Basically, we start with simple-typed lambda calculus. Then, on top of that we add a non-deterministic monad for quantum parallelism, and finally we add arrows for quantum measurements. The work has a more theoretical flavour in the investigation of the categorical models and also has a more practical flavour in the use of the language for the investigation of quantum algorithms. We have a prototype implementation of the language in Haskell. Our first motivation is to try to understand quantum computing using well known models and tools normally used in the design and semantics of traditional (not quantum) functional programming languages. Second, we hope our work can approximate the computer science (and informatics in general) community to quantum computing. We hope that for a cs student would be easier to understand quantum computing and to develop quantum algorithms using a high-level quantum programming language than to use quantum circuits or linear algebra. Of course this is a under development work and there are many things to be done still, as higher-order, high-level quantum data structures, quantum algorithms, etc.
Nowadays, we work at Federal University of Santa Maria (UFSM) in the South of Brazil, where we have undergraduate courses and also a cs master course.
Here one can find some of our publications.