License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2022.8
URN: urn:nbn:de:0030-drops-184513
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18451/
Go to the corresponding LIPIcs Volume Portal

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

Linear Rank Intersection Types

pdf-format:
LIPIcs-TYPES-2022-8.pdf (0.8 MB)

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.

BibTeX - Entry

@InProceedings{reis_et_al:LIPIcs.TYPES.2022.8,
  author =	{Reis, F\'{a}bio and Alves, Sandra and Florido, M\'{a}rio},
  title =	{{Linear Rank Intersection Types}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{8:1--8:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/18451},
  URN =		{urn:nbn:de:0030-drops-184513},
  doi =		{10.4230/LIPIcs.TYPES.2022.8},
  annote =	{Keywords: Lambda-Calculus, Intersection Types, Quantitative Types, Tight Typings}
}

Keywords: Lambda-Calculus, Intersection Types, Quantitative Types, Tight Typings
Collection: 28th International Conference on Types for Proofs and Programs (TYPES 2022)
Issue Date: 2023
Date of publication: 28.07.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI