A Typed Lambda Calculus with Gradual Intersection Types

• Type: Article in International Conference Proceedings Book
• Date: 2022

Authors

Ângelo, P (Author) Other; Florido, M (Author) FCUP

Conference proceedings International

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

Pages: 9:1-9:13

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

20 September 2022 through 22 September 2022

Indexing

ISI Web of Science

Scopus

Other information

Authenticus ID: 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.

Language: English

Type (Professor's evaluation): Scientific