"Extending Refinement Calculus with Separation Logic for Safe Modification of Pointer Programs" (西村 進 氏）

ポインターに関するプログラムで、同じ意味だろうと思って下手に書き換えると、実は文脈によって違った挙動を示してしまうことがあります。では、安全(safe)な書き換えとは何か？西村氏はそれをプログラムをseparation logicの論理式の predicate transformer と見なす refinement calculusの枠組みで定式化（safeな書き換えとはspecificに書き換えることである）した上で、allocation, deallocationなどの基本動作をその枠組みで表現し、それを使用して、いくつかのポインターを含むプログラムの変形がsafeであることを示しました。
refinement calculusは完全な公理化や形式化がされておらず、電話帳のようなルール集があって、それを「適宜使用」して必要な式変形をするとかで。ちゃんとした意味論もない（特にoperationalな意味論がないので、safe性の定義がかなりad hocに見える）とかで、話を聞いていてとにかく大変そうでした。