A Typed Lambda Calculus with Gradual Intersection Types

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

Autores

Ângelo, P (Autor) Outra; Florido, M (Autor) FCUP

Ata de Conferência Internacional

Título: PPDP 2022: 24th International Symposium on Principles and Practice of Declarative Programming, Tbilisi, Georgia, September 20 - 22, 2022

Páginas: 9:1-9:13

24th International Symposium on Principles and Practice of Declarative Programming, PPDP 2022

20 September 2022 through 22 September 2022

Indexação

ISI Web of Science

Scopus

Outras Informações

ID Authenticus: P-00X-9KR

DOI: 10.1145/3551357.3551382

Abstract (EN): Intersection types have the power to type expressions which are all of many different types. Gradual types combine type checking at both compile-time and run-time. Here we combine these two approaches in a new typed calculus that harness both of their strengths. We incorporate these two contributions in a single typed calculus and define an operational semantics with type cast annotations. We also prove several crucial properties of the type system, namely that types are preserved during compilation and evaluation, and that the refined criteria for gradual typing holds. © 2022 ACM.

Idioma: Inglês

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