Softness of hypercoherences and MALL full completeness

Richard Blute, Masahiro Hamano, Philip Scott

Research output: Contribution to journalArticlepeer-review

12 Citations (Scopus)


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: • 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 MALL proof-structure. • The proof-structure associated with any dinatural transformation is a MALL 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.

Original languageEnglish
Pages (from-to)1-63
Number of pages63
JournalAnnals of Pure and Applied Logic
Issue number1-3
Publication statusPublished - 2005 Jan

All Science Journal Classification (ASJC) codes

  • Logic


Dive into the research topics of 'Softness of hypercoherences and MALL full completeness'. Together they form a unique fingerprint.

Cite this