Mackey-complete spaces and power series -- A topological model of Differential Linear Logic
classification
💻 cs.LO
keywords
linearlogicdifferentialmackey-completemodelproofsfunctionsinterpreted
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.