このエントリーをはてなブックマークに追加

Jul

3

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

Organizing : 株式会社 PRINCIPIA

Hashtag :#Coq
Registration info

一般

9000 (Pre-pay)

FCFS
9/10

About Prepayment

About Prepayment Contact Info:

(Only shown to attendees.)

Cancel/Refund Policy:

お申込み後のキャンセルはできません。セミナーについての説明をよくお読みいただき、十分ご検討の上お申し込みください。

Print receipt data:

発行しない (詳しくはこちら)

Description

セミナーの内容

定理証明支援系 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 までお気軽にご連絡ください。

Media View all Media

If you add event media, up to 3 items will be shown here.

Group

PRINCIPIA

Number of events 96

Members 244

Ended

2021/07/03(Sat)

13:00
18:00

Registration Period
2021/06/08(Tue) 00:00 〜
2021/07/03(Sat) 12:30

Location

Zoom

オンライン

Zoom

Organizer

Attendees(9)

TakeshiHori

TakeshiHori

定理証明支援系 Coq チュートリアル に参加を申し込みました!

tukejonny

tukejonny

定理証明支援系 Coq チュートリアル に参加を申し込みました!

Kuniwak

Kuniwak

定理証明支援系 Coq チュートリアル に参加を申し込みました!

yjszk

yjszk

定理証明支援系 Coq チュートリアル に参加を申し込みました!

RyosukeNakagawa

RyosukeNakagawa

定理証明支援系 Coq チュートリアル に参加を申し込みました!

shigemi1014

shigemi1014

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

altitude3190

altitude3190

定理証明支援系 Coq チュートリアル に参加を申し込みました!

sawaragikun

sawaragikun

定理証明支援系 Coq チュートリアル に参加を申し込みました!

Yutaka HARA

Yutaka HARA

定理証明支援系 Coq チュートリアル に参加を申し込みました!

Attendees (9)