The vectorial λ-calculus

Volver a la Vista simple
dc.conicet.fuenteindividual
dc.conicet.organizacionAix-Marseille Université
dc.conicet.organizacionCentre National de la Recherche Scientifique
dc.conicet.organizacionConsejo Nacional de Investigaciones Científicas y Técnicas
dc.conicet.organizacionUniversidad Nacional de Quilmes. Departamento de Ciencia y Tecnología
dc.conicet.organizacionUniversité Paris Sud
dc.conicet.organizacionCentre National de la Recherche Scientifique
dc.conicet.organizacionUniversité Paris-Saclay
dc.conicet.paisOrganizacionFrancia
dc.conicet.paisOrganizacionFrancia
dc.conicet.paisOrganizacionArgentina
dc.conicet.paisOrganizacionArgentina
dc.conicet.paisOrganizacionFrancia
dc.conicet.paisOrganizacionFrancia
dc.conicet.paisOrganizacionFrancia
dc.conicet.produccionid6372131
dc.contributor.authorArrighi, Pablo
dc.contributor.authorDíaz Caro, Alejandro
dc.contributor.authorValiron, Benoît
dc.date.accessioned2019-03-26T15:36:34Z
dc.date.available2019-03-26T15:36:34Z
dc.date.issued2017-06
dc.date.updated2019-03-26T13:49:01Z
dc.description.abstractWe describe a type system for the linear-algebraic λ-calculus. The type system accounts for the linear-algebraic aspects of this extension of λ-calculus: it is able to statically describe the linear combinations of terms that will be obtained when reducing the programs. This gives rise to an original type theory where types, in the same way as terms, can be superposed into linear combinations. We prove that the resulting typed λ-calculus is strongly normalising and features weak subject reduction. Finally, we show how to naturally encode matrices and vectors in this typed calculus.es
dc.description.filFil: Arrighi, Pablo. Aix-Marseille Université; Francia. Centre National de la Recherche Scientifique; Francia
dc.description.filFil: Díaz Caro, Alejandro. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina. Universidad Nacional de Quilmes. Departamento de Ciencia y Tecnología; Argentina
dc.description.filFil: Valiron, Benoît. Université Paris Sud; Francia. Centre National de la Recherche Scientifique; Francia. Université Paris-Saclay; Francia
dc.formatapplication/pdfes
dc.identifier.citationArrighi, Pablo; Díaz Caro, Alejandro; Valiron, Benoît; The vectorial λ-calculus; Academic Press Inc Elsevier Science; Information and Computation; 254; Parte 1; 6-2017; 105-139es
dc.identifier.institucionalCONICET
dc.identifier.issn0890-5401es
dc.identifier.repoCONICET Digital
dc.identifier.urihttp://hdl.handle.net/11336/72528
dc.journal.numberParte 1es
dc.journal.pagination105-139es
dc.journal.paisEstados Unidoses
dc.journal.titleInformation and Computationes
dc.journal.volume254es
dc.language.isoenges
dc.publisherAcademic Press Inc Elsevier Sciencees
dc.relation.alternativeidinfo:eu-repo/semantics/altIdentifier/url/https://www.sciencedirect.com/science/article/pii/S0890540117300482
dc.relation.alternativeidinfo:eu-repo/semantics/altIdentifier/doi/http://dx.doi.org/10.1016/j.ic.2017.04.001
dc.relation.alternativeidinfo:eu-repo/semantics/altIdentifier/url/https://arxiv.org/abs/1308.1138
dc.rightsinfo:eu-repo/semantics/embargoedAccess*
dc.rights.embargoDate2019-07-01*
dc.rights.urihttps://creativecommons.org/licenses/by-nc-nd/2.5/ar/*
dc.subjectLambda Calculuses
dc.subjectType Theoryes
dc.subjectQuantum Computinges
dc.subject.classificationCiencias de la Computaciónes
dc.subject.classificationCiencias de la Computación e Informaciónes
dc.subject.classificationCIENCIAS NATURALES Y EXACTASes
dc.titleThe vectorial λ-calculuses
dc.typeinfo:eu-repo/semantics/article
dc.typeinfo:ar-repo/semantics/artículo
dc.typeinfo:eu-repo/semantics/publishedVersion

Archivos

Bloque original

Miniatura
Nombre:
CONICET_Digital_Nro.17e192dc-44a7-4ffa-a8a5-3fdb8ba7bcb5_X.pdf
Tamaño:
515.45 KB
Formato:
Adobe Portable Document Format
Descripción:
Descargar

Colecciones

Articulos(SEDE CENTRAL)
Volver a la Vista simple