CoChat
Sign Up
Cited by 378Logic, programming, and type systemsAdvanced Algebra and LogicLogic, Reasoning, and Knowledge

The DOI matches its Crossref record.

Games and full completeness for multiplicative linear logic

Abramsky, Samson, Jagadeesan, Radha·1994·Journal of Symbolic Logic
DOI 10.2307/2275407
Open this paper in CoChat — free account

Abstract

We present a game semantics for Linear Logic, in which formulas denote games and proofs denote winning strategies. We show that our semantics yields a categorical model of Linear Logic and prove full completeness for Multiplicative Linear Logic with the MIX rule: every winning strategy is the denotation of a unique cut-free proof net. A key role is played by the notion of history-free strategy; strong connections are made between history-free strategies and the Geometry of Interaction. Our semantics incorporates a natural notion of polarity, leading to a refined treatment of the additives. We make comparisons with related work by Joyal, Blass, et al.

Overview

Integrity signals

Registry

Crossref · 10.2307/2275407

Cites

Statistics

Recomputing p-values needs the paper’s full text.

Verification

Claims the paper makes

This paper’s full text isn’t openly available, so its claims and self-check weren’t run. The registry and citation checks still apply.

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

Citations

Cites

No references could be resolved yet.

Research works printed but not linked: 35

  1. 10.1090/conm/092/1003210 · DOI
  2. 10.1016/0304-3975(77)90044-5 · DOI
  3. Lafont, 1991, Proceedings of the sixth annual symposium on logic in computer science, 43
  4. Lafont, 1990, Proceedings of the seventeenth ACM symposium on principles of programming languages, 95
  5. Joyal, 1977, Remarques sur la theorie des jeux a deux personnes, Gazette des sciences mathematiques du Quebec, 1
  6. 10.1007/BFb0040266 · DOI
  7. Hoare, 1985, Communicating sequential processes
  8. Girard, 1989, Logic Colloquium 88, 221
  9. Gonthier, 1992, Proceedings of the seventh symposium on logic in computer science, 223
  10. Freyd, 1990, Categories, allegories, 39
  11. 10.1016/0304-3975(90)90151-7 · DOI
  12. 10.1017/S0960129500001274 · DOI
  13. Abramsky, 1992, Proceedings of the seventh symposium on logic in computer science, 211
  14. 10.1090/conm/092/1003194 · DOI
  15. 10.1090/conm/092/1003197 · DOI · Paper page
  16. 10.1017/S0960129500000189 · DOI
  17. 10.1016/0304-3975(86)90044-7 · DOI
  18. 10.1007/BFb0064579 · DOI
  19. Coquand, 1987, Third workshop on the mathematical foundations of programming language semantics, 344
  20. 10.1016/0168-0072(92)90073-9 · DOI
  21. Abramsky, 1991, Proofs as processes
  22. 10.1017/S0960129500001328 · DOI
  23. Berry, 1985, Theory and practice of sequential algorithms: the kernel of the applicative language CDS, Algebraic semantics, 35
  24. 10.1016/0304-3975(93)90181-R · DOI
  25. 10.1007/3-540-56287-7_113 · DOI
  26. Girard, 1988, International Conference on Computer Logic, COLOG 88, 417, 76
  27. 10.4064/fm-77-2-151-166 · DOI
  28. Abramsky S. , A strong completeness theorem for multiplicative linear logic: Preliminary announcement, E-mail communication on types mailing list, 1992. · DOI
  29. Jacobs B. , Semantics of weakening and contraction, 1992, preprint.
  30. Blute, 1992, Linear logic, coherence, and dinaturality
  31. Milner, 1975, Logic colloquium, Bristol 1973, 157
  32. 10.1007/BF01622878 · DOI
  33. 10.1016/0304-3975(87)90045-4 · DOI · Paper page
  34. Conway, 1976, volume 6 of London Mathematical Society Monographs, 6
  35. Davey, 1990, Introduction to lattices and order

Cited by

Sorted by citations

See all 378

Metadata

Authors
Abramsky, S., & Jagadeesan, R.
Affiliations
  • Imperial College London (GB)
  • Loyola University Chicago (US)
ORCID
Venue
Journal of Symbolic Logic
Publisher
Cambridge University Press (CUP)
Published
1994-06
Volume
59
Issue
2
Pages
543-574
ISSN
  • 0022-4812 (ISSN-L)
  • 1943-5886
DOI
10.2307/2275407
OpenAlex
W2094685149
Cited by
378
References
0
Citations by year
2026: 2 · 2025: 2 · 2024: 4 · 2023: 6 · 2022: 3 · 2021: 7 · 2020: 5 · 2019: 7 · 2018: 12 · 2017: 3 · 2016: 9 · 2015: 9 · 2014: 10 · 2013: 11 · 2012: 9
FWCI
23.17
Type
journal article
Language
en
Open access
closed
Licence
www.cambridge.org/core/terms (unspecified, 7224 d)
Locations
Journal of Symbolic Logic (publishedVersion)
Topics
  • Physical Sciences › Computer Science › Software › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Advanced Algebra and Logic
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, Reasoning, and Knowledge
Keywords
game semantics, linear logic, multiplicative linear logic, winning strategies, categorical models, geometry of interaction, polarity, additives

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review