Weak topologies for Linear Logic
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 sequen...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2016-03-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1626/pdf |
| _version_ | 1827322869508472832 |
|---|---|
| author | Marie Kerjean |
| author_facet | Marie Kerjean |
| author_sort | Marie Kerjean |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:35:46Z |
| format | Article |
| id | doaj.art-964316d6f5d64ef59c6efd092289ad47 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:35:46Z |
| publishDate | 2016-03-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-964316d6f5d64ef59c6efd092289ad472024-03-08T09:43:02ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742016-03-01Volume 12, Issue 110.2168/LMCS-12(1:3)20161626Weak topologies for Linear LogicMarie Kerjeanhttps://orcid.org/0000-0001-6141-6251We 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.https://lmcs.episciences.org/1626/pdfcomputer science - logic in computer science |
| spellingShingle | Marie Kerjean Weak topologies for Linear Logic Logical Methods in Computer Science computer science - logic in computer science |
| title | Weak topologies for Linear Logic |
| title_full | Weak topologies for Linear Logic |
| title_fullStr | Weak topologies for Linear Logic |
| title_full_unstemmed | Weak topologies for Linear Logic |
| title_short | Weak topologies for Linear Logic |
| title_sort | weak topologies for linear logic |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/1626/pdf |
| work_keys_str_mv | AT mariekerjean weaktopologiesforlinearlogic |