論文2本同時執筆
IPSJ-PRO以来＆今回は英文。年末年始のダンピング労働の結果です。さすがに疲れたので今日は休暇をいただいて、子供二人＆家内と三井アウトレットパーク仙台港でショッピングでした。
内容は例によって「理論的」（基礎的）ですが、従来は極めて取り扱いの難しかった問題２つを簡単に扱うことができたと考えています。
A Complete Characterization of Observational Equivalence in Polymorphic lambda-Calculus with General References.
Eijiro Sumii.
http://www.kb.ecei.tohoku.ac.jp/~sumii/pub/poly-ref.pdf
Abstract: We give a (sound and complete) characterization of observational equivalence in full polymorphic $\lambda$-calculus with existential types and first-class, higher-order references. Our method is syntactic and elementary in the sense that it only employs simple structures such as relations on terms. It is nevertheless powerful enough to prove many interesting equivalences that can and cannot be proved by previous approaches, including the latest work by Ahmed, Dreyer and Rossberg (to appear in POPL 2009).
A Higher-Order, Call-By-Value Applied Pi-Calculus.
Nobuyuki Sato and Eijiro Sumii.
http://www.kb.ecei.tohoku.ac.jp/~sumii/pub/hoapp.pdf
Abstract: We define a higher-order process calculus with algebraic operations such as encryption and decryption, and develop a bisimulation proof method for behavioral equivalence in this calculus. Such development has been notoriously difficult because of the subtle interactions among generative names, processes as data, and the algebraic operations. We handle them by carefully defining the calculus and adopting Sumii et al.'s environmental bisimulation, and thereby give (to our knowledge) the first ``useful'' proof method in this setting. We demonstrate the utility of our method through examples involving both higher-order processes and asymmetric cryptography.
