お知らせ connpassではさらなる価値のあるデータを提供するため、2024年5月23日(木)を以ちましてイベントサーチAPIの無料での提供の廃止を決定いたしました。
2024年5月23日(木)以降より開始予定の「connpass 有料API」の料金プランにつきましてはこちらをご覧ください。

お知らせ connpassをご利用いただく全ユーザーにおいて健全で円滑なイベントの開催や参加いただけるよう、イベント参加者向け・イベント管理者向けのガイドラインページを公開しました。内容をご理解の上、イベント内での違反行為に対応する参考としていただきますようお願いいたします。

6月

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

主催 : 株式会社 PRINCIPIA

ハッシュタグ：#Isabelle

募集内容	一般 1000円（前払い）先着順 7/10人
申込者	申込者一覧を見る
開催日時	2020/06/19(金) 21:00 ～ 22:30 Googleカレンダー icsファイル
募集期間	2020/06/18(木) 00:00 〜 2020/06/19(金) 20:30まで
会場	Zoom オンライン
前払いについて	前払いについての連絡先: (参加者にのみ公開されます)
	キャンセル・参加費用の払い戻しについて主催者からの説明: お申込み後のキャンセルはできません．セミナーについての説明をよくお読みいただき，十分ご検討の上お申し込みください．CONNPASS上でキャンセルしても，セミナー当日に不参加であったとしても参加費用は返却されません．
	領収データの発行: 発行しない (詳しくはこちら)

イベントの説明

セミナーの内容

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

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

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

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

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