Paper Info
Title
Softness of MALL proof-structures and a correctness criterion with Mix
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.
Year
DOI
Venue
2004
10.1007/s00153-004-0222-6
Arch. Math. Log.
Keywords
Field
DocType
or phrases: linear logic,multiplicative additive proof-nets,sequentialization,linear logic,satisfiability
Discrete mathematics,Algebraic number,Categorical variable,Correctness,Linear logic,Jump,Mathematics
Journal
Volume
Issue
ISSN
43
6
0933-5846
Citations 
PageRank 
References 
3
0.60
10
Authors
1
Name
Order
Citations
PageRank
Masahiro Hamano1397.66