27 de febrero de 2012

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.