新機能 イベント詳細画面に「参加者への情報」欄を追加しました。イベント管理者、発表者、参加者(抽選中や補欠は除く)だけに表示されるフィールドです。詳しくはこちら

新機能 オンラインイベントが検索できるようになりました。オンラインイベントとして検索できるようにするには こちら をご確認ください

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

Jun

19

関数型言語の操作的意味論 in Isabelle

Organizing : 株式会社 PRINCIPIA

Hashtag :#Isabelle
Registration info

一般

1000 (Pre-pay)

FCFS
7/10

About Prepayment

About Prepayment Contact Info:

(Only shown to attendees.)

Cancel/Refund Policy:

お申込み後のキャンセルはできません.セミナーについての説明をよくお読みいただき,十分ご検討の上お申し込みください.CONNPASS上でキャンセルしても,セミナー当日に不参加であったとしても参加費用は返却されません.

Print receipt data:

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

Description

セミナーの内容

定理証明支援ツール Isabelle 上で小さな関数型言語の操作的意味論を表現し,プログラムの性質を証明します.

集合の帰納的定義の応用例第2弾です.(前回はシーケント計算の推論規則でした)

プログラミング言語で書かれたプログラムが表す"動作"あるいは"計算"がどのようなものであるかは,文書の中で自然言語で規定されていることが多いでしょう.ほとんどの場合はそれで充分でしょう.しかし自然言語による規定は曖昧になってしまうことがあり,あるプログラムコードがどのような動作になるのか不明確であるということが起こりえます.そのようなケースはまれかもしれませんが,検証をする人やコンパイラを作る人にとっては問題になります.

この問題を解決するためにプログラムの動作を数学的に厳密に定めるという方法があります.今回はそのような手法の1つである操作的意味論を定理証明支援ツール Isabelle で扱ってみます.小さな関数型言語を対象に操作的意味論を定め,それを使ってプログラムの性質を証明します.

初等的なレベルです.圏論の話はしません.

プログラム

  • プログラミング言語の意味論
  • プログラミング言語 PCF
  • PCF の操作的意味論
  • Isabelle 上での表現
  • 証明例
  • 演習問題
  • チャレンジ問題

講師について

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

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

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

セミナー参加の前提条件

前提知識

  • Isabelle の文書 tutorial.pdf の part I, II 程度の知識(Isabelle チュートリアル第1~4回相当)

必要なもの

配布物

スライド資料(PDF)と Isabelle の理論ファイルを CONNPASS のメッセージにて配布します。

Zoom Meeting link

CONNPASS のメッセージにてお知らせします。

Slack

https://join.slack.com/t/syncstitch/shared_invite/zt-e52dcyza-Vs0vCglGNcPSGOFriRIehQ

注意事項

  • 配布スライド資料と理論ファイルの公開は禁止です。

連絡先

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

Media View all Media

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

Ended

2020/06/19(Fri)

21:00
22:30

Registration Period
2020/06/18(Thu) 00:00 〜
2020/06/19(Fri) 20:30

Location

Zoom

オンライン

Zoom

Organizer

Attendees(7)

elkel53930

elkel53930

関数型言語の操作的意味論 in Isabelleに参加を申し込みました!

Kuniwak

Kuniwak

関数型言語の操作的意味論 in Isabelle に参加を申し込みました!

tukejonny

tukejonny

関数型言語の操作的意味論 in Isabelle に参加を申し込みました!

niszet

niszet

関数型言語の操作的意味論 in Isabelle に参加を申し込みました!

TakeshiHori

TakeshiHori

関数型言語の操作的意味論 in Isabelle に参加を申し込みました!

tkokamo

tkokamo

関数型言語の操作的意味論 in Isabelleに参加を申し込みました!

shigemi1014

shigemi1014

I joined 関数型言語の操作的意味論 in Isabelle!

Attendees (7)