Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abramsky, S., Melliès, P.-A.: Concurrent games and full completeness. In: LICS, pp. 431–442. IEEE Computer Society Press, Los Alamitos (1999)
Blute, R., Hamano, M., Scott, P.J.: Softness of hypercoherences and MALL full completeness. Ann. Pure Appl. Logic 131(1-3), 1–63 (2005)
Bucciarelli, A., Ehrhard, T.: Sequentiality and strong stability. In: LICS, pp. 138–145. IEEE Computer Society Press, Los Alamitos (July 1991)
Danos, V., Regnier, L.: The structure of multiplicatives. Archive for Mathematical Logic 28, 181–203 (1989)
Ehrhard, T.: Hypercoherence: A strongly stable model of linear logic. In: Advances in Linear Logic, pp. 83–108. Cambridge University Press, Cambridge (1995)
Girard, J.-Y.: Linear logic. Th. Comp. Sc. 50, 1–102 (1987)
Girard, J.-Y.: Proof-nets: the parallel syntax for proof-theory. In: Logic and Algebra. Lecture Notes in Pure and Appl. Math, vol. 180, pp. 97–124 (1996)
Hughes, D., van Glabbeek, R.: Proof nets for unit-free multiplicative-additive linear logic. In: LICS, pp. 1–10. IEEE Computer Society Press, Los Alamitos (2003)
Laurent, O., de Falco, L.T.: Slicing polarized additive normalization. In: Linear Logic in Computer Science, pp. 247–282 (2004)
Melliès, P.-A., Mimram, S.: Asynchronous games without alternation (submitted, 2008)
Pagani, M.: Acyclicity and coherence in multiplicative and exponential linear logic. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 531–545. Springer, Heidelberg (2006)
Pagani, M.: Proof nets and cliques: towards the understanding of analytical proofs. PhD thesis, Università Roma Tre / Université Aix-Marseille II (April 2006)
Pagani, M.: Visible acyclic nets: between interaction and semantics (in preparation, 2008)
Paolini, L.: A stable programming language. Inf. Comput. 204(3), 339–375 (2006)
Plotkin, G.D.: Lcf considered as a programming language. Theor. Comput. Sci. 5(3), 225–255 (1977)
Retoré, C.: A semantic characterisation of the correctness of a proof net. Mathematical Structures in Computer Science 7(5), 445–452 (1997)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tranquilli, P. (2008). A Characterization of Hypercoherent Semantic Correctness in Multiplicative Additive Linear Logic. In: Kaminski, M., Martini, S. (eds) Computer Science Logic. CSL 2008. Lecture Notes in Computer Science, vol 5213. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87531-4_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-87531-4_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-87530-7
Online ISBN: 978-3-540-87531-4
eBook Packages: Computer ScienceComputer Science (R0)