A linear linear lambda-calculus

DOI10.1017/S0960129524000197MaRDI QIDQ7020354zbMATH OpenFDO

Authors Alejandro Díaz-Caro, Gilles Dowek

Publication date 4 March 2025

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/S0960129524000197

zbMATH Keywords

lambda calculuslinear logicproof theoryquantum computing

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Theory of programming languages (68N15) Quantum computation (81P68)

Cites work

• A lambda calculus for quantum computation with classical control
• A new connective in natural deduction, and its application to quantum computing
• A System F accounting for scalars
• Coherent Banach spaces: A continuous denotational semantics
• Higher-order rewrite systems and their confluence
• Hopf algebras and linear logic
• scientific article; zbMATH DE number 6712184 (Why is no real title available?)
• Linear logic
• Linearity in the non-deterministic call-by-value setting
• On Köthe sequence spaces and linear logic
• On quantum lambda calculi: a foundational perspective
• Picturing quantum processes. A first course in quantum theory and diagrammatic reasoning
• Quantum Control in the Unitary Sphere: Lambda-S1 and its Categorical Model
• Realizability in the unitary sphere
• The algebraic lambda calculus
• The vectorial \(\lambda\)-calculus

Cited in

(4)

• An algebraic extension of intuitionistic linear logic: the \(\mathcal{L}_!^{\mathcal{S}}\)-calculus and its categorical model
• Towards a computational quantum logic. An overview of an ongoing research program
• A linear proof language for second-order intuitionistic linear logic
• The sup connective in IMALL: a categorical semantics

This page was built for publication: A linear linear lambda-calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7020354)