A formalization of Staged Specification Logic for Verifying Higher-Order Imperative Programs (FM 2024). Start here. For shift/reset, start here.