Softness of MALL proof-structures and a correctness criterion with Mix

Research output: Contribution to journalArticlepeer-review

3 Citations (Scopus)

Abstract

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.

Original languageEnglish
Pages (from-to)751-794
Number of pages44
JournalArchive for Mathematical Logic
Volume43
Issue number6
DOIs
Publication statusPublished - 2004 Aug

All Science Journal Classification (ASJC) codes

  • Philosophy
  • Logic

Fingerprint

Dive into the research topics of 'Softness of MALL proof-structures and a correctness criterion with Mix'. Together they form a unique fingerprint.

Cite this