Enriching a Linear/Non-linear Lambda Calculus

DOI10.1145/3209108.3209196zbMATH Open1454.03023arXiv1804.09822OpenAlexW4289760920MaRDI QIDQ5145342FDOQ5145342

Michael Mislove, Vladimir Zamdzhiev, Bert Lindenhovius

Publication date: 20 January 2021

Published in: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Abstract: Linear/non-linear (LNL) models, as described by Benton, soundly model a LNL term calculus and LNL logic closely related to intuitionistic linear logic. Every such model induces a canonical enrichment that we show soundly models a LNL lambda calculus for string diagrams, introduced by Rios and Selinger (with primary application in quantum computing). Our abstract treatment of this language leads to simpler concrete models compared to those presented so far. We also extend the language with general recursion and prove soundness. Finally, we present an adequacy result for the diagram-free fragment of the language which corresponds to a modified version of Benton and Wadler's adjoint calculus with recursion.

Full work available at URL: https://arxiv.org/abs/1804.09822

zbMATH Keywords

programming languagescategorical semanticsquantum computingenriched category theorystring diagrams

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Functional programming and lambda calculus (68N18)

Cited In (12)

• Lambda-calculus with director strings
• Formalization of metatheory of the Quipper quantum programming language in a linear logic
• Semantics of quantum programming languages: Classical control, quantum control
• Title not available (Why is that?)
• Semantics for a lambda calculus for string diagrams
• Title not available (Why is that?)
• Title not available (Why is that?)
• Quantum programming with inductive datatypes: causality and affine type theory
• Quantum Suplattices
• Title not available (Why is that?)
• Quantum CPOs
• Title not available (Why is that?)

Uses Software

• Quipper

This page was built for publication: Enriching a Linear/Non-linear Lambda Calculus

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