Softness of hypercoherences and full completeness

Annals of Pure and Applied Logic 131 (1-3):1-63 (2005)

Abstract
We prove a full completeness theorem for multiplicative–additive linear logic using a double gluing construction applied to Ehrhard’s *-autonomous category of hypercoherences. This is the first non-game-theoretic full completeness theorem for this fragment. Our main result is that every dinatural transformation between definable functors arises from the denotation of a cut-free proof. Our proof consists of three steps. We show:• Dinatural transformations on this category satisfy Joyal’s softness property for products and coproducts.• Softness, together with multiplicative full completeness, guarantees that every dinatural transformation corresponds to a Girard proof-structure.• The proof-structure associated with any dinatural transformation is a proof-net, hence a denotation of a proof. This last step involves a detailed study of cycles in additive proof-structures.The second step is a completely general result, while the third step relies on the concrete structure of a double gluing construction over hypercoherences.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/j.apal.2004.05.002
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 43,914
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

The Structure of Multiplicatives.Vincent Danos & Laurent Regnier - 1989 - Archive for Mathematical Logic 28 (3):181-203.
Linear Logic: Its Syntax and Semantics.Jean-Yves Girard - 1995 - In Jean-Yves Girard, Yves Lafont & Laurent Regnier (eds.), Advances in Linear Logic. Cambridge University Press. pp. 222--1.
Linear Läuchli Semantics.R. F. Blute & P. J. Scott - 1996 - Annals of Pure and Applied Logic 77 (2):101-142.

View all 8 references / Add more references

Citations of this work BETA

A Categorical Semantics for Polarized MALL.Masahiro Hamano & Philip Scott - 2007 - Annals of Pure and Applied Logic 145 (3):276-313.

Add more citations

Similar books and articles

Z-Modules and Full Completeness of Multiplicative Linear Logic.Masahiro Hamano - 2001 - Annals of Pure and Applied Logic 107 (1-3):165-191.
Linear Läuchli Semantics.R. F. Blute & P. J. Scott - 1996 - Annals of Pure and Applied Logic 77 (2):101-142.
The Shuffle Hopf Algebra and Noncommutative Full Completeness.R. F. Blute & P. J. Scott - 1998 - Journal of Symbolic Logic 63 (4):1413-1436.
The Shuffle Hopf Algebra and Noncommutative Full Completeness.R. F. Blute & P. J. Scott - 1998 - Journal of Symbolic Logic 63 (4):1413-1436.
Completeness of MLL Proof-Nets W.R.T. Weak Distributivity.Jean-Baptiste Joinet - 2007 - Journal of Symbolic Logic 72 (1):159 - 170.

Analytics

Added to PP index
2014-01-16

Total views
12 ( #649,209 of 2,266,272 )

Recent downloads (6 months)
1 ( #850,735 of 2,266,272 )

How can I increase my downloads?

Downloads

My notes

Sign in to use this feature