Skip to main content
SpringerLink
Log in

Interpreting Polymorphic FPC into Domain Theoretic Models of Parametric Polymorphism

  • Conference paper
Automata, Languages and Programming (ICALP 2006)

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

Included in the following conference series:

Abstract

This paper shows how parametric PILL Y (Polymorphic Intuitionistic / Linear Lambda calculus with a fixed point combinator Y) can be used as a metalanguage for domain theory, as originally suggested by Plotkin more than a decade ago. Using recent results about solutions to recursive domain equations in parametric models of PILL Y , we show how to interpret FPC in these. Of particular interest is a model based on “admissible” pers over a reflexive domain, the theory of which can be seen as a domain theory for (impredicative) polymorphism. We show how this model gives rise to a parametric and computationally adequate model of PolyFPC, an extension of FPC with impredicative polymorphism. This is the first model of a language with parametric polymorphism, recursive terms and recursive types in a non-linear setting.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. Abadi, M., Plotkin, G.D.: A per model of polymorphism and recursive types. In: 5th Annual IEEE Symposium on Logic in Computer Science, pp. 355–365. IEEE Computer Society Press, Los Alamitos (1990)

    Chapter  Google Scholar 

  2. Barber, A.: Linear Type Theories, Semantics and Action Calculi. PhD thesis, Edinburgh University (1997)

    Google Scholar 

  3. Benton, P.N.: A mixed linear and non-linear logic: Proofs, terms and models (preliminary report). Technical report, University of Cambridge (1995)

    Google Scholar 

  4. Bierman, G.M., Pitts, A.M., Russo, C.V.: Operational properties of Lily, a polymorphic linear lambda calculus with recursion. In: Fourth International Workshop on Higher Order Operational Techniques in Semantics, Montréal, sep 2000. Electronic Notes in Theoretical Computer Science, vol. 41, Elsevier, Amsterdam (2000)

    Google Scholar 

  5. Birkedal, L., Møgelberg, R.E.: gelberg,Categorical models of Abadi-Plotkin’s logic for parametricity. Mathematical Structures in Computer Science 15(4), 709–772 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  6. Birkedal, L., Møgelberg, R.E., Petersen, R.L.: Category theoretic models of linear Abadi & Plotkin logic. Submitted

    Google Scholar 

  7. Birkedal, L., Møgelberg, R.E., Petersen, R.L.: Domain theoretic models of parametric polymorphism. Submitted

    Google Scholar 

  8. Birkedal, L., Møgelberg, R.E., Petersen, R.L.: Linear Abadi & Plotkin logic. Submitted

    Google Scholar 

  9. Birkedal, L., Møgelberg, R.E., Petersen, R.L.: Parametric domain-theoretic models of linear Abadi & Plotkin logic, Submitted (2005)

    Google Scholar 

  10. Birkedal, L., Møgelberg, R.E., Petersen, R.L.: Parametric domain-theoretic models of polymorphic intuitionistic / linear lambda calculus. In: Proceedings of the Twenty-first Conference on the Mathematical Foundations of Programming Semantics, To appear (2005)

    Google Scholar 

  11. Birkedal, L., Petersen, R.L., Møgelberg, R.E., Varming, C.: Operational semantics and models of linear Abadi-Plotkin logic. Manuscript

    Google Scholar 

  12. Fiore, M.: Axiomatic Domain Theory in Categories of Partial Maps. Distinguished Dissertations in Computer Science. Cambridge University Press, Cambridge (1996)

    Book  MATH  Google Scholar 

  13. Freyd, P.J.: Algebraically complete categories. In: Carboni, A., Pedicchio, M.C., Rosolini, G. (eds.) Category Theory. Proceedings, Como 1990. Lecture Notes in Mathematics, vol. 1488, pp. 95–104. Springer, Heidelberg (1990)

    Google Scholar 

  14. Freyd, P.J.: Recursive types reduced to inductive types. In: Proceedings of the fifth IEEE Conference on Logic in Computer Science, pp. 498–507 (1990)

    Google Scholar 

  15. Freyd, P.J.: Remarks on algebraically compact categories. In: Fourman, M.P., Johnstone, P.T., Pitts, A.M. (eds.) Applications of Categories in Computer Science. Proceedings of the LMS Symposium, Durham 1991. London Mathematical Society Lecture Note Series, vol. 177, pp. 95–106. Cambridge University Press, Cambridge (1991)

    Google Scholar 

  16. Girard, J.-Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  17. Johann, P., Voigtländer, J.: Free theorems in the presence of seq. In: Proc. of 31st ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL 2004, Venice, Italy, 14–16 Jan. 2004, pp. 99–110. ACM Press, New York (2004)

    Chapter  Google Scholar 

  18. Maneggia, P.: Models of Linear Polymorphism. PhD thesis, University of Birmingham (Feb 2004)

    Google Scholar 

  19. Maraist, Odersky, Turner, Wadler.: Call-by-name, call-by-value, call-by-need and the linear lambda calculus. TCS: Theoretical Computer Science 228, 175–210 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  20. Møgelberg, R.E.: Categorical and domain theoretic models of parametric polymorphism. PhD thesis, IT University of Copenhagen (2005)

    Google Scholar 

  21. Pitts, A.M.: Typed operational reasoning. In: Pierce, B.C. (ed.) Advanced Topics in Types and Programming Languages. chapter 7, pp. 245–289. MIT Press, Cambridge (2005)

    Google Scholar 

  22. Pitts, A.M.: Relational properties of domains. Information and Computation 127, 66–90 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  23. Plotkin, G.D.: Type theory and recursion (extended abstract). In: Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science, Montreal, Canada, 19–23 June 1993, p. 374. IEEE Computer Society Press, Los Alamitos (1993)

    Chapter  Google Scholar 

  24. Plotkin, G.D.: Lectures on predomains and partial functions. In: Notes for a course given at the Center for the Study of Language and Information, Stanford (1985)

    Google Scholar 

  25. Plotkin, G.D.: Second order type theory and recursion, February 1993. Notes for a talk at the Scott Fest (1993)

    Google Scholar 

  26. Plotkin, G., Abadi, M.: A logic for parametric polymorphism. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 361–375. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  27. Reynolds, J.C.: Types, abstraction, and parametric polymorphism. Information Processing 83, 513–523 (1983)

    Google Scholar 

  28. Tse, S., Zdancewic, S.: Translating dependency into parametricity. j-SIGPLAN 39(9), 115–125 (2004)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DISI, Università di Genova,  

    Rasmus Ejlers Møgelberg

Authors
  1. Rasmus Ejlers Møgelberg
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università Ca’ Foscari, Venice,  

    Michele Bugliesi

  2. Interdisciplinary Institute for BroadBand Technology (IBBT), Belgium

    Bart Preneel

  3. ECS, University of Southampton, UK

    Vladimiro Sassone

  4. FB Informatik, LS2, Univ. Dortmund, 44221, Dortmund, Germany

    Ingo Wegener

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Møgelberg, R.E. (2006). Interpreting Polymorphic FPC into Domain Theoretic Models of Parametric Polymorphism. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds) Automata, Languages and Programming. ICALP 2006. Lecture Notes in Computer Science, vol 4052. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11787006_32

Download citation

  • DOI: https://doi.org/10.1007/11787006_32

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-35907-4

  • Online ISBN: 978-3-540-35908-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation