Linear Rank Intersection Types

• Tipo: Artigo em Livro de Atas de Conferência Internacional
• Data: 2022

Autores

Reis, F (Autor) Outra; Sandra Alves (Autor) FCUP; Florido, M (Autor) FCUP

Ata de Conferência Internacional

Título: 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France

Páginas: 8:1-8:21

28th International Conference on Types for Proofs and Programs, TYPES 2022

Nantes, 20 June 2022 through 25 June 2022

Indexação

Scopus - 0 Citações

Outras Informações

ID Authenticus: P-00Y-5J4

DOI: 10.4230/lipics.types.2022.8

Abstract (EN): 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. © Fábio Reis, Sandra Alves, and Mário Florido.

Idioma: Inglês

Tipo (Avaliação Docente): Científica