Coherence for sharing proof-nets

Sharing graphs are an implementation of linear logic proof-nets in which a redex is never duplicated. In their usual formulation, sharing graphs present a problem of coherence: if the proof-net N reduces by standard cut-elimination to N′, then, by reducing the sharing graph of N we do not obtain the sharing graph of N′. We solve this problem by changing the way the information is coded into sharing graphs and introducing a new reduction rule (absorption). The rewriting system is confluent and terminating. The proof exploits an algebraic semantics for sharing graphs.

Authors

• Stefano Guerrini
• Simone Martini
• Andrea Masini

Keywords

• Linear logic
• Cut-elimination
• Proof-nets
• Lambda-calculus optimal reductions
• Sharing graphs