トップエスイー特別講義、定理証明と検証

Yoshihiro Imai @yoshihiro503

これからCoqセミナーへ行く #topse_coq

ogawa kiyoshi @kaizen_nagoya

#topse_coq 会場到着 http://t.co/uBAwnquP

山本和彦 @kazu_yamamoto

top se の会場に来た。Coq のインストールは、どうするのか心配していたら、端末が用意してあった。おそるべし。　#topse_coq

山本和彦 @kazu_yamamoto

チュートリアルなのに参加者のレベルが高い。 　#topse_coq

山本和彦 @kazu_yamamoto

OCaml で開発しているのなら、Coq がとても有用。 #topse_coq

ogawa kiyoshi @kaizen_nagoya

#topse_coq 演習記録 http://t.co/2j6RtFYX

山本和彦 @kazu_yamamoto

新しい Emacs は入れたのに coq を入れてなかった！インストール中。 #topse_coq

imuno@シリコンバレー7年目 @imunolion

山本先生も今日の #topse_coq にいらっしゃるのか. すごい集客力

山本和彦 @kazu_yamamoto

check と print の説明。 #topse_coq

山本和彦 @kazu_yamamoto

いきなり、Extraction です。:) #topse_coq

山本和彦 @kazu_yamamoto

= は命題。単純に評価はできない。 #topse_coq

山本和彦 @kazu_yamamoto

nat と 命題 (2+1=3) が同じレベルに書かれている。型と命題が対応するから？ #topse_coq

山本和彦 @kazu_yamamoto

上がプログラムの世界、下が命題の世界。 #topse_coq

山本和彦 @kazu_yamamoto

型の大文字小文字に意味はない！ #topse_coq

山本和彦 @kazu_yamamoto

大文字小文字は区別するが、公の名前付け規則はない。 #topse_coq

山本和彦 @kazu_yamamoto

プログラム、型、証明、命題は、どれも式。混ぜられる。 #topse_coq

山本和彦 @kazu_yamamoto

でも、混ぜると危険。:) #topse_coq

山本和彦 @kazu_yamamoto

2 + 1 = 3 という型を持つプログラム refl_equal 3 を定義する。 #topse_coq

山本和彦 @kazu_yamamoto

右辺も左辺も 3 になる。 #topse_coq

Seizan Shimazaki @seizans

Definition aproof : (2 + 1 = 3) := refl_equal 3. aproof という (2 + 1 = 3)型のものを定義する。定義は refl_equal 3。 refl_equal は 両辺 3 になるなら True #topse_coq

ogawa kiyoshi @kaizen_nagoya

coq seminar at NII http://t.co/uBAwnquP #topse_coq

ogawa kiyoshi @kaizen_nagoya

昼休みの講師の助言：coqは型検査と評価を同時にする #topse_coq

ogawa kiyoshi @kaizen_nagoya

#topse_coq Q&A Q.インデント，空白，改行は意味があるか。A. インデント，空白，改行を追加しても意味は変わらない。識別子の区分のための空白は意味がある。