勉強会：Proof Summit 2019
Proof Summit 2019
定理証明系に関するユーザーイベントです。
■ 日時：2019/ 9/29 11:00ｰ16:30
■ 感想
→ Coqの証明系だけかと思っていたら
もっと幅広いツールが言及されていた
→ 自分としても、
型付ラムダ関数、カリーハワード対応などを勉強する基盤が出来つつある
次の飛躍を求めて見知を広めるべきだと思っている
→ 年一度の開催なので
是非、来年も参加したいと思っている
■ 開催・資料
（セミナ・メモ）
11:10 〜 11:40
● Idrisの話とIdris2のウワサ @blackenedgold
・Idris → 依存型
→ 型、型の型
・証明の話
→ カリーハワード対応
→ Dependent Pair
11:40 〜 12:10
● 300行で作るproof assistant @___yuni
・高階論理（HOL）
・Lean Proos Asistantを実装
→ Lean：証明支援系言語
→ αリネーミング
・THOAS → 型検査
・NbE → 意味の世界から構文(正規化済み)が取り出せる
13:50 〜 14:20
● ProofIrrelevance @2015fuj
・ProofIrrelevance
→ 全ての命題について、その証明は全て等しい
→ PropとSetは違う
→ UIP(uniqueness ofidentity proofs)
→ 排中律 ⇒ Proof Irrelevance
→ Raux →
14:20 〜 14:50
● Mathcompで文字列を使う @suharahiromichi
15:10 〜 15:40
● 人工知能によるIsabelle/HOLの証明支援 YutakaNg
・
15:40 〜 16:10
● Coqのベース体系の無矛盾性について（仮題） @yf0fyf
・Coqの正しさの証明
・論理体系の無矛盾性
以上
