開催日：2024/11/25～2024/11/26

コンピュータによる定理証明支援とその応用｜2024a024

開催概要

プログラム

https://www.math.nagoya-u.ac.jp/~garrigue/tpp2024

11月25日（月）【公開】 12:50-17:55

12:50-13:00:Opening

13:00-14:00

Pierre-Marie Pédrot (INRIA Atlantique)
A Kernel of Truth (Invited talk)

14:15-16:10

Yosuke Ito (Sompo Himawari Life Insurance Inc.)
Formalizing Premium Calculation of Life Insurance (30mn)

Kenta Inoue
Coq/SSReflectでコンストラクタ数が引数に依存して変化するInductive 型とseq T型のconsの型をT -> seq (seq T) -> seq Tに変更した型を定義したい

Makoto Kanazawa (法政大学理工学部)
Verification of the Garsia-Wachs algorithm

Yoshihiro Imai (株式会社proof ninja)
ブロックチェーンにおける支払い認証ポリシーの静的検証ツールの形式検証

16:25-17:55 (short talks, 15min each)

Sho Sonoda (Riken)
Automated Theorem Proving by HyperTree Proof Search with Retrieval-Augmented Tactic Generator

松岡和貴 (東京科学大学　理工学系情報理工学院数理・計算科学系数理・計算科学コース)
Isabelle/HOLを用いた差分プライベートなアルゴリズムの安全な実装

野口真柊 (神戸大学システム情報学科)
標準的な様相論理のLeanでの形式化について

大森章裕 (東京科学大学 情報理工学院 数理計算科学系 南出研究室)
Postの対応問題のインスタンスの証明生成

城戸道仁 (法政大学大学院理工学研究科システム理工学専攻)
重複を除き辞書順で最小の部分リストを返す効率的なアルゴリズムの Agdaによる検証

Takafumi Saikawa (Nagoya University)
TBA

11月26日（火）【公開】 9:00-16:40

9:00-10:30

Masahiko Sato (京都大学 情報学研究科)
λ-計算の代数と幾何 (40min talk)

Daiki Funane (東北大学大学院情報科学研究科)
ZF+￢ACの相対的無矛盾性証明のIsabelle/ZFによる形式化

齋藤彰悟 (東北大学大学院理学研究科数学専攻)
Leanを用いたGödelの第一・第二不完全性定理の形式化

10:45-12:25

櫻田英樹 (NTTコミュニケーション科学基礎研究所)
暗号プロトコルの形式記述に向けたLLMチャットボットの活用

平田路和 (東京科学大学)
A Formalization of Prokhorov’s Theorem in Isabelle/HOL

川上竜司 (名古屋大学 多元数理学研究科)
Delayモナドを用いた一般再帰関数に対する等式変形による検証

Satoshi Matsuoka (産業技術総合研究所工学計測標準部門データサイエンス研究グループ)
On Representability of Multiple-Valued Functions by Linear Lambda Terms Typed with Second-order Polymorphic Type System

13:30-15:10

手塚 凜 (千葉大学大学院 融合理工学府)
ペトリネットにおける到達可能性問題の変種間の還元可能性の形式化

Sewon Park (Kyoto University)
Axiomatic real numbers for verified exact real-number computation

Yue Niu (National Institute of Informatics)
Combining cost and behavior in type theory

瀬川秀一 (北陸先端科学技術大学院大学)
Leanを用いたスイッチング回路の安全性検証

15:25-16:40

Jacques Garrigue (Nagoya University) and provers
TPPmark 2024 (20min)

西島海斗 (山口大学)
導出原理の逆適用による定理の自動生成手法の提案 (25min)

早川銀河 (九州大学 数理学府 数理学専攻)
Coq証明支援系によるDNA計算の形式化 (15min)

石黒吉洋 (名古屋大学)
Coqによる実解析のための実用的な補題の開発 (15min)

申込方法

事前申込制（組織委員，講演者のかたも登録が必要です）
参加無料
定員になり次第，参加登録を締め切らせていただく場合がございます.

＼下記URLより参加登録をお願いいたします／

Zoom（オンライン）からご参加の方

Zoomを使ったオンライン開催，ハイブリッド開催の場合

参加登録後に件名［九大IMIより］Zoom用URLのお知らせというメールがimikyoten@gmail.comから自動配信されます．
届いていない方は，お手数をおかけしますがもう一度ご登録いただくか下記にメールにてご連絡をお願い申し上げます．
（迷惑メールフォルダもご確認お願いいたします）

＜九州大学マス・フォア・インダストリ研究所 共同利用・共同研究拠点事務室＞
imikyoten(at)jimu.kyushu-u.ac.jp
(at)を@に変更してください

Zoomについて

開催日までにZoomアプリをインストールしてください．
Zoomアプリは無料版で問題なくご視聴いただけます．

ミーティング用Zoomクライアントのダウンロードは下記からお願いします．
すでにインストールされている方は最新版にアップデートをお願いいたします．
https://zoom.us/download#client_4meeting

パソコンやスマホへのインストール方法は下記をご参照ください．
https://zoom.nissho-ele.co.jp/blog/manual/zoom-install.html