日時：
2006年2月24日 17：00〜19：00
場所：
三田東宝ビル８F人文COE会議室
（＊場所等不明な方は慶大正門のガードマンにお尋ね下さい）
(JR田町駅または都営地下鉄三田駅または赤羽橋駅（大江戸線）から
徒歩5分)
＊建物の入口が常時ロックされておりますので，
ドア脇のインターホンにて7Fの事務室又は8Fをお呼び出し下さい．
アブストラクト： If you have a program and run it, then it usually shows some behaviour. This may take the form of interactions with a display, a printer, or communication ports. More closely, its main interactions may be with an operating system, libraries and other software. Anyway it has a certain behaviour, which can be useful, can be disastrous, can be enjoyable, or can be all of these three, for example.
A program logic allows us to describe such software behaviour using logical assertions. It may also enable syntactic derivation of valid assertions. Such a logic may as well have a semantic basis, in the sense that its assertions discuss all and only observable behaviour of programs. One of the well-known logics with this property is Hoare's logic for first-order imperative programs, developed on the basis of Floyd's assertion method.
This talk is about an extension of Hoare logic to higher-order procedures and general forms of aliasing. Extending Hoare logic with these features has been one of the subtle open issues for decades: this work uses ideas from the pi-calculus, a basic calculus for communicating processes, to develop such an extension. The logic allows clean and general description of higher-order behaviour with aliasing, and is observationally complete in the sense that two programs are observationally indistinguishable if and only if they satisfy the same set of assertions. In this talk, I will illustrate core ideas of the logic using simple examples, position it among related works, and discuss further topics. If time allows, we shall also discuss practical and theoretical issues in applying such logics and related technologies for making software safe and secure, a concern of increasing urgency in modern society.
問合せ先：
慶應義塾大学 文学部 岡田 光弘
住所：東京都港区三田 3-1-7 三田東宝ビル 8F
e-mail：philosophy at abelard.flet.keio.ac.jp