Alberto Ciaffaglione, Luigi Liquori, Marino Miculan. Reasoning on an imperative object-based calculus in Higher Order Abstract Syntax. In Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003. ACM, 2003. [doi]
Abstract is missing.