RT @mzp: 東京の人はFormalMethodForum、名古屋の人はProofCafe #proofsummit

posted at 17:01:59

ProofCafe こわい! #proofsummit

posted at 17:01:51

RT @cho_tekitou: みんなで翻訳しよう！　#proofsummit

posted at 16:53:44

RT @oskimura: Proof server はcoqで証明されているのだろうか？　#proofsummit

posted at 16:53:01

AoPA 読んでみよう #proofsummit

posted at 16:39:20

定理自動証明だと一階述語なので数学的帰納法が使えない #proofsummit

posted at 16:25:38

自動的にソクラテスが死ぬ……！ #proofsummit

posted at 16:24:37

質疑応答「ssreflect があなぷるに入るのはいつごろですか？」「先週入れ始めようとしたんですが、ゲームが発売されたので……。」 #proofsummit

posted at 16:11:20

W.O.L.G. tacticｗｗｗ #proofsummit

posted at 16:06:24

「ある程度簡単なものは done で終わらせてください」「どれくらい簡単なものですか」「done で終わるくらい簡単なものです」 #proofsummit

posted at 15:58:43

RT @sacrinnatsaku: (-> <-.) ふえぇぇん RT @mzp: #proofsummit move=> -> <-. 顔文字にしか見えねぇ

posted at 15:57:34

おお、なるほど！ #proofsummit

posted at 15:55:27

-> <- かわいい #proofsummit

posted at 15:53:23

シンプルすぎて証明が読めない……。 #proofsummit

posted at 15:44:44

RT @keigoi: さっきのスライドを http://proofcafe.org/~keigoi/start_seplog-proofsummit-keigo... に置きました #proofsummit

posted at 15:38:32

サブゴールがわかるように証明を書いておくとメンテナンスがしやすい #proofsummit

posted at 15:37:58

続いて @kikx さんのはっぴょう #proofsummit

posted at 15:30:41

Concurrent Separation Logic と云うものがあるらしい #proofsummit

posted at 15:27:42

プロセス計算。プロセス p を表現する様相論理式 L( p ) がある。 #proofsummit

posted at 15:23:48

新しい潮流：OCaml のコードと一意対応する "特性論理式" を生成する？？？ #proofsummit

posted at 15:22:21

続いて swap の例 #proofsummit

posted at 15:14:51

「証明長いですね。書きたくないですね。Coq つかいこなして自動で生成出来たらいいのにと思うんですが」 #proofsummit

posted at 15:13:30

「階乗の証明。長いですね！」 #proofsummit

posted at 15:12:49

「これは僕の手で証明しろと云うことなんでしょうか」ｗｗｗ #proofsummit

posted at 15:12:16

Eiffel とか DbC の背景はホーアロジック #proofsummit

posted at 15:11:52

RT @pi8027: なるほど。ホーア論理と分離論理の組み合わせで手続き型言語風のプログラムを記述するのか……。 #proofsummit

posted at 15:11:02

「ホーア論理の普及を妨げているのは必ずループ不変条件を書かなくてはいけないところ」 #proofsummit

posted at 15:10:38

ホーア論理で C の証明を書く例。まずは階乗の仕様記述の例から。 #proofsummit

posted at 15:07:52

ついにホーア論理と seplog が合流！「やっとここまできた！」 #proofsummit

posted at 15:05:43

RT @pi8027: CoPL でも、 evalto という「eval できる」という関係を使って自分で正しい eval のプロセスを書くという問題があった。eval の関係と eval の関係を作る物(evaluator)は別だと考えた方が良い。 #proofsummit

posted at 15:03:42

「まあまあまあ、待ってください」 #proofsummit

posted at 15:02:34

s -- c --> s' と書く。終状態は停止しないかもしれないから、始状態、終状態ともに option で前後の状態を渡す。(Big Step semantics というらしい) #proofsummit

posted at 14:51:07

Coq 上に C インタプリタを作りたい。しかし、C の意味論で許容されている停止しない函数が Coq では書けない！どうする？三項関係を使う！ #proofsummit

posted at 14:49:26

分離論理では Coq の上に C インタプリタを作ろうとしている #proofsummit

posted at 14:45:53

分離論理では状態が必要なので、Prop 型ではなく store.s や heap.h などの状態を組にした assert 型を使う #proofsummit

posted at 14:43:18

「それは私に説明させて下さい。」ｗｗｗ #proofsummit

posted at 14:42:02

プログラムはボトムアップに読んだりトップダウンに読んだり色々あるけど、証明はボトムアップに読んでいくのがよい #proofsummit

posted at 14:40:48

Coq で 2万行……だと……？ #proofsummit

posted at 14:37:57

「目を通しておくといつの日かみなさんもCoq で暗号アルゴリズムと OS コードがかけるようになるかもしれない」 #proofsummit

posted at 14:36:45

分離論理で追加される論理結合子は x |-> e (x mapsto e), p ** q (P∧Q, P と Q は異なるメモリ領域), P -* Q (魔法の杖 / P → Q / Pで参照してる領域はQでも参照している?) #proofsummit

posted at 14:35:10

にわとりキモい！！！！！！！！ #proofsummit

posted at 14:33:34

けいごいさんによる分離論理のはなし！ #proofsummit

posted at 14:27:39

また名古屋か！ #proofsummit

posted at 14:26:23

applpi こわい…… #proofsummit

posted at 14:22:35

http://bit.ly/quEA3l この問題か……！ #proofsummit

posted at 14:11:05

困ったときのあなぷるｗｗｗ #proofsummit

posted at 14:10:50

名古屋こわい #proofsummit

posted at 14:03:50

そういえばいつも 𝐍 をどうやって入力するのかわからない #proofsummit

posted at 12:54:41

#proofsummit だった

posted at 12:52:23

一番後ろの床に座っているのが僕です #proofsummit

posted at 12:48:10