Skip to main content
SpringerLink
Log in

Differential Linear Logic and Polarization

  • Conference paper
Typed Lambda Calculi and Applications (TLCA 2009)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5608))

Included in the following conference series:

Abstract

We extend Ehrhard–Regnier’s differential linear logic along the lines of Laurent’s polarization. We provide a denotational semantics of this new system in the well-known relational model of linear logic, extending canonically the semantics of both differential and polarized linear logics: this justifies our choice of cut elimination rules. Then we show this polarized differential linear logic refines the recently introduced convolution \({\bar\lambda}\mu\)-calculus, the same as linear logic decomposes λ-calculus.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ehrhard, T., Regnier, L.: Differential interaction nets. Theor. Comput. Sci. 364, 166–195 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  2. Ehrhard, T., Regnier, L.: The differential lambda-calculus. Theor. Comput. Sci. 309, 1–41 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  3. Girard, J.Y.: Normal functors, power series and lambda-calculus. Ann. Pure Appl. Logic 37, 129–177 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  4. Ehrhard, T.: Finiteness spaces. Math. Struct. Comput. Sci. 15, 615–646 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  5. Tranquilli, P.: Intuitionistic differential nets and lambda-calculus. To appear in Theor. Comput. Sci (2008)

    Google Scholar 

  6. Andreoli, J.M.: Logic programming with focusing proofs in linear logic. Journal of Logic and Computation 2, 297–347 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  7. Girard, J.Y.: A new constructive logic: Classical Logic. Math. Struct. Comput. Sci. 1, 255–296 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  8. Laurent, O.: Étude de la polarisation en logique. PhD thesis, Université Aix-Marseille 2 (2002)

    Google Scholar 

  9. Danos, V.: Une application de la logique linéaire à l’étude des processus de normalisation (principalement du λ-calcul). PhD thesis, Université Paris 7 (1990)

    Google Scholar 

  10. Regnier, L.: Lambda-calcul et réseaux. PhD thesis, Université Paris 7 (1992)

    Google Scholar 

  11. Laurent, O., Regnier, L.: About translations of classical logic into polarized linear logic. In: Proceedings of LICS 2003 (2003)

    Google Scholar 

  12. Bierman, G.M.: What is a categorical model of intuitionistic linear logic? In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  13. Vaux, L.: The differential λμ-calculus. Theor. Comput. Sci. 379, 166–209 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  14. Bucciarelli, A., Ehrhard, T., Manzonetto, G.: Not enough points is enough. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 298–312. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  15. Vaux, L.: Convolution \(\bar\lambda\mu\)-calculus. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 381–395. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  16. Mazza, D.: Interaction Nets: Semantics and Concurrent Extensions. PhD thesis, Université Aix–Marseille 2, Università degli Studi Roma Tre (2006)

    Google Scholar 

  17. Lafont, Y.: From proof nets to interaction nets. In: Advances in Linear Logic. London Math. Soc. Lect. Not., vol. 222. Cambridge University Press, Cambridge (1995)

    Google Scholar 

  18. Schwartz, L.: Théorie des distributions. Hermann (1966)

    Google Scholar 

  19. Vaux, L.: λ-calcul différentiel et logique classique: interactions calculatoires. PhD thesis, Université Aix-Marseille 2 (2007)

    Google Scholar 

  20. Polonowski, E.: Substitutions explicites, logique et normalisation. PhD thesis, Université Paris 7 (2004)

    Google Scholar 

  21. Ehrhard, T., Regnier, L.: Uniformity and the Taylor expansion of ordinary lambda-terms. Theor. Comput. Sci. 403, 347–372 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  22. Ehrhard, T., Regnier, L.: Böhm trees, Krivine’s machine and the Taylor expansion of lambda-terms. In: Proceedings of CiE 2006 (2006)

    Google Scholar 

  23. Ehrhard, T., Laurent, O.: Interpreting a finitary pi-calculus in differential interaction nets. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 333–348. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  24. Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, i. Inf. Comput. 100(1), 1–40 (1992)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire de Mathématiques de l’Université de Savoie, UMR 5127 CNRS, 73376, Le Bourget-du-Lac Cedex, France

    Lionel Vaux

Authors
  1. Lionel Vaux
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Laboratoire PPS (CNRS / Paris 7), Case 7014, Université Paris Diderot - Paris 7, 75205, Paris Cedex 13, France

    Pierre-Louis Curien

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Vaux, L. (2009). Differential Linear Logic and Polarization. In: Curien, PL. (eds) Typed Lambda Calculi and Applications. TLCA 2009. Lecture Notes in Computer Science, vol 5608. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02273-9_27

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02273-9_27

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-02272-2

  • Online ISBN: 978-3-642-02273-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation