出席者6人、14:15〜15:15。プロジェクターがとても淡くて薄い上、15秒に一回点滅し、話にならない。結局残り時間15分になって別の教室に移動して再開（イギリスでは何が起こるか分からない）。 反応は…プロジェクターがひどかった割には良かったです、はい。…

「とにかくまずコレを読め」（by P先生)。「すばらしかった」そうです。 参考：檜山さんのところの資料編

最小論理(minimal logic)を実装した interactive proof system MINLOG上で、bioinformaticsの定理の自動証明に挑戦する話。 最小論理とは、直観主義論理から矛盾律を除去した体系であり、最小論理における命題の証明は*1λ項によって完全に対応づけられ*2、従…

CICの集合論的解釈について。WernerとAczel、またMiquel at el の結果を概観し、またβ変換による等号の判定を体系の外側でやるCIC方式と、体系の内側でやるマーティン・レフ方式を比較した。

現在従事中のプロジェクトについて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 softwar…

案内はこちら。 （内容については、後で追加します）

ワークショップ二日目。なぜか、教室に張ってあるワークショップ名の張り紙が、昨日アナウンスのあった公式タイトルとは違っていた。謎だ。印象に残った講演は以下の通り。内容については、昨日と同様、近いうちに、講演のスライドが公式web siteで更新され…

本日から開始＠数理解析研究所。印象に残った講演は以下の通り。内容については、近いうちに、講演のスライドが公式web siteで更新されるようなので、それから紹介します。 "Inductive Cyclic Sharing Data Structures" （浜名 誠）

おそらく、この話はもう新聞で報道されているので、ここに書いても問題はないだろうと思います（何かありましたら、ご連絡をお願いします）。オランダで、公共交通用電子カードの安全性に重大な欠陥があることを証明した論文について、オランダ政府の国務長…

本日、資料整理をしたところ、机の上にプリントアウトの山を発見しました。どれも途中まで読みかけで、そして紛失したと思っていたものばかり。自分でもタイトルを忘れていたので、備忘を兼ねてメモっておきます。 "Cut elimination for Zermelo's set theor…

16時より17時半まで、出席者は10人程度。（内容については後日追加します）

談話会で発表、参加者8名、16:00-16:45。情報処理学会での発表の内容増補版、タイトルに「、」が増えている点がその増補っぷりを物語る（寒）。 （内容は後で追加します） これで、地獄の発表シーズンもやっと幕。この6週間の間に、論文締め切り1、3カ所に出…

日本IBM東京基礎研究所（中央林間）にて開催された情報処理学会 第68回プログラミング研究会にて発表しました。 （内容は後で追加します）

情報処理学会 第68回プログラミング研究会（＠日本IBM東京基礎研究所）で、上記の題で発表をすることになりました。3月17日（月）14:15-15:00の予定です。内容は業務研究の成果報告で、知識様相論理の充足関数を証明支援系に実装するさいの問題点を解決した…

業務研究の内容（Agdaで知識様相論理の体系を実装する）について発表しました。発表の出来はそれなり、会場の受けは一応好評でした。要旨は以下の通りです。 目的: 知識様相論理の意味論を証明支援系に実装 二つの問題点 多変数述語を持つ型のデータ型の定義…

コードをコンパイルするとき、実行ファイルを効率化して実行時間などを最小化するコンパイラ最適化にはいくつもの方法がありますが、今回はSSA形式の話です。SSA ではまずファイルを各変数への代入が一箇所だけで行われる形に変換し、最適化（余計なコードの…

本日の懇親会で。某大手製造業の人と雑談していて出た話。最近、ヨーロッパを中心に、ソフトウェアの安全性と品質の保証ため、形式的手法による検証が実際のシステム設計現場などでも使われつつあります。では、なぜ日本ではそれが定着しないのか。 日本の「…

ポインターに関するプログラムで、同じ意味だろうと思って下手に書き換えると、実は文脈によって違った挙動を示してしまうことがあります。では、安全(safe)な書き換えとは何か？西村氏はそれをプログラムをseparation logicの論理式の predicate transforme…

citeseerから入手可能。今まで、職場関係の論文はBlogで取り上げなかったのですが、備忘を兼ねてこちらにのせることにしました。といっても、私は計算機科学に関してはド素人なので、あまり有益な情報提供はできないと思います。 この論文、本文が7ページで…

東北大の富山先生による、項書き換え系の有名な定理：二つのconfluentな項書き換え系で、関数記号や定数記号を共有しないものは modularity を持つ、の前提条件を減らして証明した、という話。Terminationする場合は簡単だが、もちろんTerminationしない場合…

物理ではシミュレーションはもはや不可欠な道具だが、シミュレーションに関して 定量的な議論はできるが、定性的な議論はできない モデルの妥当性を問うことが難しい（シミュレーションが変な数字を出してきて初めて前提のおかしさに気づく） という問題があ…

MLLの proof net の集合上に、error-correcting コードでよく使われるやり方を応用して距離を定義する。今回はアイディアのみ。T氏曰く「Linear Logicへの愛を感じる講演」でした。

アセンブラで書かれたプログラムをモデル検査した事例の報告。モデル化するだけで見つかるエラーは少なくないが、一方で、状態爆発が起こるため実際のモデルを動かすのは大変らしい。

セキュリティ・プロトコルについて概説。BAN Logicを中心とした歴史の説明。次回はPCL。 Needham-Shroeder公開鍵認証プロトコルは、BAN Logicで安全性が証明されたにもかかわらず、実はアタックがありうることがLoweによって示された（PCLに拡張するとこのア…

関数型言語に対応する計算はλ計算、それに対応するのは Cartesian closed category。プロセスに対応する計算といえばCCSやπ算法、それではそのカテゴリー的対応物は？ 一応、Abramskyの interaction categories が提案されているが、ちゃんと定義が与えられ…

16:00-17:00 0とsuccessorとrecursorを持つsimple typed calculusをprimitive recursive functionalの中に埋め込むGandy translationを使って、strong normalizationの証明においてnormal formにいきつくまでのreductionの列の長さのupper boundを求める。up…

Distributed conflict resolution problems （ネットワークに繋いである一台のプリンターを複数のPCで使うとき、みんなが一斉にプリントしようとすると困るので交通整理が必要という話）についての Quorum system によるアプローチ。中央に司令塔があるToken…

16:00-17:00 線形時間論理の2つのシーケント計算体系の同等性およびcut除去の概要、また分岐時間論理の拡張 4CTL*（4-valued CTL）、 4LCTL* （4CTL+場所）の紹介。背景説明が主。 17:00-18:00 プログラム更新システムのプロトコルの、 信念を表すBAN logic…

産総研CLC、16:00-17:30。最近はやりの SaaS (Software as a Service)などを裏で支える、個別サーバーの故障やネットワークの断絶を乗り越えて複数のサーバーを安定的にサービスを維持する（sustainする）システムの開発。ネットワーク障害からの復旧後の「…

産総研CLC、13:30-15:00。様相論理KTBを含む normal modal logic の生成する latticeの、Splittingに関する構造について、他の体系の結果と比較しつつ。KTBのlatticeはかなり他と似ているらしい。難しかったけど、面白かったです。