国立大学法人東北大学電気通信研究所公式ウェブサイト|Research Institute of Electrical Communication Tohoku University

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

研究会名:コンピュータサイエンス研究会
開催日:2010年6月17日(木)15:00~16:30
題目: “A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While”
講師:Keiko Nakata氏 (Institute of Cybernetics, Tallinn University of Technology)
開催場所:電気情報系3号館206号室


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

コンピュータサイエンス研究会
主査  篠原 歩

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

  • 日時: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.

問い合わせ先

幹事

住井 英二郎

E-MAIL:sumiiecei.tohoku.ac.jp

内線:7526(青葉山)