"A new project on formalizing specifications"

現在従事中のプロジェクトについて45分間発表。

In this talk we introduce a new on-going research project (jointly with several companies) for developing a methodology and software tools that can improve the upper development scene of software product.
This aims to formalize a unified form of specifications of Embedded Software in a proof assistant system Agda, and develop tools which assist in writing such formalized specifications.

出来は少し悪い程度、聴衆の方々が非常に好意的で、とても助かりました。
S氏から「Agdaで仕様書を記述する場合の例を見せてくれ」といわれ、日本語の電気ポットの仕様書の状態遷移図をagdaで表現したものを見せたところ、皆「この日本語の意味は」とかを聞き始め、「日本のkettleはハイテクなんだ」とかいう結論になりました（イギリスのelectronic kettleは、コンセントを指したら沸騰させるだけ）。

その後、O氏とパブで夕食、ソーセージ＆マッシュを食べる。