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

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

5月

7
tackeさんからの挑戦状
Isabelleによるプログラムの正当性証明事例解説

主催 : PRINCIPIA Limited

ハッシュタグ：#FormalVerification

募集内容	一般無料先着順 3/10人「証明には甘いお菓子が必要」支援 500円（前払い）先着順 3/10人
申込者	申込者一覧を見る
開催日時	2020/05/07(木) 19:30 ～ 21:00 Googleカレンダー icsファイル
募集期間	2020/05/05(火) 00:00 〜 2020/05/07(木) 19:00まで
会場	Zoom オンライン
前払いについて	前払いについての連絡先: (参加者にのみ公開されます)
	キャンセル・参加費用の払い戻しについて主催者からの説明: 支援ありがとうございます。
	領収データの発行: 発行しない (詳しくはこちら)

イベントの説明

tacke さんからの挑戦状

初谷@PRINCIPIAです．

セミナーに参加していた tacke さん（仮名）から挑戦状が届きました。

君にこの問題が証明できるかな？

2つの列 xs と ys を考えよう。ys の各要素は xs の要素でもあり、対応する要素の並び順は xs 上でのインデックス順になっているとき、ys は xs のサブシーケンスであるという。サブシーケンスであるかどうかを判定するプログラムを書き、正当性を証明してごらん。

subsequence

挑戦を受けた私は Isabelle で証明を試みました。その過程をそのまま解説したいと思います。整理された証明と違って追うのはたいへんかもしれませんが、試行錯誤の過程も含めてどんなふうに考え、どんなふうに証明しているのか一例を紹介する機会にしたいと考えました。調べるべき可能性はまだありますが、一応プログラムの証明ができたところまでにします。

お菓子と飲み物など用意して気軽に聞いてください．途中参加・途中退出はご自由にどうぞ．

Isabelle の理論ファイルと Zoom の URL は CONNPASS のメッセージでお知らせします．