Skip to main content
SpringerLink
Log in

Polymorphic Intersection Type Assignment for Rewrite Systems with Abstraction and β-Rule

  • Conference paper
  • First Online:
Types for Proofs and Programs (TYPES 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1956))

Included in the following conference series:

Abstract

We define two type assignment systems for first-order rewriting extended with application, λ-abstraction, and β-reduction, using a combination of (ω-free) intersection types and second-order polymorphic types. The first system is the general one, for which we prove subject reduction, and strong normalisation of typeable terms. The second is a decidable subsystem of the first, by restricting to Rank 2 (intersection and quantified) types. For this system we define, using an extended notion of unification, a notion of principal typing which is more general than ML’s principal type property, since also the types for the free variables of terms are inferred.

Partially supported by MURST COFIN’99 TOSCA Project.

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. S. van Bakel. Complete restrictions of the Intersection Type Discipline. TCS, 102(1):135–163, 1992.

    Article  MathSciNet  MATH  Google Scholar 

  2. S. van Bakel. Principal type schemes for the Strict Type Assignment System. Logic and Computation, 3(6):643–670, 1993.

    Article  MathSciNet  MATH  Google Scholar 

  3. S. van Bakel. Intersection Type Assignment Systems. TCS, 151(2):385–435, 1995.

    Article  MathSciNet  MATH  Google Scholar 

  4. S. van Bakel. Rank 2 Intersection TypeAssignment in Term Rewriting Systems. Fundamenta Informaticae, 2(26):141–166, 1996.

    MATH  Google Scholar 

  5. S. van Bakel, F. Barbanera, and M. Fernández. Rewrite Systems with Abstraction and β-rule: Types, Approximants and Normalization. In ESOP’96, LNCS1058, pages 387–403. Springer-Verlag, 1996.

    Google Scholar 

  6. S. van Bakel and M. Fernández. Normalization Results for Typeable Rewrite Systems. I&C 133(2):73–116, 1997.

    Google Scholar 

  7. F. Barbanera and M. Fernández. Intersection Type Assignment Systems with Higher-Order Algebraic Rewriting. TCS 170:173–207, 1996.

    Article  MathSciNet  MATH  Google Scholar 

  8. F. Barbanera, M. Fernández, and H. Geuvers. Modularity of Strong Normalization and Confluence in the Algebraic λ-cube. In LICS’ 94, 1994.

    Google Scholar 

  9. H. Barendregt. The Lambda Calculus: its Syntax and Semantics. North-Holland, Amsterdam, revised edition, 1984.

    Google Scholar 

  10. H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. J. of Symbolic Logic, 48(4):931–940, 1983.

    Article  MathSciNet  MATH  Google Scholar 

  11. V. Breazu-Tannen. Combining algebra and higher-order types. In LICS’ 88, 1988.

    Google Scholar 

  12. V. Breazu-Tannen and J. Gallier. Polymorphic rewriting conserves algebraic strong normalization. TCS 83(1):3–28, 1991.

    Article  MATH  Google Scholar 

  13. V. Breazu-Tannen and J. Gallier. Polymorphic rewriting conserves algebraic confluence. I&C 82:3–28, 1992.

    Google Scholar 

  14. A. Bucciarelli, S. De Lorenzis, A. Piperno, I. Salvo. Some Computational Properties of Intersection Types (Extended Abstract). In LICS’ 99, pages 109–118, 1999.

    Google Scholar 

  15. L.M.M. Damas. Type Assignment in Programming Languages. PhD Thesis, University of Edinburgh, 1984.

    Google Scholar 

  16. N. Dershowitz and J.P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 6, pages 245–320. North-Holland, 1990.

    Google Scholar 

  17. D. J. Dougherty. Adding algebraic rewriting to the untyped lambda calculus. Information and Computation, 101, 251–267 (1992).

    Article  MathSciNet  MATH  Google Scholar 

  18. M Fernández. Type Assignment and Termination of Interaction Nets. Mathematical Structures in Computer Science, 8:593–636, 1998.

    Article  MathSciNet  MATH  Google Scholar 

  19. M. Fernández and J.P. Jouannaud. Modular termination of term rewriting systems revisited. In LNCS 906, pages 255–272. Springer-Verlag, 1994.

    Google Scholar 

  20. J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

    Google Scholar 

  21. J.Y. Girard. The System F of Variable Types, Fifteen years later. TCS 45:159–192, 1986.

    Article  MathSciNet  MATH  Google Scholar 

  22. B. Jacobs, I. Margaria, and M. Zacchi. Filter models with polymorphic types. TCS 95:143–158, 1992.

    Article  MathSciNet  MATH  Google Scholar 

  23. T. Jim. What are principal typings and what are they good for? In Proc. POPL’96, ACM Symposium on Principles of Programming Language, 1996.

    Google Scholar 

  24. J.P. Jouannaud and M. Okada. Executable higher-order algebraic specification languages. In LICS’ 91, pages 350–361, 1991.

    Google Scholar 

  25. A.J. Kfoury and J. Tiuryn. Type reconstruction in finite-rank fragments of the second-order λ-calculus. I&C 98(2):228–257, 1992.

    Google Scholar 

  26. A.J. Kfoury and J.B. Wells. A Direct Algorithm for Type Inference in the Rank-2 Fragment of the Second-Order λ-Calculus. In LFP’94, 1994.

    Google Scholar 

  27. A.J. Kfoury and J.B. Wells. Principality and decidable type inference for finite-rank intersection types. In Proc. 26th ACM Symp. Principles of Prog. Languages, POPL’ 99, pages 161–174, 1999.

    Google Scholar 

  28. J.W. Klop. Term Rewriting Systems. In S. Abramsky, Dov.M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, chapter 1, pages 1–116. Clarendon Press, 1992.

    Google Scholar 

  29. J. Launchbury and S.L. Peyton Jones. Lazy functional state threads. In Proc. ACM SIGPLAN’94 Conference on Programming Language Design and Implementation, 1994.

    Google Scholar 

  30. I. Margaria and M. Zacchi. Principal Typing in a ∀∩-Discipline. Logic and Computation, 5(3):367–381, 1995.

    Article  MathSciNet  MATH  Google Scholar 

  31. M.H.A. Newman. On theories with a combinatorial definition of ‘equivalence’. Ann. Math., 43:223–243, 1942.

    Article  MathSciNet  MATH  Google Scholar 

  32. E.G.J.M.H. Nöcker, J.E.W. Smetsers, M.C.J.D. van Eekelen, and M.J. Plasmeijer. Concurrent Clean. In PARLE’ 91, LNCS 506-II, pages 202–219. Springer-Verlag, 1991.

    Google Scholar 

  33. J.A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23–41, 1965.

    Article  MathSciNet  MATH  Google Scholar 

  34. S.Ronchi Della Rocca and B. Venneri. Principal type schemes for an extended type theory. TCS 28:151–169, 1984.

    Article  MathSciNet  MATH  Google Scholar 

  35. H. Yokohuchi. Embedding a Second-Order Type System into an Intersection Type System. I&C 117:206–220, 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing, Imperial College, 180 Queen’s Gate, London, SW7 2BZ, UK

    Steffen van Bakel

  2. Dipartimento di Matematica e Informatica, Universitá degli Studi di Catania, Viale A. Doria 6, 95125, Catania, Italia

    Franco Barbanera

  3. LIENS (CNRS UMR 8548), École Normale Supérieure, 45, rue d’Ulm, 75005, Paris, France

    Maribel Fernández

Authors
  1. Steffen van Bakel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Franco Barbanera
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Maribel Fernández
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing Science, Chalmers University of Technology and University of Göteborg, 41296, Göteborg, Sweden

    Thierry Coquand , Peter Dybjer , Bengt Nordström  & Jan Smith , ,  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

van Bakel, S., Barbanera, F., Fernández, M. (2000). Polymorphic Intersection Type Assignment for Rewrite Systems with Abstraction and β-Rule. In: Coquand, T., Dybjer, P., Nordström, B., Smith, J. (eds) Types for Proofs and Programs. TYPES 1999. Lecture Notes in Computer Science, vol 1956. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44557-9_3

Download citation

  • DOI: https://doi.org/10.1007/3-540-44557-9_3

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41517-6

  • Online ISBN: 978-3-540-44557-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation