• 九州大学マス・フォア・インダストリ研究所

• 溝口 佳寛
• Garrigue Jacques
• 萩原 学
• AFFELDT Reynald

詳細プログラム:

English http://imi.kyushu-u.ac.jp/lasm/tpp2014/

日本語 http://imi.kyushu-u.ac.jp/lasm/tpp2014/index_ja.html

--
Dec. 3, 2014.

13:00 Registration

Session Chair: Garrigue Jacques
13:30 - 14:00 Shogo Sekine (Chiba Univ.)
Formalizing Karp and Miller Acceralation for Petri Nets using SSReflect
14:00 - 14:30 Sosuke Moriguchi (Kwansei Gakuin Univ.)
Towards verification of program generations
14:30 - 15:00 Ryosuke Obi (Chiba Univ.)
Formalization of Variable-Length Source Coding Theorem: Converse Part
15:00 - 15:30 Kazuhiko Sakaguchi (Tsukuba Univ.)
Formalizing Strong Normalization Proofs

Session Chair: Affeldt Reynald
15:45 - 16:15 Masahiko Sato (Kyoto Univ.)
A name-free lambda calculus
16:15 - 16:45 Kazuhisa Nakasho (Shinshu Univ.)
Formalization of Direct Sum Decomposition of Groups in Mizar
16:45 - 17:15 Hiroyuki Okazaki (Shinshu Univ.)
Formalization of polynomially bounded functions in Mizar

--
Dec. 4, 2014.

Session Chair: Manabu Hagiwara
09:30 - 10:30 Yoshihiro Imai (IT Planning, Inc.)
Formalization and verification of stream data processing for datacasting in Coq

Session Chair: Keijiro Araki
10:40 - 11:40 Taro Kurita (FeliCa Networks, Inc.)
The Application of VDM (Vienna Development Method) to the Industrial
Development of Firmware for a Smart Card IC Chip

Session Chair: Affeldt Reynald
13:00 - 14:00 Adam Chlipala (MIT)
Correct-by-Construction Program Synthesis in Coq

Session Chair: Yoshihiro Imai
14:15 - 14:45 Reynald Affeldt(AIST)
Jacques Garrigue(Nagoya Univ.) Formalization of Error-correcting Codes using SSReflect
14:45 - 15:15 Fadoua Ghourabi(Kwansei Gakuin Univ.)
Formalization of matrix representation of direction relations with application to the superposition of rectangles

15:15 - 15:45 Yoshinori Tanabe
(NII) Coq code extraction to Scala and its correctness

Session Chair: Mitsuharu Yamamoto
16:00 - 16:30 Kentaro Okumura (Kyoto Univ.)
Formalization of Featherweight Java on Coq by using weak HOAS
16:30 - 17:00 Masahiro Yasugi (Kyushu Institute of Technology)
Towards Design of Universal Typed Intermediate Languages in Consideration of Memory Models
17:00 - 17:30 Masahiro Sato (Nagoya Univ.)
An intuitionistic Set-theoretical Model of the Extend Calculus of Construction

17:45 - 18:30 TPPmark2014
https://github.com/KyushuUniversityMathematics/TPP2014/wiki

--
Dec. 5, 2014

Session Chair: Yoshihiro Mizoguchi
09:30 - 10:30 Shunsuke Yatabe (JR West)
Preparing formal specifications: uses of semiformal methods
in the concept phase of a system design

Session Chair: Yoshihiro Mizoguchi
10:40 - 11:10 Kenichi Kuga(Chiba Univ.), Manabu Hagiwara(Chiba Univ.)
On formalization of basic geometric topology
11:10 - 11:40 Takafumi Saikawa (Nagoya Univ.)
Formalizing a coding theory
11:40 - 12:10 Tetsuo Ida (Tsukuba Univ.)
Formalization of geometric algebra with application to computational origami

Session Chair: Jaques Garrigues
13:30 - 14:30 Cyril Cohen (INRIA)
Mathematical Components and Algebraic Numbers

Session Chair: Shun'ichi Yokoyama
14:45 - 15:45 Kazushi Ahara (Meiji Univ.)
Interactive geometry software and automated theorem proving
- Cinderella and Kids Cindy

16:00 Closing

高信頼なソフトウェア開発のために必要な形式手法・ソフトウェア検証・数学の形式化・数学の証明のコンピュータによる検証, といった事項をテーマとし, 定理証明器に関心のある多くの参加者により研究発表, 実践報告, 討論が行われた.

特に, 米MITにおいてプログラム検証について研究を行っているAdam Chlipala氏, 仏INRIA研究所において数学理論の形式証明のためのライブラリ開発等に従事しているCyril Cohen氏, また, 産業界からは, ICカード(おさいふ携帯)の形式仕様策定に従事されたフェリカネットワークスの栗田太郎氏, デジタル放送のプログラム検証等に従事するITプランニング社の今井宣洋氏, そして, 幾何学における数学ソフトウェアを専門とする明治大学の阿原一志氏に特別講演をお願いした.

実問題の中でプログラムとして実装される様々な数学理論, そして, 数理論理学などの数学研究者, プログラム言語理論, ソフトウェア工学などの計算機科学者, さらには, 現実にソフトウェア開発に従事している開発技術者らが約80名集い, 充実した情報交換と討論を行うことが出来た.

それぞれの分野における現状の把握, 問題点の明確化, そして, 定理証明器を用いた高信頼なソフトウェア開発を行うための方向性のアイデアを出し合えた.

また, TPPmarkと称して具体的な問題に既存の定理証明器による形式証明を与え, その証明方法や定理証明器の特徴についての意見交換会も行った. 問題としては, 大学入試問題レベルの数学の論証問題を提示した. 国内外から7種類の定理証明器による15件の応募があり, 有意義な意見交換が出来た.

本来, 正しいプログラムの検証のために開発された定理証明器が近年, 証明の正しさの確認が難しい数学定理の証明の検証のために利用されて来ている. 例えば, 定理証明器Coqによる証明検証では, Gonthier氏らによる平面グラフの四色定理(2004), 群論の奇数位数定理(2012), Affeld氏らによるシャノンの定理(2012), Mahboubi氏らによるアペリーの定理(2014)などの数学定理の形式証明がある. さらに, HOL Light/Isabelleによる証明では, Hales氏らによる10年来の検証プロジェクトで, 昨年夏にその完成が公表された, 3次元空間の球充填問題「ケプラー予想」の形式証明がある. これらの例のように, 定理証明器は実用の域に来ている. 数学理論の形式証明は数学理論そのものの発展のためだけではなく, 数学理論を用いた応用プログラムの実用性のための検証には不可欠なものである. 今後, 数学理論とプログラミングが定理証明器を介して同時並行的に進化しなければならない状況が明らかになって来た.

数学理論は数学の問題としての重要性にのみ着目されがちで, その理論の構成方法, また, その証明方法については, なかなか議論されることが少なかった. 証明方法から, 理論の構成方法にある程度の指針が見えて来ることもある. 実問題の計算機での解決を考えるとき, 問題=定理, プログラム=証明に対応するが, プログラム出来ない問題を考えることは実用上意味がない, というか, いかに解決出来るように問題を整理するのかということが重要になる. 計算機の計算能力が進歩した昨今, 人が今まで数学の中で考えて来た, 計算(数に限らない思考手続き)を具体的な定理証明器の上で再構築することの実現可能性が見えて来ただけでなく, その重要性が明らかになって来た. もうひとつ明らかになったことは, 数学,計算機科学,プログラミング言語,計算機システム,システム工学など, 形式化の視点から交流することで, それぞれの立場でのシステム化の問題点が見えて来ること, また, 解決に必要な定理証明器の方向性も少しだけ見えて来た.

このような機会は, 是非, 継続され, また, 拡大されるべきだと思う. 本課題は数学と諸分野の恊働ではあるが, 計算機に関わる分野においても, プログラミング言語の理論研究とソフトウェア工学の応用研究においては, 交流が十分とは思われない. その仲介を, 定理証明器を用いた数学の形式証明に関する研究を通して行うことが出来る. 数理論理学や様々な数学理論の形式証明に関する研究は, その方法論において, 実問題のプログラムによる解決へと直接的に結びつく. TPPmark2014の問題と解答については,  今後の定理証明器の発展を祈念しつつ, レポジトリに保存し記録として公開し続ける.
https://github.com/KyushuUniversityMathematics/TPP2014/wiki