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