検索条件

キーワード
タグ
ツール
開催日
こだわり条件

タグ一覧

JavaScript
PHP
Java
Ruby
Python
Perl
Scala
Haskell
C言語
C言語系
Google言語
デスクトップアプリ
スマートフォンアプリ
プログラミング言語
U/UX
MySQL
RDB
NoSQL
全文検索エンジン
全文検索
Hadoop
Apache Spark
BigQuery
サーバ構成管理
開発サポートツール
テストツール
開発手法
BI
Deep Learning
自然言語処理
BaaS
PaaS
Iaas
Saas
クラウド
AI
Payment
クラウドソフトウェア
仮想化ソフトウェア
OS
サーバ監視
ネットワーク
WEBサーバ
開発ツール
テキストエディタ
CSS
HTML
WEB知識
CMS
WEBマーケティング
グラフィック
グラフィックツール
Drone
AR
マーケット知識
セキュリティ
Shell
IoT
テスト
Block chain
知識

定理証明支援系 Coq チュートリアル

  • Coq
  • 数学
2021/07/03(土)
13:00〜18:00

主催:PRINCIPIA

セミナーの内容

定理証明支援系 Coq のチュートリアルです。実際に Coq を使いながら学ぶハンズオン形式です。はじめて Coq に触れる人が対象です。かんたんな論理式の証明からはじめて、証明付きプログラムからコードを抽出できるようになることを目指します。

プログラミングに関わる人が Coq を仕様やプログラムの検証に使うことを想定しています。内容として初等的なものになります。数学や論理学を専門にしている人向けではありません。

セミナーは2日間の構成です。この CONNPASS のイベントに申し込むことで2日間のセミナーに参加できます。

はじめての人にとっては知的好奇心をくすぐる目新しい考え方が次から次へと現れる刺激的なセミナーです。フルに頭を使いますから甘いものを用意してご参加ください。

プログラム

第1日目 7月3日(土)13:00-18:00

  • Coq による論理式の証明
  • 定義と使用
  • 数学的帰納法
  • 述語の帰納的定義

第2日目 7月4日(日)13:00-18:00

  • Calculus of Inductive Constructions
  • 依存型によるプログラミングと検証
  • プログラム抽出

※ 進捗によって一部内容とスケジュールを変更する場合があります。

講師について

株式会社 PRINCIPIA 代表取締役 初谷 久史

CSP 理論に基づいたモデリング・検査ツール SyncStitch 開発者

国立情報学研究所トップエスイープロジェクト「並行システムの設計検証」講師

必要な知識

  • 高校で習う程度の数学の知識:命題と論理,数学的帰納法
  • 関数型プログラミングの初等的な知識:関数適用,抽象(λ式,無名関数),再帰,代数的データ型,パターンマッチ

必要なもの

配布物と Zoom meeting URL

セミナー開始時刻までにCONNPASS のメッセージにてお知らせします。

同じメッセージを複数回送信する場合があります。あらかじめご了承ください。

注意事項

  • 配布資料の公開は禁止です。
  • 不測の事態が生じセミナーを開催または完遂できなかった場合は、日を改めて再開催することで対処させていただきます。
  • 都合により申し込み後に参加できなくなった場合は、同等のセミナーを再演する際にご参加いただけるよう配慮しますのでご連絡ください。

連絡先

ご質問等がありましたら isaac@principia-m.com までお気軽にご連絡ください。