pith. sign in

arxiv: 1507.03262 · v1 · pith:YTHMT5OJnew · submitted 2015-07-12 · 💻 cs.LO

Mackey-complete spaces and power series -- A topological model of Differential Linear Logic

classification 💻 cs.LO
keywords linearlogicdifferentialmackey-completemodelproofsfunctionsinterpreted
0
0 comments X
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.