Hostname: page-component-586b7cd67f-t7czq Total loading time: 0 Render date: 2024-11-28T03:17:50.276Z Has data issue: false hasContentIssue false
  • English
  • Français

A completeness theorem for symmetric product phase spaces

Published online by Cambridge University Press:  12 March 2014

Thomas Ehrhard
Thomas Ehrhard*
Affiliation:
Fédération de Recherche des Unités de Mathématiques de Marseille FR 2291 and, Institut de Mathematiques de Luminy UMR 6206, Campus de Luminy, Case 907, 13288 Marseille Cedex 9, France, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract.

In a previous work with Antonio Bucciarelli, we introduced indexed linear logic as a tool for studying and enlarging the denotational semantics of linear logic. In particular, we showed how to define new denotational models of linear logic using symmetric product phase models (truth-value models) of indexed linear logic. We present here a strict extension of indexed linear logic for which symmetric product phase spaces provide a complete semantics. We study the connection between this new system and indexed linear logic.

Keywords

linear logicphase semanticscompletenessdenotational semantics
Type
Research Article
Information
The Journal of Symbolic Logic , Volume 69 , Issue 2 , June 2004 , pp. 340 - 370
Copyright
Copyright © Association for Symbolic Logic 2004

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Amadio, Roberto and Curien, Pierre-Louis, Domains and lambda-calculi, Cambridge Tracts in Theoretical Computer Science, vol. 46, Cambridge University Press, 1998.CrossRefGoogle Scholar
[2]Bierman, Gavin, What is a categorical model of intuitionistic linear logic?, Proceedings of the second typed lambda-calculi and applications conference (Dezani-Ciancaglini, Mariangiola and Plotkin, Gordon D., editors), Lecture Notes in Computer Science, vol. 902, Springer-Verlag, 1995, pp. 73–93.Google Scholar
[3]Bruasse-Bac, Alexandra, Logique linéaire indexée du second ordre, Thèse de doctorat, Université de la Méditerranée, 2001.Google Scholar
[4]Bucciarelli, Antonio and Ehrhard, Thomas, On phase semantics and denotational semantics in multiplicative-additive linear logic, Annals of Pure and Applied Logic, vol. 102 (2000), no. 3, pp. 247–282.CrossRefGoogle Scholar
[5]Bucciarelli, Antonio, On phase semantics and denotational semantics: the exponentials, Annals of Pure and Applied Logic, vol. 109 (2001), no. 3, pp. 205–241.CrossRefGoogle Scholar
[6]Ehrhard, Thomas and Regnier, Laurent, The differential lambda-calculus, Theoretical Computer Science, (2003), To appear.Google Scholar
[7]Girard, Jean-Yves, Linear logic, Theoretical Computer Science, vol. 50 (1987), pp. 1–102.CrossRefGoogle Scholar
[8]Girard, Jean-Yves, Linear logic: its syntax and semantics, Advances in linear logic (Girard, Jean-Yves, Lafont, Yves, and Regnier, Laurent, editors), London Mathematical Society Lecture Note Series, vol. 222, Cambridge University Press, 1995.CrossRefGoogle Scholar
[9]Girard, Jean-Yves, On denotational completeness, Theoretical Computer Science, vol. 227 (1999), pp. 249–273.CrossRefGoogle Scholar
[10]Lamarche, François, Generalizing coherent domains and hypercoherences, Electronic Notes in Theoretical Computer Science, vol. 2 (1995).Google Scholar
[11]Okada, Mitsuhiro, Girard's phase semantics and a higher order cut elimination proof, Unpublished, 1994.Google Scholar
[12]Okada, Mitsuhiro, Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic, Theoretical Computer Science, vol. 227 (1999), no. 1-2, pp. 333–396.CrossRefGoogle Scholar