Document Open Access Logo

Linear Rank Intersection Types

Authors Fábio Reis , Sandra Alves , Mário Florido

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2022.8.pdf
  • Filesize: 0.76 MB
  • 21 pages

Document Identifiers

Author Details

Fábio Reis
  • DCC-FCUP, University of Porto, Portugal
  • LIACC - Artificial Intelligence and Computer Science Laboratory, University of Porto, Portugal
Sandra Alves
  • DCC-FCUP, University of Porto, Portugal
  • LIACC - Artificial Intelligence and Computer Science Laboratory, University of Porto, Portugal
  • CRACS, INESC-TEC - Centre for Research in Advanced Computing Systems, Porto, Portugal
Mário Florido
  • DCC-FCUP, University of Porto, Portugal
  • LIACC - Artificial Intelligence and Computer Science Laboratory, University of Porto, Portugal

Funding

  • Reis, Fábio: This work was partially financially supported by Base Funding - UIDB/00027/2020 of the Artificial Intelligence and Computer Science Laboratory - LIACC - funded by national funds through the FCT/MCTES (PIDDAC).
  • Alves, Sandra: Partially supported by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia, within project LA/P/0063/2020.
  • Florido, Mário: This work was partially financially supported by Base Funding - UIDB/00027/2020 of the Artificial Intelligence and Computer Science Laboratory - LIACC - funded by national funds through the FCT/MCTES (PIDDAC).

Cite As Get BibTex

Fábio Reis, Sandra Alves, and Mário Florido. Linear Rank Intersection Types. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 8:1-8:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.TYPES.2022.8

Abstract

Non-idempotent intersection types provide quantitative information about typed programs, and have been used to obtain time and space complexity measures. Intersection type systems characterize termination, so restrictions need to be made in order to make typability decidable. One such restriction consists in using a notion of finite rank for the idempotent intersection types. In this work, we define a new notion of rank for the non-idempotent intersection types. We then define a novel type system and a type inference algorithm for the λ-calculus, using the new notion of rank 2. In the second part of this work, we extend the type system and the type inference algorithm to use the quantitative properties of the non-idempotent intersection types to infer quantitative information related to resource usage.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Lambda-Calculus
  • Intersection Types
  • Quantitative Types
  • Tight Typings

Metrics

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

Related Versions

References

  1. Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. Tight typings and split bounds. Proc. ACM Program. Lang., 2(ICFP), July 2018. URL: https://doi.org/10.1145/3236789.
  2. H. P. Barendregt. Lambda calculi with types. In Handbook of Logic in Computer Science (Vol. 2): Background: Computational Structures, pages 117-309. Oxford University Press, Inc., 1993. Google Scholar
  3. Hendrik Pieter Barendregt. The Lambda Calculus - Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1985. Google Scholar
  4. Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambda-calculus. Log. J. IGPL, 25(4):431-464, 2017. Google Scholar
  5. Alonzo Church. A formulation of the simple theory of types. The Journal of Symbolic Logic, 5(2):56-68, 1940. URL: http://www.jstor.org/stable/2266170.
  6. M. Coppo and M. Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. Notre Dame Journal of Formal Logic, 21(4):685-693, October 1980. URL: https://doi.org/10.1305/ndjfl/1093883253.
  7. Mario Coppo. An extended polymorphic type system for applicative languages. In Piotr Dembinski, editor, Mathematical Foundations of Computer Science 1980 (MFCS'80), Proceedings of the 9th Symposium, Rydzyna, Poland, September 1-5, 1980, volume 88 of Lecture Notes in Computer Science, pages 194-204. Springer, 1980. Google Scholar
  8. H. B. Curry. Functionality in combinatory logic. Proceedings of the National Academy of Sciences, 20(11):584-590, 1934. URL: https://doi.org/10.1073/pnas.20.11.584.
  9. Haskell Brooks Curry, Robert Feys, William Craig, J Roger Hindley, and Jonathan P Seldin. Combinatory Logic, volume 1. North-Holland Amsterdam, 1958. Google Scholar
  10. Luis Damas and Robin Milner. Principal type-schemes for functional programs. In Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '82, pages 207-212, New York, NY, USA, 1982. Association for Computing Machinery. URL: https://doi.org/10.1145/582153.582176.
  11. Ferruccio Damiani. Rank 2 intersection for recursive definitions. Fundamenta Informaticae, 77(4):451-488, 2007. Google Scholar
  12. Daniel de Carvalho. Sémantiques de la logique linéaire et temps de calcul. Phd thesis, Université Aix-Marseille II, 2007. Google Scholar
  13. Andrej Dudenhefner and Jakob Rehof. Intersection type calculi of bounded dimension. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL '17, pages 653-665, New York, NY, USA, 2017. Association for Computing Machinery. URL: https://doi.org/10.1145/3009837.3009862.
  14. Andrej Dudenhefner and Jakob Rehof. Typability in bounded dimension. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-12, 2017. URL: https://doi.org/10.1109/LICS.2017.8005127.
  15. Mário Florido and Luís Damas. Linearization of the lambda-calculus and its relation with intersection type systems. J. Funct. Program., 14(5):519-546, 2004. URL: https://doi.org/10.1017/S0956796803004970.
  16. Philippa Gardner. Discovering needed reductions using type theory. In TACS, volume 789 of LNCS, pages 555-574. Springer, 1994. Google Scholar
  17. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  18. Trevor Jim. Rank 2 type systems and recursive definitions. Massachusetts Institute of Technology, Cambridge, MA, 1995. Google Scholar
  19. A. J. Kfoury and J. B. Wells. Principality and decidable type inference for finite-rank intersection types. In POPL '99, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 161-174. ACM, 1999. Google Scholar
  20. Assaf Kfoury. A linearization of the lambda-calculus and consequences. Journal of Logic and Computation, 10(3):411-436, 2000. Google Scholar
  21. Daniel Leivant. Polymorphic type inference. In Proceedings of the 10th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), pages 88-98, 1983. Google Scholar
  22. Alberto Martelli and Ugo Montanari. An efficient unification algorithm. ACM Trans. Program. Lang. Syst., 4:258-282, 1982. Google Scholar
  23. Fábio Reis, Sandra Alves, and Mário Florido. Linear rank intersection types. In 28th International Conference on Types for Proofs and Programs (TYPES 2022), 2022. URL: https://types22.inria.fr/files/2022/06/TYPES_2022_paper_33.pdf.
  24. J. A. Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12(1):23-41, January 1965. URL: https://doi.org/10.1145/321250.321253.
  25. Pawel Urzyczyn. The emptiness problem for intersection types. The Journal of Symbolic Logic, 64(3):1195-1215, 1999. Google Scholar
  26. Steffen van Bakel. Intersection type disciplines in lambda calculus and applicative term rewriting systems. Phd thesis, Mathematisch Centrum, Katholieke Universiteit Nijmegen, 1993. Google Scholar
  27. Steffen van Bakel. Rank 2 intersection type assignment in term rewriting systems. Fundam. Informaticae, 26(2):141-166, 1996. 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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact