ワークショップ情報
研究集会
「高信頼な理論と実装のための定理証明および定理証明器」
高信頼なソフトウェア開発のために必要な形式手法,
ソフトウェア検証,
数学の形式化, および, 証明の計算機による検証に関する研究集会を九州大学西新プラザで開催します.
TPP (Theorem Proving and Provers Meeting)は, 2005 年から年に 1 回開催され,
定理証明系を作っている人から使う側の人まで幅広い人たちが集まり,
様々な側面からの話をしてアイディアの交換をしてきたものです.
今年は, その第10回目になります.
多くの皆様に興味を持って頂き, 参加して頂けることを期待しています.
報告書:
研究集会「高信頼な理論と実装のための定理証明および定理証明器」(PDF 7.4MB)
(溝口佳寛,Jacques Garrigue,萩原学, Reynald Affeldt編集)
,
MI Lecture Notes, Vol.61, Kyushu University, 138pages, 2015/03/06.
日程
- 平成26年12月3日(水) 13:00 〜 5日(金) 16:00
場所
招待講演者
-
Adam Chlipala (MIT, USA)
Correct-by-Construction Program Synthesis in Coq (12月4日(木) 13:00-14:00)Fiat is a Coq library supporting deriving efficient programs from specifications. We think of it as enabling a new style of modularity in programming, where it is possible to separate functionality from performance, with language-enforced encapsulation keeping the latter from interfering with the former. More concretely, the programmer starts with a program written to be as easy to understand as possible. From here, optimization scripts are applied to do stepwise refinement, gradually replacing nondeterministic constructions with deterministic ones, and replacing slow algorithms with fast ones. As the implementation language of optimization scripts, we reuse Ltac, Coq's language for coding proofs and decision procedures. We inherit Ltac's support for generating proof trails that vouch for the soundness of all operations. With highly expressive functional programming languages for both the functionality and performance parts of programs, we develop new abstraction and modularity patterns on each side of the divide. Our main case study so far deals with specifications that resemble SQL query and update operations. A set of operations over a particular schema are packaged together as an abstract data type, hiding the concrete representation of a relational database. We refine these nondeterministic descriptions of operations into efficient functional programs, which can be extracted to OCaml and run with good performance. In ongoing work, we are extending the refinement process to produce efficient assembly code using imperative data structures (via the Bedrock library), retaining proof trails to relate those programs to the original specifications. We are also exploring several new specification domains with associated refinement strategies, including for parsing, graph algorithms, and stencils in scientific computing.
Joint work with Benjamin Delaware, Clément Pit--Claudel, and Jason Gross
- Cyril Cohen (INRIA Sophia-Antipolis, France)
Mathematical Components and Algebraic Numbers (12月5日(金) 13:30-14:30)The Mathematical Components project spanned 6 years and involved 15 people, with the purpose of formalizing a proof of Feit-Thompson theorem (also known as the odd order theorem), which is a milestone in the classification of finite groups. The proof relies on various areas in mathematics, including group theory, linear algebra, representation theory, Galois theory,... The project succeeded in formalizing the proof thanks to the development of a large set of libraries and methodologies covering the mathematics. One of the main achievements of the project, besides the formalization of the main theorem, is this set of libraries, which were designed to be reused. They were indeed reused in other developments such as, for example, in formalizations on homological algebra, elliptic curves, Shannon's information theory, error correcting codes,... My personal contribution to the Mathematical Components libraries was to build algebraic numbers and the tools to construct and use them. In this talk, I will give an overview of the project, its library and I will detail my own contributions.
TPPmark2014(問題)
- 皆で問題(PDF)を解いて, 研究集会中に証明を比べようと思います。証明や質問は下記の問合せ先のメールアドレスに送って下さい。研究集会に参加出来ない方の応募もお待ちしています。初めての方も、そうでない方も、気楽に応募下さい。送って頂いた、いろいろなシステムでの、いろいろな証明方法をgithubレポジトリにて公開します。
プログラム
- 12月3日(水)の講演
13:00 受付開始
Time Specker Title 13:30 - 14:00 関根 祥吾
(千葉大)SSReflectを用いたペトリネットにおけるカープミラー加速の形式化 14:00 - 14:30 森口 草介
(関西学院大)プログラム生成の検証へ向けて 14:30 - 15:00 小尾 良介
(千葉大)SSReflectによる可変長情報源符号化逆定理の形式化 15:00 - 15:30 坂口 和彦
(筑波大)Formalizing Strong Normalization Proofs 休憩 (15分) 15:45 - 16:15 佐藤 雅彦
(京都大)A name-free lambda calculus 16:15 - 16:45 中正 和久
(信州大)Mizarによる群の直和分解の形式化 16:45 - 17:15 岡崎 裕之
(信州大)Mizarによる多項式オーダーの関数に関する形式化
- 12月4日(木)の講演
Time Specker Title 09:30 - 10:30 今井 宣洋
(ITプランニング)Coqを使ったデジタルデータ放送におけるストリームデータ処理の形式化と検証 休憩 (10分) 10:40 - 11:40 栗田 太郎
(フェリカネットワークス)システム開発において数理論理学に基づいた仕様記述言語を用いることによる品質の確保
～文書の記述力とチームのコミュニケーション力を鍛える～昼食(80分) 13:00 - 14:00 Adam Chlipala
(MIT)Correct-by-Construction Program Synthesis in Coq 休憩 (15分) 14:15 - 14:45 Reynald Affeldt(AIST)
Jacques Garrigue(名古屋大)Formalization of Error-correcting Codes using SSReflect 14:45 - 15:15 Fadoua Ghourabi
(関西学院大)Formalization of matrix representation of direction relations with application to the superposition of rectangles 15:15 - 15:45 田辺 良則
(情報学研究所)CoqからScalaへのコード抽出とその妥当性 休憩 (15分) 16:00 - 16:30 奥村 健太郎
(京都大)Weak HOASを用いたFeatherweight JavaのCoq上での形式化 16:30 - 17:00 八杉 昌宏
(九州工大)メモリモデルを考慮した汎用型付中間言語設計に向けて 17:00 - 17:30 佐藤 雅大
(名古屋大)An intuitionistic Set-theoretical Model of the Extend Calculus of Construction 休憩 (15分) 17:45 - 18:30 TPPmark2014 (Repository)
懇親会(19:00から) @ 居酒屋ひなたぼっこ (会費:5000円(学生:4000円))
※準備の都合上, 懇親会へ参加される方は事前にEmail等で連絡をお願いします.
- 12月5日(金)の講演
Time Specker Title 09:30 - 10:30 矢田部 俊介
(JR西日本)コンセプト段階における準形式手法のシステム設計への利用 休憩 (10分) 10:40 - 11:10 久我 健一(千葉大)
萩原 学(千葉大)On formalization of basic geometric topology 11:10 - 11:40 才川 隆文
(名古屋大)Formalizing a coding theory 11:40 - 12:10 井田 哲雄
(筑波大)Formalization of geometric algebra with application to computational origami 昼食 (80分) 13:30 - 14:30 Cyril Cohen
(INRIA)Mathematical Components and Algebraic Numbers 休憩 (15分) 14:45 - 15:45 阿原 一志
(明治大)対話型幾何ソフトウエアと自動証明—シンデレラとキッズシンディ
16:00 閉会
問い合わせ先・連絡先
- tpp2014 at imi.kyushu-u.ac.jp (溝口 佳寛 (九州大学))
Follow @ym9568
運営責任者
- 溝口 佳寛 (九州大学)
- Jacques Garrigue (名古屋大学)
- 萩原 学 (千葉大学)
- Reynald Affeldt (産業技術総合研究所)
主催
九州大学マス・ フォア・インダストリ研究所 数学理論先進ソフトウェア開発室
共催
「高信頼な理論と実装のための定理証明および定理証明器」
後援
電子情報通信学会九州支部※ この研究集会の一部は【科学研究費補助金 挑戦的萌芽研究 課題番号:25610034 研究代表者:溝口佳寛】および【科学研究費補助金 基盤研究(B) 課題番号:25289118 研究代表者:萩原学】（日本学術振興会）の支援のもと開催されます。
