Skip Navigation



Journal of Logic and Computation Advance Access published online on August 25, 2009
Journal of Logic and Computation, doi:10.1093/logcom/exp044
This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Laurent, O.
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author, 2009. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Original Papers

Intuitionistic Dual-intuitionistic Nets

Olivier Laurent

Laboratoire de l’Informatique du Parallélisme, ENS Lyon – Université de Lyon, UMR 5668 CNRS ENS-Lyon UCBL INRIA, 46, allée d’Italie, 69364 Lyon cedex 07, France. E-mail: olivier.laurent{at}ens-lyon.fr

Received 15 December 2008.

The intuitionistic sequent calculus (at most one formula on the right-hand side of sequents) comes with a natural dual system: the dual-intuitionistic sequent calculus (at most one formula on the left-hand side). We explain how the duality between these two systems exactly corresponds to the intensively studied duality between call-by-value systems and call-by-name systems for classical logic. Relying on the uniqueness of the computational behaviour underlying these four logics (intuitionistic, dual-intuitionistic, call-by-value classical and call-by-name classical), we define a generic syntax of nets which can be used for any of these logics.

Keywords: Classical logic; intuitionistic logic; computational duality; proof-nets



References

  1. Crolard. T. Subtractive logic. Theoretical Computer Science (2001) 254:151–185.[CrossRef][Web of Science]
  2. Curien P.-L, Herbelin. H. The duality of computation. In: Proceedings of the International Conference on Functional Programming (2000) ACM Press: Association for Computing Machinery. 233–243. Vol. 35(9) of ACM SIGPLAN Notices.
  3. Czermak. J. A remark on Gentzen's calculus of sequents. Notre Dame Journal of Formal Logic (1977) 18:471–474.[CrossRef]
  4. Danos V, Joinet J-B, Schellinx. H. LKQ and LKT: sequent calculi for second order logic based upon dual linear decompositions of classical implication. In: Advances in Linear Logic—Girard J.-Y, Lafont Y, Regnier L, eds. (1995) Cambridge University Press. 211–224. Vol. 222 of London Mathematical Society Lecture Note Series.
  5. Danos V, Joinet J.-B, Schellinx. H. A new deconstructive logic: linear logic. Journal of Symbolic Logic (1997) 62:755–807.[CrossRef][Web of Science]
  6. Filinski A. Declarative Continuations and Categorical Duality. Master's Thesis, Computer Science Department, University of Copenhagen, DIKU Report 89/11, August 1989.
  7. Girard. J.-Y. Linear logic. Theoretical Computer Science (1987) 50:1–102.[CrossRef][Web of Science]
  8. Girard. J.-Y. A new constructive logic: classical logic. Mathematical Structures in Computer Science (1991) 1:255–296.[CrossRef]
  9. Girard. J.-Y. Quantifiers in linear logic II. In: Nuovi problemi della logica e della filosofia della scienza—Corsi, Sambin, eds. (1991) 79–90.
  10. Girard J.-Y. Typed Lambda Calculi and Applications’99 (1999) Springer. Vol. 1581 of Lecture Notes in Computer Science.
  11. Glivenko V. Sur quelques points de la logique de M. Brouwer (1929) Académie Royale de Belgique: Bulletins de la classe des sciences.
  12. Griffin T. A formulae-as-types notion of control. In Proceedings of the 1990 Principles of Programming Languages Conference. IEEE Computer Society Press, pp. 47–58. Intuitionistic Dual-intuitionistic Nets 27.
  13. Hofmann M, Streicher. T. Completeness of continuation models for lambda-mu-calculus. Information and Computation (2002) 179:332–355.[CrossRef][Web of Science]
  14. IEEE. (1990) Proceedings of the 1990 Principles of Programming Languages Conference. IEEE Computer Society Press.
  15. Lafont Y. Interaction nets. In Proceedings of the 1990 Principles of Programming Languages Conference, IEEE Computer Society Press, pp. 95–108.
  16. Lafont Y, Reus B, Streicher. T. Continuation semantics or expressing implication by negation. In: Technical Report 93-21 (1993) München: Ludwig-Maximilians-Universität.
  17. Lamarche F. Proof nets for intuitionistic linear logic I: essential nets. In: Preliminary report. April 1994.
  18. Laurent. O. Polarized proof-nets: proof-nets for LC (extended abstract). In: Typed Lambda Calculi and Applications’99—Girard J.-Y, ed. Springer. 213–227. Vol. 1581 of Lecture Notes in Computer Science.
  19. Laurent O. Étude de la polarisation en logique (2002) Université Aix-Marseille II: Thèse de doctorat.
  20. Laurent. O. Polarized proof-nets and {lambda}µ-calculus. Theoretical Computer Science (2003) 290:161–188.[CrossRef][Web of Science]
  21. Laurent. O. Classical isomorphisms of types. Mathematical Structures in Computer Science (2005) 15:969–1004.[CrossRef][Web of Science]
  22. Laurent O, Quatrini M, Falco. L. Tortora de. Polarized and focalized linear and classical proofs. Annals of Pure and Applied Logic (2005) 134:217–264.[CrossRef][Web of Science]
  23. Laurent O, de Falco L. Tortora. Slicing polarized additive normalization. In: Linear Logic in Computer Science—Ehrhard T, Girard J.-Y, Ruet P, Scott P, eds. (2004) Cambridge University Press. 247–282. Vol. 316 of London Mathematical Society Lecture Note Series.
  24. Levy P. B. Call-by-push-value: a subsuming paradigm. In: Typed Lambda Calculi and Applications’99—Girard J.-Y, ed. Springer. 228–242. Vol. 1581 of Lecture Notes in Computer Science.
  25. Murawski A, Ong L. Dominator trees and fast verification of proof nets. In: Proceedings of the fifteenth annual symposium on Logic In Computer Science (2000) IEEE Computer Society Press: IEEE. 181–191.
  26. Ogata I. Cut elimination for classical proofs as continuation passing style computation. In: Advances in Computing Science ASIAN, Vol.—Hsiang J, Ohori A, eds. (1998) Springer. 61–78. Vol. 1538 of Lecture Notes in Computer Science.[CrossRef]
  27. Parigot M. {lambda}µ-calculus: an algorithmic interpretation of classical natural deduction. In: Proceedings of International Conference on Logic Programming and Automated Reasoning (1992) Springer. 190–201. Vol. 624 of Lecture Notes in Computer Science.
  28. Quatrini M, de Falco L. Tortora. Polarisation des preuves classiques et renversement. Comptes Rendus de l’Académie des Sciences de Paris (1996) 323:113–116.
  29. Selinger. P. Control categories and duality: on the categorical semantics of the lambda-mu calculus. Mathematical Structures in Computer Science (2001) 11:207–260.[CrossRef]
  30. Streicher T, Reus. B. Classical logic, continuation semantics and abstract machines. Journal of Functional Programming (1998) 8:543–572.[CrossRef]

Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?



This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Laurent, O.
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?