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.
📄 Full Paper Available as PDF
This paper is available as a downloadable PDF.
📄 Download PDF
Comments (0)
No comments yet. Be the first to comment.
Research
