#TPP2014 高信頼な理論と実装のための定理証明および定理証明器
-
yoshihiro503
- 5167
- 0
- 4
- 14
-
- いいね！14
Masahiro Sakai
@masahiro_sakai
#TPP2014 に着いた。 imi.kyushu-u.ac.jp/lasm/tpp2014/ (@ 九州大学 西新プラザ in 福岡市, 福岡県) swarmapp.com/c/i9IvSm4AkLE
2014-12-03 13:39:01
Sosuke MORIGUCHI
@chiguri
monadとして扱うことでoptionを使った部分関数をうまくやっている。やっぱ使い勝手良いよね。 #TPP2014
2014-12-03 13:44:49
Sosuke MORIGUCHI
@chiguri
KM加速を使った可達（到達可能な状態の）木は本来無限だったのが有限につぶせる。・・・でいいのかな。 #TPP2014
2014-12-03 13:47:41
Masahiro Sakai
@masahiro_sakai
SSReflectを用いたペトリネットにおけるカープミラー加速の形式化 (関根 祥吾) : 形式化は割と素直そうだけど、Karp-Millar加速というのは知らなくて面白そう。あと、SSreflectに用意されているという有限集合上の関数の型は便利そう。 #tpp2014
2014-12-03 13:52:36
Masahiro Sakai
@masahiro_sakai
プログラム生成の検証へ向けて (森口 草介 / chiguri) うーん、当たり前のことを言っているようにしか聞こえないが…… #tpp2014
2014-12-03 14:16:50
Masahiro Sakai
@masahiro_sakai
@masahiro_sakai 結局、代数的データ型で表現された命令形プログラムに対して簡単な公理的意味論を定義して、仕様の記述と証明を出来るようにしたということなのかな? むしろ、生成側の情報を使った証明の書き方の方？ #tpp2014
2014-12-03 14:34:59
Sosuke MORIGUCHI
@chiguri
無限和は計算可能だからとかの問題かな・・・？自然数しか使わないんだから書けない、という方がまずいような・・・？ #TPP2014
2014-12-03 14:50:19
Masahiro Sakai
@masahiro_sakai
Formalizing Strong Normalization Proofs (坂口 和彦) : monusを使った最小値をとる関数 x ∸ (x ∸ y) の可換性をomegaで証明しようとすると、止まらないくなるらしい。 #tpp2014
2014-12-03 15:15:22
Sosuke MORIGUCHI
@chiguri
α等価の推論規則の形成。λの引数を複数にして、その形に関してのみ議論（0でも可）。このとき、α等価なものの示す証明木がα等価な項全体を代表する元として扱える。 #TPP2014
2014-12-03 16:12:05
Sosuke MORIGUCHI
@chiguri
IとKの間だからJにした。（コンビネータのIとK） n個をとってi番目を返すコンビネータらしい。 #TPP2014
2014-12-03 16:15:06
Masahiro Sakai
@masahiro_sakai
A name-free lambda calculus (佐藤 雅彦) : タイトルから想像していたより、ずっと面白かった。 α-同値な閉ラムダ項の部分項が、閉でなくα-同値でないラムダ項になりうるのは、確かに考えてみれば気持ち悪い。 #tpp2014
2014-12-03 16:33:23
Takashi Miyamoto
@tmiya_
#tpp2014 Mizarは割と英文ぽい感じに記述出来るのは強みかもしれんなぁ... 普通のプログラム開発の仕様記述とか、もしかしてCoqとかより向いてるかもしれんなぁ...
2014-12-03 16:42:34
Masahiro Sakai
@masahiro_sakai
Mizarによる多項式オーダーの関数に関する形式化 (岡崎 裕之) 「(game-sequence proof のような)特定のモデル上ではなく、普通の暗号研究者が書くように形式的証明したい」 #tpp2014
2014-12-03 16:59:55