31
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

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

      Preprint
      , ,

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          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.

          Related collections

          Most cited references7

          • Record: found
          • Abstract: not found
          • Book Chapter: not found

          Interacting Quantum Observables

            Bookmark
            • Record: found
            • Abstract: not found
            • Book Chapter: not found

            A mixed linear and non-linear logic: Proofs, terms and models

            P. Benton (1995)
              Bookmark
              • Record: found
              • Abstract: not found
              • Article: not found

              QWIRE: a core language for quantum circuits

                Bookmark

                Author and article information

                Journal
                25 April 2018
                Article
                1804.09822
                1cbcd220-a915-478e-99a4-471da97a5bff

                http://arxiv.org/licenses/nonexclusive-distrib/1.0/

                History
                Custom metadata
                To appear in LICS 2018
                cs.LO cs.PL math.CT quant-ph

                Quantum physics & Field theory,Theoretical computer science,Programming languages,General mathematics

                Comments

                Comment on this article