- Submit
-
Browse
- All Categories
- Metaphysics and Epistemology
- Value Theory
- Science, Logic, and Mathematics
- Science, Logic, and Mathematics
- Logic and Philosophy of Logic
- Philosophy of Biology
- Philosophy of Cognitive Science
- Philosophy of Computing and Information
- Philosophy of Mathematics
- Philosophy of Physical Science
- Philosophy of Social Science
- Philosophy of Probability
- General Philosophy of Science
- Philosophy of Science, Misc
- History of Western Philosophy
- Philosophical Traditions
- Philosophy, Misc
- Other Academic Areas
- More
Switch to: Citations
References in:
A categorical semantics for polarized MALL
Annals of Pure and Applied Logic 145 (3):276-313 (2007)
Add references
You must login to add references.
|
|
|
|
|
|
|
|
|
This paper presents a coherence theorem for star-autonomous categories exactly analogous to Kelly and Mac Lane’s coherence theorem for symmetric monoidal closed categories. The proof of this theorem is based on a categorial cut-elimination result, which is presented in some detail. |
|
|
We show that every MALL proof-structure [9] satisfies the property of softness, originally a categorical notion introduced by Joyal. Furthermore, we show that the notion of hereditary softness precisely captures Girard’s algebraic restriction of the technical condition on proof-structures. Relying on this characterization, we prove a MALL+Mix sequentialization theorem by a proof-theoretical method, using Girard’s notion of jump. Our MALL+Mix correctness criterion subsumes the Danos/Fleury-Retoré criterion [6] for MLL+Mix. |
|
|
|
|
|
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 (...) |
|
|
This paper proposes a synthetic presentation of the proof construction paradigm, which underlies most of the research and development in the so-called “logic programming” area. Two essential aspects of this paradigm are discussed here: true non-determinism and partial information. A new formulation of Focussing, the basic property used to deal with non-determinism in proof construction, is presented. This formulation is then used to introduce a general constraint-based technique capable of dealing with partial information in proof construction. One of the baselines (...) |
|
|
|
|
|
This paper proposes a synthetic presentation of the proof construction paradigm, which underlies most of the research and development in the so-called “logic programming” area. Two essential aspects of this paradigm are discussed here: true non-determinism and partial information. A new formulation of Focussing, the basic property used to deal with non-determinism in proof construction, is presented. This formulation is then used to introduce a general constraint-based technique capable of dealing with partial information in proof construction. One of the baselines (...) |
|
|
We introduce a linear analogue of Läuchli's semantics for intuitionistic logic. In fact, our result is a strengthening of Läuchli's work to the level of proofs, rather than provability. This is obtained by considering continuous actions of the additive group of integers on a category of topological vector spaces. The semantics, based on functorial polymorphism, consists of dinatural transformations which are equivariant with respect to all such actions. Such dinatural transformations are called uniform. To any sequent in Multiplicative Linear Logic (...) |
PhilPapers logo by Andrea Andrews and Meghan Driscoll.
This site uses cookies and Google Analytics (see our terms & conditions for details regarding the privacy implications). Use of this site is subject to terms & conditions.
All rights reserved by The PhilPapers Foundation
Server: philpapers-web-c4c498947-42cwx uwo