Logical Reasoning for Higher-Order Functions with Local State


Full Version [pdf-file]

Old Full Version This contains more examples to reason the data structures. (Oct 2006) [pdf-file]


Logics for Imperative Higher-Order Functions with Aliasing and Local State: Thee Completeness Results (Oct 2006) This note provides the proof of three completenes results. [pdf-file]

Recent Logic Papers cited from the Paper [link]