A linear linear lambda-calculus
Logic in Computer Science
2025-09-25 v7
Abstract
We present a linearity theorem for a proof language of intuitionistic multiplicative additive linear logic, incorporating addition and scalar multiplication. The proofs in this language are linear in the algebraic sense. This work is part of a broader research program aiming to define a logic with a proof language that forms a quantum programming language.
Keywords
Cite
@article{arxiv.2201.11221,
title = {A linear linear lambda-calculus},
author = {Alejandro Díaz-Caro and Gilles Dowek},
journal= {arXiv preprint arXiv:2201.11221},
year = {2025}
}
Comments
This is the full revised journal version of the FSCD 2022 paper published at LIPIcs 228:21, 2022