HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

On the relation between coherence semantics and multiplicative proof nets

Christian Retoré 1
1 MEIJE - Concurrency, Synchronization and Real-time Programming
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : It is known that (mix) proof nets admits a coherence semantics, computed as a set of experiments. We prove here the converse: a proof structure is shown to be a proof net whenever its sets of experiments is a semantical object --- a clique of the corresponding coherence space. Moreover the interpretation of atomic formulae can be restricted to a given coherent space with three tokens in its web. This is done by transforming \tt cut links into \tt tensor links. Dealing directly with non-cut-free proof structure we characterise the deadlock freeness of the reduced proof structure. These results are especially convenient for Abramsky's proof expressions, and can be extended to the pomset calculus.
Document type :
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 2:51:02 PM
Last modification on : Friday, February 4, 2022 - 3:19:28 AM
Long-term archiving on: : Monday, April 5, 2010 - 12:07:13 AM


  • HAL Id : inria-00074245, version 1



Christian Retoré. On the relation between coherence semantics and multiplicative proof nets. RR-2430, INRIA. 1994. ⟨inria-00074245⟩



Record views


Files downloads