Wed 23 Oct 2024 16:20 - 16:40 at San Gabriel - Formal Methods 2 Chair(s): Bor-Yuh Evan Chang

Compositional programming is a programming paradigm that emphasizes modularity and is implemented in the CP programming language. The foundations for compositional programming are based on a purely functional variant of System F with intersection types, called Fi+, which includes distributivity rules for subtyping.

This paper shows how to extend compositional programming and CP with mutable references, enabling a modular, imperative compositional programming style. A technical obstacle solved in our work is the interaction between distributive intersection subtyping and mutable references. Davies and Pfenning [2000] studied this problem in standard formulations of intersection type systems and argued that, when combined with references, distributive subtyping rules lead to type unsoundness. To recover type soundness, they proposed dropping distributivity rules in subtyping. CP cannot adopt this solution, since it fundamentally relies on distributivity for modularity. Therefore, we revisit the problem and show that, by adopting bidirectional typing, a more lightweight and type sound restriction is possible: we can simply restrict the typing rule for references. This solution retains distributivity and an unrestricted intersection introduction rule. We present a first calculus, based on Davies and Pfenning’s work, which illustrates the generality of our solution. Then we present an extension of Fi+ with references, which adopts our restriction and enables imperative compositional programming. We implement an extension of CP with references and show how to model a modular live-variable analysis in CP. Both calculi and their proofs are formalized in the Coq proof assistant.

Wed 23 Oct

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

16:00 - 17:40
Formal Methods 2OOPSLA 2024 at San Gabriel
Chair(s): Bor-Yuh Evan Chang University of Colorado Boulder & Amazon
16:00
20m
Talk
A Constraint Solving Approach to Parikh Images of Regular Languages
OOPSLA 2024
Amanda Stjerna Uppsala university, Philipp Rümmer University of Regensburg and Uppsala University
DOI
16:20
20m
Talk
Imperative Compositional Programming: Type Sound Distributive Intersection Subtyping with References via Bidirectional Typing
OOPSLA 2024
Wenjia Ye University of Hong Kong, Yaozhu Sun University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
DOI
16:40
20m
Talk
Inductive diagrams for causal reasoning
OOPSLA 2024
Jonathan Castello University of California, Santa Cruz, Patrick Redmond University of California at Santa Cruz, Lindsey Kuper University of California, Santa Cruz
DOI Pre-print
17:00
20m
Talk
Message-Observing Sessions
OOPSLA 2024
Ryan Kavanagh Université du Québec à Montréal (UQAM), Brigitte Pientka McGill University
DOI
17:20
20m
Talk
Plume: Efficient and Complete Black-box Checking of Weak Isolation Levels
OOPSLA 2024
Si Liu ETH Zurich, Long Gu State Key Laboratory for Novel Software Technology, Nanjing University, Hengfeng Wei State Key Laboratory for Novel Software Technology, Nanjing University, David Basin ETH Zurich
DOI