Law and Order for Typestate with Borrowing
Hannes Saffrich, Yuki Nishida, Peter Thiemann

TL;DR
This paper introduces a novel transition-oriented typestate system for impure functional programming that effectively manages aliasing and borrowing, supported by formal proofs and an implemented typechecker.
Contribution
It presents a new foundation for typestate using ordered types and resource types, supporting flexible borrowing and formalizing the approach with proofs and implementation.
Findings
Proved syntactic type soundness of the system.
Developed an algorithmic type system and proved its soundness.
Implemented a typechecker and interpreter for the language.
Abstract
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 implications. 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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Model-Driven Software Engineering Techniques
