Authors: Marie Kerjean

We construct a denotational model of linear logic, whose objects are all the locally convex and separated topological vector spaces endowed with their weak topology. The negation is interpreted as the dual, linear proofs are interpreted as continuous linear functions, and non-linear proofs as sequences of monomials. We do not complete our constructions by a double-orthogonality operation. This yields an interpretation of the polarity of the connectives in terms of topology.

• 03B44 - Temporal logic
• 68Q25 - Analysis of algorithms and problem complexity
• 68Q85 - Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)