ワークショップ情報
研究 集会
「
TPP (Theorem Proving and Provers Meeting)は, 2005
報告 書 :
研究 集会 「高信頼 な理論 と実装 のための定理 証明 および定理 証明 器 」(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 (
産業 技術 総合 研究所 )
主催
共催
「
後援
※ この
