Document Open Access Logo

On Classical PCF, Linear Logic and the MIX Rule

Authors Shahin Amini, Thomas Erhard

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2015.582.pdf
  • Filesize: 0.56 MB
  • 15 pages

Document Identifiers

Subject Classification

Keywords
  • lambda-calculus
  • linear logic
  • classical logic
  • denotational semantics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We study a classical version of PCF from a semantical point of view. We define a general notion of model based on categorical models of Linear Logic, in the spirit of earlier work by Girard, Regnier and Laurent. We give a concrete example based on the relational model of Linear Logic, that we present as a non-idempotents intersection type system, and we prove an Adequacy Theorem using ideas introduced by Krivine. Following Danos and Krivine, we also consider an extension of this language with a MIX construction introducing a form of must non-determinism; in this language, a program of type integer can have more than one value (or no value at all, raising an error). We propose a refinement of the relational model of classical PCF in which programs of type integer are single valued; this model rejects the MIX syntactical constructs (and the MIX rule of Linear Logic).

Cite As Get BibTex

Shahin Amini and Thomas Erhard. On Classical PCF, Linear Logic and the MIX Rule. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 582-596, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CSL.2015.582

Author Details

Shahin Amini
Thomas Erhard

References

  1. Pierre-Louis Curien and Hugo Herbelin. The duality of computation. In Martin Odersky and Philip Wadler, editors, Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP'00), Montreal, Canada, September 18-21, 2000., pages 233-243. ACM, 2000. Google Scholar
  2. Vincent Danos and Jean-Louis Krivine. Disjunctive Tautologies as Synchronisation Schemes. In Peter Clote and Helmut Schwichtenberg, editors, CSL, volume 1862 of Lecture Notes in Computer Science, pages 292-301. Springer-Verlag, 2000. Google Scholar
  3. Daniel De Carvalho. Execution Time of λ-Terms via Denotational Semantics and Intersection Types. Research Report RR-6638, INRIA, 2008. To appear in Mathematical Structures in Computer Sciences. Google Scholar
  4. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1-102, 1987. Google Scholar
  5. Jean-Yves Girard. A new constructive logic: classical logic. Mathematical Structures in Computer Science, 1(3):225-296, 1991. Google Scholar
  6. Jean-Yves Girard. The blind spot: lectures on logic. European Mathematical Society, 2011. 537 pages. Google Scholar
  7. Timothy G. Griffin. The Formulae-as-Types Notion of Control. In Proceedings of the 17h ACM Symposium on Principles of Programming Languages (POPL), pages 47-57. Association for Computing Machinery, January 1990. Google Scholar
  8. Hugo Herbelin. Games and Weak-Head Reduction for Classical PCF. In Philippe de Groote, editor, TLCA, volume 1210 of Lecture Notes in Computer Science, pages 214-230. Springer-Verlag, 1997. Google Scholar
  9. Martin Hofmann and Thomas Streicher. Completeness of Continuation Models for lambda-mu-Calculus. Information and Computation, 179(2):332-355, 2002. Google Scholar
  10. Olivier Laurent. Polarized games. Annals of Pure and Applied Logic, 130(1-3):79-123, 2004. Google Scholar
  11. Olivier Laurent and Laurent Regnier. About Translations of Classical Logic into Polarized Linear Logic. In 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings, pages 11-20. IEEE Computer Society, 2003. Google Scholar
  12. Paul-André Melliès. Categorical Semantics of Linear Logic. Panoramas et Synthèses, 27, 2009. Google Scholar
  13. Michel Parigot. λμ-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. In Andrei Voronkov, editor, Logic Programming and Automated Reasoning,International Conference LPAR'92, St. Petersburg, Russia, July 15-20, 1992, Proceedings, volume 624 of Lecture Notes in Computer Science, pages 190-201. Springer-Verlag, 1992. Google Scholar
  14. Peter Selinger. Control Categories and Duality: on the Categorical Semantics of the Lambda-Mu Calculus. Mathematical Structures in Computer Science, 11(2):207-260, 2001. Google Scholar
  15. Thomas Streicher and Bernhard Reus. Classical Logic, Continuation Semantics and Abstract Machines. Journal of Functional Programming, 8(6):543-572, 1998. Google Scholar
  16. Lionel Vaux. Convolution lambda-bar-mu-calculus. In Simona Ronchi Della Rocca, editor, Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings, volume 4583 of Lecture Notes in Computer Science, pages 381-395. Springer, 2007. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact