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

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.

In Proceedings DCM 2011, arXiv:1207.6821

References in corpus (3)

• A Lambda Calculus for Quantum Computation
• A functional quantum programming language
• Linearity in the non-deterministic call-by-value setting

Cited by in corpus (4)

• Call-by-value non-determinism in a linear logic type discipline
• Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi
• Non determinism through type isomorphism
• The probability of non-confluent systems