Fri 25 Oct 2024 13:50 - 14:10 at Pasadena - Types and Gradual Typing 2 Chair(s): Fabian Muehlboeck

Data races have long been a notorious problem in concurrent programming. They are subtle to detect, and lead to non-deterministic behaviours. There has been a lot of interest in type systems that statically guarantee data race freedom. Significant progress has been made in this area, and these type systems are increasingly usable and practical. However, their adoption in mainstream programming languages is still limited, which is largely attributed to their strict alias prevention principles that obstruct the usage of existing programming patterns. This is a deterrent to the migration of existing code bases. To tackle this problem, we propose Capture Separation Calculus (System CSC), which statically prevents data races while being compatible with established programming patterns. It follows a \emph{control-as-you-need} philosophy: by default, aliases are allowed, but they are tracked in the type system. When data races are a concern, the tracked aliases are controlled to prevent data-race-prone patterns. We study the formal properties of System CSC. Type soundness is proven via the standard progress and preservation theorems. Additionally, we formally verify the data race freedom property of System CSC by proving that the reduction of a well-typed program is confluent.

Fri 25 Oct

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

13:50 - 15:30
Types and Gradual Typing 2OOPSLA 2024 at Pasadena
Chair(s): Fabian Muehlboeck Australian National University
13:50
20m
Talk
Degrees of Separation: A Flexible Type System for Safe Concurrency
OOPSLA 2024
DOI
14:10
20m
Talk
Full Iso-recursive Types
OOPSLA 2024
Litao Zhou University of Hong Kong, Qianyong Wan The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
DOI
14:30
20m
Talk
Gradually Typed Languages Should Be Vigilant!
OOPSLA 2024
Olek Gierczak Northeastern University, Lucy Menon Northeastern University, Christos Dimoulas Northwestern University, Amal Ahmed Northeastern University, USA
DOI
14:50
20m
Talk
Merging Gradual Typing
OOPSLA 2024
Wenjia Ye National University of Singapore, Bruno C. d. S. Oliveira University of Hong Kong, Matías Toro University of Chile
DOI
15:10
20m
Talk
Persimmon: Nested Family Polymorphism with Extensible Variant Types
OOPSLA 2024
Anastasiya Kravchuk-Kirilyuk Harvard University, Gary Feng University of Waterloo, Jonas Iskander Harvard University, Yizhou Zhang University of Waterloo, Nada Amin Harvard University
DOI