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

Jun

2

Coq ユーザのための Isabelle ガイド

Organizing : 株式会社 PRINCIPIA

Hashtag :#Isabelle
Registration info

Coq ユーザ

Free

FCFS
5/6

Description

セミナーの内容

定理証明支援系 Coq を使っている人に Isabelle/HOL の概要を紹介するセミナーです. Coq と Isabelle/HOL の機能を比較することで効率よく使えるようになってしまおうという趣旨です.

新しいプログラミング言語を覚えようと思ったとき,プログラミング経験のない入門者向けの本しかないことがあります.すでにプログラミングに慣れている人にとって「プログラムとは?」から始まる本は冗長です.一方で公式のリファレンスマニュアルは形式的で厳密で網羅的なので,よく使う重要なポイントだけを拾って学習する目的には向いていません.

ここでもし自分の知っているプログラミング言語との差分を提示してもらえたら効率よく習得できるのではないでしょうか.「この機能はこれに対応しててほとんど同じ」,「これはこう違う」,「この機能はない」,「かわりにこれがある」などです.

これを Coq と Isabelle でやってみようと思います.知識や経験の量は人それぞれですから誰にでも合うというわけにはいかないかもしれませんが,それでも学習効率はかなり高いのではないかと期待しています.参加型のセミナー方式ですから情報交換をすることで自分の知りたいポイントをおさえることもできるでしょう.

英語の勉強をすると比較によって日本語のことも改めてよくわかってくるように,Coq しか知らない人にとっては Isabelle を知ることで Coq の理解が深まるかもしれません.私は Isabelle が先でしたが,Coq の学習を通しての比較をとても楽しむことができました.

理論的な基礎や実装のことは知らないのでそういった話はしません.どちらかといえばユーザの立場で実際に証明できるようになることを目指したいと思います.

せっかくなので Isabelle をインストールしてして,体験しながら参加してください.

講師について

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

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

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

配布物と Zoom Meeting の URL

セミナー募集締め切り後に CONNPASS のメッセージにてお知らせします.

Isabelle のインストール

こちらのサイトからダウンロードできます:

注意事項

  • 配布スライド資料の公開は禁止です.
  • Isabelle で証明を書く方法にはコマンドによるものと Isar と呼ばれる可読性の高い方法の2つがあります.このセミナーではコマンドによる方法を紹介します.コマンドによる方法は Coq の tactic に似ていて入りやすいと考えるからです.Isar を知りたい人も,先にコマンドを知っておくと習得しやすいと思います.

連絡先

ご質問等がありましたら 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 245

Ended

2021/06/02(Wed)

20:00
21:30

Registration Period
2021/05/25(Tue) 00:00 〜
2021/06/02(Wed) 19:30

Location

Zoom

オンライン

Zoom

Organizer

Attendees(5)

yak_ex

yak_ex

Coq ユーザのための Isabelle ガイドに参加を申し込みました!

glacier345

glacier345

Coq ユーザのための Isabelle ガイドに参加を申し込みました!

てぴか✨

てぴか✨

Coq ユーザのための Isabelle ガイド に参加を申し込みました!

sawaragikun

sawaragikun

Coq ユーザのための Isabelle ガイド に参加を申し込みました!

itleigns

itleigns

Coq ユーザのための Isabelle ガイドに参加を申し込みました!

Attendees (5)