Modeling Reachability Types with Logical Relations - Semantic Type Soundness, Termination, Effect Safety, and Equational Theory

Explore a conference presentation that introduces an alternative semantic model for reachability types using logical relations, extending Rust-style memory reasoning to higher-level programming languages. Learn how this research addresses limitations in current techniques by providing comprehensive support for higher-order functions, parametric types, and shared mutable state. Discover the framework's four key contributions: semantic type soundness that encompasses even syntactically ill-typed code fragments, termination properties in the presence of higher-order mutable references, effect safety guarantees including the absence of observable mutation, and program equivalence principles that enable safe reordering of non-interfering expressions for parallelization and compiler optimization. Examine how logical relations provide a more robust foundation for understanding reachability types compared to traditional syntactic approaches of progress and preservation, offering deeper insights into memory safety and program behavior in functional programming contexts with mutable state.