## コンピュータサイエンス研究会 講演会の御案内

コンピュータサイエンス研究会

主査 篠原 歩

下記のようにコンピュータサイエンス研究会の講演会を開催いたしますので，ご案内申し上げます．

- 日 時 ： 2010年6月17日(木) 15:00〜16:30
- 場 所 ： 電気情報系3号館206号室
- 題 目 ： “A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While”

（講演は日本語の予定） - 話 者 ： Keiko Nakata (Institute of Cybernetics, Tallinn University of Technology)
- 概 要 ： In search for a foundational framework for reasoning about observable behavior of programs that may not terminate, we have previously studied a trace-based big-step semantics for the While language. In this semantics, both traces and evaluation (relating initial states of program runs to traces they produce) are defined coinductively. On terminating runs, it agrees with the standard inductive state-based semantics. We then devised a Hoare logic counterpart of our coinductive trace-based semantics and prove it sound and complete.Our logic subsumes both the partial correctness Hoare logic and the total correctness Hoare logic: they are embeddable. Since we work
with a constructive underlying logic, the range of expressible program properties has a rich structure; in particular, we can distinguish
between termination and nondivergence, e.g., unbounded total search fails to be terminating but is nonetheless nondivergent. Our
metatheory is entirely constructive as well, and we have formalized it in Coq.

In this talk, I will present the coinductive trace-based semantics and the Hoare logic, and demonstrate the expressivity of our logic with an example of unbounded total search inspired by Markov’s principle.

I also want to talk about our recent work on the operational semantics of While with interactive input/output, based on resumptions and termination-sensitive weak bisimilarity. This is a step towards concurrency.

- 問い合わせ先
- 幹事: 住井 英二郎 sumii(at)ecei.tohoku.ac.jp 青葉山内線7526