Enriching a linear/non-linear lambda calculus: a programming language for string diagrams

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

Authors: Bert Lindenhovius, Vladimir Zamdzhiev, Michael Mislove 

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

Recommendations

• A Linear-non-Linear Model for a Computational Call-by-Value Lambda Calculus (Extended Abstract)
• The enriched effect calculus: syntax and semantics
• Enriching an Effect Calculus with Linear Types
• Categorical models for a semantically linear \(\lambda\)-calculus
• scientific article

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: a programming language for string diagrams

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