Staged Specification Logic for Verifying Higher-Order Imperative Programs (Technical Report)

Darius Foo, Yahui Song, Wei-Ngan Chin

Higher-order functions and imperative states are language features supported by many mainstream languages. Their combination is expressive and useful, but complicates specification…