Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams

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.

arXiv commentTo appear in LICS 2018

References in corpus (2)

• Classical Control, Quantum Circuits and Linear Logic in Enriched Category Theory
• Relative symmetric monoidal closed categories I: Autoenrichment and change of base

Cited by in corpus (10)

• Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory
• Realizability in the Unitary Sphere
• Quantum CPOs
• Semantics for first-order affine inductive data types via slice categories
• The Relational Machine Calculus
• Computational Adequacy for Substructural Lambda Calculi
• Proto-Quipper with Reversing and Control
• Reflecting Algebraically Compact Functors
• Quantum Suplattices
• A Framework for Rewriting Families of String Diagrams