みぞメモ

ブログ作成用のメモ登録

勉強会【マルレク】プログラムと論理

【マルレク】プログラムと論理

■ 日時:2019/10/10 19:00ー22:00
■ 感想

 → 今、興味を持って一番勉強している論理学とプログラムの話
   Coqを始めに「マルレク」の中心テーマに成るらしい
 → Coqや論理学、型付関数論の基本を勉強しながら
   他の勉強会と併せて学習を進めていきたい

■ 開催・資料

program-logic.peatix.com

  • 講演資料

www.marulabo.net


セミナ・メモ)


● 第一部 計算と論理 20世紀

・型付ラムダ計算と論理
 → Curry-Howard 対応
   → ラムダ計算の関数型 論理式の合意
   → 型付λ式の型の定義:論理式の三段論法
   → 「型」と「命題」、「要素」と「証明」
     → 証明は型を持つ

・Dependent Type と論理
 → Martine-Los 論理的な命題も型である
 → Polymorphic 型に依存して型が決まる → vec(ベクトル)
 → Indutive Type 帰納的型 → nat(自然数)
 → 同一性の型

・証明とは何か?
 → 命題 a → b の証明
   → 命題:aの証明から命題:bに変換する方法
 → a:A の解釈
   → 集合論構成主義、PAT、型の理論、HoTT

・PAT:"Propsitions as Types" "Proofs as Terms"

・証明支援システム Coq
 → ソフトウェア基礎科学の普遍言語(Ligua Franca)


● 第二部 プログラムと論理 20世紀

・形式手法
 → Hoare - Hoare Logic
   → P {Q} R → 事前状態{プログラム}事後状態
 → Dikstra - Nondeterminacy
   → Pで必要である条件 → wp(S,R) → guard
 → Lamport - Temporal Logic
   → 時性理論

・証明の性質をめるる論争
 → 数学者 → 
 → 社会的プロセス

・形式手法の後退
 → Hoare
 → Lamport


● 第三部 21世紀の形式手法

・Deep Specification と証明システム Coq
   -- 形式手法の’Lingua Franca
 → Deep Specification → rich, two-side, formal, live

・形式的推論・証明サンプル
 -- Hoare Logic の三組の証明

・Deep Specification における仕様と実装例
 -- Kami プロジェクトを例に

・Software Foundation

以上