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

categorical semanticsenriched category theoryprogramming languagesquantum computingstring 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; zbMATH DE number 6712184

Cited in

(13)

• Lambda-calculus with director strings
• Semantics of quantum programming languages: Classical control, quantum control
• Quantum programming with inductive datatypes: causality and affine type theory
• Formalization of metatheory of the Quipper quantum programming language in a linear logic
• LNL-FPC: the linear/non-linear fixpoint calculus
• A framework for rewriting families of string diagrams
• Computational adequacy for substructural lambda calculi
• scientific article; zbMATH DE number 7453968 (Why is no real title available?)
• Classical control, quantum circuits and linear logic in enriched category theory
• Quantum Suplattices
• Semantics for a lambda calculus for string diagrams
• Quantum CPOs
• The relational machine calculus

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)