2013年04月25日西田　直樹助教（情報システム学専攻）
組織的な若手研究者等海外派遣プログラム

　私は2012年10月14日から21日までの1週間，本研究科の「組織的な若手研究者海外派遣プログラム」の一環としてインスブルック大学（University ofInnsbruck，オーストリア）のAart Middeldorp教授のグループを訪問し，共同研究を行いました。インスブルックを訪問するのは，Middeldorp教授との縁もあり，今回が3回目でした。インスブルックはアルプス山脈の谷の中にあり，南北に3,000メートル級の山々が壁のようにそびえ立っています。市街地からケーブルカー，ロープウェイを乗り継ぐだけであっという間に3,000メートルの山の頂上に行くことができます。そのため，街の至る場所から雄大な自然を見ることができる都市です。

　インスブルック大学は本学と学術協定を締結しており，さらに平成24年度から本学・酒井正彦教授とMiddeldorp教授をリーダーとして二国間共同研究を行っています。私も二国間共同研究のメンバーであり，その研究テーマである「制約付き書換え」は本グループが近年，成果を挙げている研究分野です。そのため，私は共同研究の主タスクの日本側代表を努めさせていただいており，本訪問でもその共同研究を進めました。さらに，Middeldorp教授のグループが主催する修士課程学生向けのセミナーにて講演も行いました。

　共同研究では私が担当するタスクについてオーストリア側のメンバーであるCynthia Kop研究員と行いました。現在取り組んでいることは制約付き書換えの既存の枠組みすべてを包括し，さらにプログラムをより自然な形式で表現できる制約付き書換えの枠組みの構築です。また，その枠組みで，プログラムの解析などに有用である合流性・停止性を証明する手法を新しい枠組みに移植すること，さらにプログラムの性質を表す等式が帰納的に成立することを証明するための定理自動証明の技術の移植を検討しました。特に，制約付き書換えにおける定理自動証明は最近になって盛んに研究されているテーマであり，本グループで提案した手法は手続き型プログラムの検証において今後の発展が期待される成果です。共同研究ではその成果を基盤として新しい枠組み，および検証技術のその枠組みへの移植における課題を議論しました。1週間という非常に短い滞在期間でしたが，二国間共同研究を7月から本格的に開始しており，9月にはメールにてさまざまな議論をしていたこともあり，今回の滞在ではより深い議論を交わすことができ，非常に有意義な時間を過ごしました。本成果はKop研究員との共著で国際会議に投稿するに至っています。

　二国間共同研究は平成25年度末まで継続され，これからさらに活発に議論を進めていくことになります。今回の派遣はその最初の一歩として非常によいきっかけとなりました。この経験を生かして，国際的な研究拠点を形成できるようより一層，努力していきたいと思います。

• 
  写真：朝の宿舎の窓からの風景