A Type System for the Vectorial Aspect of the Linear-Algebraic Lambda-Calculus

Pablo Arrighi 1, 2 Alejandro Díaz-Caro 3, 4 Benoît Valiron 4, 5
1 LIP - Laboratoire de l'Informatique du Parallélisme
2 CAPP
LIG - Laboratoire d'Informatique de Grenoble
3 LIG - Laboratoire d'Informatique de Grenoble
4 LIPN - Laboratoire d'Informatique de Paris-Nord
5 CIS - Department of Computer and Information Science [Pennsylvania]
Abstract : 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.
Type de document :
Communication dans un congrès
Elham Kashefi and Jean Krivine and Femke van Raamsdonk. DCM - 7th International Workshop on Developments of Computational Methods - 2011, Jul 2011, Zurich, Swaziland. Open Publishing Association, 88, pp.1-15, 2012, Electronic Proceedings in Theoretical Computer Science. 〈10.4204/EPTCS.88.1〉
Liste complète des métadonnées
https://hal.inria.fr/hal-00924926
Contributeur : Alejandro Díaz-Caro <>
Soumis le : mardi 7 janvier 2014 - 12:09:09
Dernière modification le : mardi 24 avril 2018 - 13:52:47

Lien texte intégral

arxiv

Identifiants

Collections

LIG | LIG_MFML_CAPP | LIG_MFML | INRIA | LIP | ENS-LYON | UNIV-PARIS13 | UGA | LIPN | USPC | LIG_SRCPR | UNIV-LYON1

Citation

Pablo Arrighi, Alejandro Díaz-Caro, Benoît Valiron. A Type System for the Vectorial Aspect of the Linear-Algebraic Lambda-Calculus. Elham Kashefi and Jean Krivine and Femke van Raamsdonk. DCM - 7th International Workshop on Developments of Computational Methods - 2011, Jul 2011, Zurich, Swaziland. Open Publishing Association, 88, pp.1-15, 2012, Electronic Proceedings in Theoretical Computer Science. 〈10.4204/EPTCS.88.1〉. 〈hal-00924926〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

176

Contact


archive-ouverte@inria.fr