A System F accounting for scalars
The Algebraic lambda-calculus and the Linear-Algebraic lambda-calculus extend the lambda-calculus with the possibility of making arbitrary linear combinations of terms. In this paper we provide a fine-grained, System F-like type system for the linear-algebraic lambda-calculus. We show that this &quo...
Main Authors: | Pablo Arrighi, Alejandro Diaz-Caro |
---|---|
Format: | Article |
Language: | English |
Published: |
Logical Methods in Computer Science e.V.
2012-02-01
|
Series: | Logical Methods in Computer Science |
Subjects: | |
Online Access: | https://lmcs.episciences.org/846/pdf |
Similar Items
-
Scalar and Vectorial mu-calculus with Atoms
by: Bartek Klin, et al.
Published: (2019-10-01) -
Lineal: A linear-algebraic Lambda-calculus
by: Pablo Arrighi, et al.
Published: (2017-03-01) -
A dependent nominal type theory
by: James Cheney
Published: (2012-02-01) -
On Irrelevance and Algorithmic Equality in Predicative Type Theory
by: Andreas Abel, et al.
Published: (2012-03-01) -
A proof of strong normalisation using domain theory
by: Thierry Coquand, et al.
Published: (2007-12-01)