Modeling Reachability Types with Logical Relations -- Semantic Type Soundness,(…)
summary
Presents a formal logical-relations model for reachability types that augments standard relations with relational store typing to localize heap reasoning, and proves a fundamental theorem giving semantic type soundness even for some syntactically ill-typed fragments. Shows termination holds (surprisingly) for higher-order mutable references under the model’s restrictions, establishes effect-qualified reachability types that guarantee absence of observable mutation, and proves program-equivalence rules for reordering non‑interfering computations; proofs and artifacts are available.
AI-written summary · about
chapters (13)
- 0:00Reachability types overview
- 1:09From restrictive to descriptive reachability
- 2:13Rich B types core idea
- 3:39Semantic properties questions
- 4:00Logical relations in lambda calculus
- 5:22Limitations of logical relations
- 6:27Store typing for local reasoning
- 7:31Semantic properties and reachability
- 8:57Qualifier-dependent function types
- 10:23Polymorphism in RB types
- 11:05Effect qualifiers for optimization
- 11:48Summary of semantic model
- 12:49Future work extensions
related talks
40mRelational Reasoning in Object-based Programs
28mReasoning about Distributed Reconfigurable Systems
18mSemantic-Type-Guided Bug Finding
45mWhat do we mean by "unsound"?
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
20mOn Extending Incorrectness Logic with Backwards Reasoning
34mLogic in Computer Science, Engineering and Industry
31mTermination in Concurrency, Revisited