Sciweavers

CSL
2008
Springer

A Characterization of Hypercoherent Semantic Correctness in Multiplicative Additive Linear Logic

13 years 11 months ago
A Characterization of Hypercoherent Semantic Correctness in Multiplicative Additive Linear Logic
We give a graph theoretical criterion on multiplicative additive linear logic (MALL) cut-free proof structures that exactly characterizes those whose interpretation is a hyperclique in Ehrhard's hypercoherent spaces. This criterion is strictly weaker than the one given by Hughes and van Glabbeek characterizing proof nets (i.e. desequentialized sequent calculus proofs). We thus also give the first proof of semantical soundness of hypercoherent spaces with respect to proof nets entirely based on graph theoretical trips, in the style of Girard's proof of semantical soundness of coherent spaces for proof nets of the multiplicative fragment of linear logic.
Paolo Tranquilli
Added 19 Oct 2010
Updated 19 Oct 2010
Type Conference
Year 2008
Where CSL
Authors Paolo Tranquilli
Comments (0)