Les dejo los detalles originales en inglés y debajo la traducción.
A type system for the vectorial aspects of the linear-algebraic lambda-calculus
(joint work with Pablo Arrighi and Benoît Valiron)
We describe a type system for the linear-algebraic lambda-calculus. The type system accounts for the part of the language emulating linear operators and vectors, i.e. it is able to statically describe the linear combinations of terms resulting from the reduction of programs. This gives rise to an original type theory where types, in the same way as terms, can be superposed into linear combinations. We show that the resulting typed lambda-calculus is strongly normalizing and features a weak subject-reduction.
Un sistema de tipos para los aspectos vectoriales del lambda cálculo algebraico lineal
(trabajo en conjunto con Pablo Arrighi y Benoît Valiron)
Describimos un sistema de tipos para el lambda cálculo algebraico lineal. El sistema de tipos tiene en cuenta la parte del lenguaje que emula operadores lineales y vectores, o sea, es capaz de describir estáticamente las combinaciones lineales de términos resultantes de la reducción de los programas. Esto conduce a una teoría de tipos original donde los tipos, de la misma manera que los términos, pueden ser superpuestos en combinaciones lineales. Mostramos que el cálculo tipado resultante tiene normalización fuerte y una versión débil de la propiedad de conservación de tipo.
Versión oficial de 12 páginas (preprint)Versión completa con todas las pruebas en apéndice
Update (05/07/11): Aquí están los slides que presenté durante el workshop.
Update (31/07/12): Finalmente el paper está online (y es de libre acceso): EPTCS.
0 comments:
Publicar un comentario