Mackey-complete spaces and power series -- A topological model of Differential Linear Logic
Logic in Computer Science
2015-07-14 v1
Abstract
In this paper, we have described a denotational model of Intuitionist Linear Logic which is also a differential category. Formulas are interpreted as Mackey-complete topological vector space and linear proofs are interpreted by bounded linear functions. So as to interpret non-linear proofs of Linear Logic, we have used a notion of power series between Mackey-complete spaces, generalizing the notion of entire functions in C. Finally, we have obtained a quantitative model of Intuitionist Differential Linear Logic, where the syntactic differentiation correspond to the usual one and where the interpretations of proofs satisfy a Taylor expansion decomposition.
Keywords
Cite
@article{arxiv.1507.03262,
title = {Mackey-complete spaces and power series -- A topological model of Differential Linear Logic},
author = {Marie Kerjean and Christine Tasson},
journal= {arXiv preprint arXiv:1507.03262},
year = {2015}
}