Thu 20 Jan 2022 13:30 - 13:55 at Salon I - Types Chair(s): Stephanie Weirich

We extend classic union and intersection type systems with a type-case construction and show that the combination of the union elimination rule of the former and the typing rules for type-cases of our extension encompasses occurrence typing. The latter is a typing technique that takes into account the result of type tests to assign different types to the same expression when it occurs in different branchings of the test. To apply this system in practice, we define a canonical form for the expressions of our extension, called MSC-form. We show that an expression of the extension is typable if and only if its MSC-form is, and reduce the problem of typing the latter to the one of reconstructing annotations for that term. We provide a sound algorithm that performs this reconstruction and a proof-of-concept implementation.

Thu 20 Jan

Displayed time zone: Eastern Time (US & Canada) change

13:30 - 14:45
TypesPOPL at Salon I
Chair(s): Stephanie Weirich University of Pennsylvania
13:30
25m
Research paper
On Type-Cases, Union Elimination, and Occurrence TypingInPerson
POPL
Giuseppe Castagna CNRS; Université de Paris, Mickaël Laurent Université de Paris, Kim Nguyễn Université Paris-Saclay, Matthew Lutze Université de Paris
DOI Media Attached
13:55
25m
Research paper
Oblivious Algebraic Data TypesInPerson
POPL
Qianchuan Ye Purdue University, Benjamin Delaware Purdue University
DOI Media Attached
14:20
25m
Research paper
SolType: Refinement Types for Arithmetic Overflow in SolidityRemote
POPL
Bryan Tan University of California at Santa Barbara, Benjamin Mariano University of Texas at Austin, Shuvendu K. Lahiri Microsoft Research, Işıl Dillig University of Texas at Austin, Yu Feng University of California at Santa Barbara
DOI Media Attached