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

DOI10.1145/3209108.3209196MaRDI QIDQ5145342zbMATH OpenOpenAlexFDO

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)

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)

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.

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

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
• Classical control, quantum circuits and linear logic in enriched category theory
• scientific article; zbMATH DE number 7450015 (Why is no real title available?)
• Semantics for a lambda calculus for string diagrams
• scientific article; zbMATH DE number 7350775 (Why is no real title available?)
• scientific article; zbMATH DE number 7454912 (Why is no real title available?)
• Quantum programming with inductive datatypes: causality and affine type theory
• Quantum Suplattices
• scientific article; zbMATH DE number 7453968 (Why is no real title available?)
• Quantum CPOs

Describes a project that uses

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)