Softness of hypercoherences and MALL full completeness

We prove a full completeness theorem for multiplicative-additive linear logic (i.e. MALL) 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 MALL proof. Our proof consists of three steps. We show:

• Type: Journal
• Year: 2005
• Where: APAL
• Authors: Richard Blute, Masahiro Hamano, Philip J. Scott
• Keywords: APAL 2005, Cut-free Mall Proof, Dinatural Transformation, MALL