Realizability in the Unitary Sphere

Abstract

In this paper we present a semantics for a linear algebraic lambda-calculus based on realizability. This semantics characterizes a notion of unitarity in the system, answering a long standing issue. We derive from the semantics a set of typing rules for a simply-typed linear algebraic lambda-calculus, and show how it extends both to classical and quantum lambda-calculi.

arXiv comment28 pages

References in corpus (10)

• A Lambda Calculus for Quantum Computation
• Quipper: A Scalable Quantum Programming Language
• A functional quantum programming language
• The Vectorial $\lambda$-Calculus
• Quantum Alternation: Prospects and Problems
• Call-by-value, call-by-name and the vectorial behaviour of the algebraic λ-calculus
• Presheaf models of quantum computation: an outline
• Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams
• Linearity in the non-deterministic call-by-value setting
• A System F accounting for scalars

Cited by in corpus (9)

• A linear linear lambda-calculus
• A categorical construction for the computational definition of vector spaces
• A concrete model for a typed linear algebraic lambda calculus
• Automating Equational Proofs in Dirac Notation
• Towards a Computational Quantum Logic: An Overview of an Ongoing Research Program
• A linear proof language for second-order intuitionistic linear logic
• IMALL with a Mixed-State Modality: A Logical Approach to Quantum Computation
• A Quantum-Control Lambda-Calculus with Multiple Measurement Bases
• A Quick Overview on the Quantum Control Approach to the Lambda Calculus