Realizability in the Unitary Sphere
Logic in Computer Science
2019-12-06 v1
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.
Cite
@article{arxiv.1904.08785,
title = {Realizability in the Unitary Sphere},
author = {Alejandro Díaz-Caro and Mauricio Guillermo and Alexandre Miquel and Benoît Valiron},
journal= {arXiv preprint arXiv:1904.08785},
year = {2019}
}
Comments
28 pages