This program is tentative and subject to change.
Typestate systems are notoriously complex as they require sophisticated machinery for tracking aliasing. We propose a new, transition-oriented foundation for typestate in the setting of impure functional programming. Our approach relies on ordered types for simple alias tracking and its formalization draws on work on bunched implication. Yet, we support a flexible notion of borrowing in the presence of typestate.
Our core calculus comes with a notion of resource types indexed by an ordered partial monoid that models abstract state transitions. We prove syntactic type soundness with respect to a resource-instrumented semantics. We give an algorithmic version of our type system and prove its soundness. Algorithmic typing facilitates a simple surface language that does not expose tedious details of ordered types. We implemented a typechecker for the surface language along with an interpreter for the core language.
This program is tentative and subject to change.
Wed 23 OctDisplayed time zone: Pacific Time (US & Canada) change
10:40 - 12:20 | Ownership, Security, and PrivacyOOPSLA 2024 at IBR West Chair(s): Tobias Wrigstad Uppsala University | ||
10:40 20mTalk | Law and Order for Typestate with Borrowing OOPSLA 2024 Hannes Saffrich University of Freiburg, Yuki Nishida Tohoku University, Peter Thiemann University of Freiburg, Germany | ||
11:00 20mTalk | Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation OOPSLA 2024 | ||
11:20 20mTalk | Gradient: Gradual Compartmentalization via Object Capabilities Tracked in Types OOPSLA 2024 Aleksander Boruch-Gruszecki EPFL, Adrien Ghosn Microsoft Research, Mathias Payer EPFL, Clément Pit-Claudel EPFL | ||
11:40 20mTalk | Automatically Reducing Privilege for Access Control Policies OOPSLA 2024 Loris D'Antoni University of Wisconsin-Madison, Shuo Ding Georgia Institute of Technology, Amit Goel AWS, Mathangi Ramesh Amazon Web Services, Neha Rungta Amazon Web Services, Chungha Sung Amazon Web Services, USA | ||
12:00 20mTalk | Functional Ownership through Fractional Uniqueness OOPSLA 2024 DOI |