論文

久しぶりにfirst authorというか単著の論文が通りました。幸い今回はexpertにreviewしてもらえたようで、「現代のプログラミングにfreeは不要」*1とか「簡単すぎる」*2とか「プログラム例がSchemeなので読めない」*3とかいった妙なコメントもなく、最高の評価をいただきました*4。と自画自賛。

http://www.kb.ecei.tohoku.ac.jp/~sumii/pub/non-mono.pdf

We develop a general method of proving contextual properties---including (but not limited to) observational equivalence, space improvement, and memory safety \emph{under arbitrary contexts}---for programs in untyped call-by-value $\lambda$-calculus with ML-like references ($\mathtt{ref}$, $:=$ and $!$) and deallocation ($\mathtt{free}$). The method significantly generalizes Sumii et al.'s environmental bisimulation technique, and gives a sound and complete characterization of each proved property, in the sense that the ``bisimilarity'' (the largest set satisfying the bisimulation-like conditions) equals the set of terms with the property to be proved. We give examples of contextual properties concerning typical data structures such as linked lists, binary search trees, and directed acyclic graphs with reference counts, all with deletion operations that release memory.

This shows the scalability of the environmental approach from contextual equivalence to other binary relations (such as space improvement) and unary predicates (such as memory safety), as well as to languages with non-monotone store, where Kripke-style logical relations have difficulties.

*1:たとえGCがあっても、garbage collectorはメモリを解放しないと駄目でしょ！　イントロの最初の段落でいってるでしょ！

*2:ポインタとfreeがある言語のlogical relationとか、いろんな人が十年（数十年？）ぐらい悩んでる問題だってば。Abstractとrelated workにハッキリ書いたでしょ！

*3:これは本当に愕然とした。念のためにλ式で書き直しましたが…

*4:なぜかページ数制限内なのに「ページ数オーバー」で1点減点(?)されたreview以外。うちの2歳児でも15ぐらい数えられますよ？　Rebuttalで「何かの間違いですよね？」と書いても直らなかったどころか、なぜかconfidenceが0（最低）から3（最高）に上がってたし。もっとも、他のreviewにも「内容がありすぎて、appendixがないとわかりにくいが、それはページ数制限が悪いのであって、著者は最善を尽くしている」とか口を揃えて書かれていましたが。他にも似たような例は多いようで、「採択論文数を減らしてでもページ数制限を緩和すべきだと思いますか？」みたいなアンケートが著者に来ていました。