進んだ型システムを持ったプログラミング言語における型検証器の機械的な証明

• 研究課題/領域番号: 22700028
• 研究種目: 若手研究(B)
• 配分区分: 補助金
• 研究分野: ソフトウエア
• 研究機関: 名古屋大学
• 研究代表者: J Garrigue (GARRIGUE Jacques) 名古屋大学, 多元数理科学研究科, 准教授 (80273530)
• 研究期間 (年度): 2010-04-01 – 2014-03-31
• 研究課題ステータス: 完了 (2013年度)
• 配分額: 3,250千円 (直接経費: 2,500千円、間接経費: 750千円); 2013年度: 780千円 (直接経費: 600千円、間接経費: 180千円); 2012年度: 780千円 (直接経費: 600千円、間接経費: 180千円); 2011年度: 780千円 (直接経費: 600千円、間接経費: 180千円); 2010年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
• キーワード: 型推論 / アルゴリズムの証明 / モジュールの証明 / 国際情報交換 / モジュール / 交際情報交換 / プログラミング言語論 / プログラムパラダイム / 定理証明支援系

研究概要

プログラムの完全な正しさを保証するには、プログラムの論理自体を機械上に証明するしかない。この研究では，OCamlと同等の機能をもった型検証器を完全に証明し，正しさを証明されたプログラミング言語の実装の中心に据えることを目指した。具体的には、Aydemir等のEngineering Metatheoryという手法に基づいてOCaml特有の構造的多相性（オブジェクトおよび多相ヴァリアント）を形式化し、型システムの健全性、型推論の健全性と完全性、スタックベースのインタープリターの正しさを形式的に証明した。さらに副作用のための「緩和された値限定多相性」や再帰的型定義の検証の一部も証明した。

研究成果

• [雑誌論文] A Certified Implementation of ML with Structural Polymorphism and Recursive Types (2014)
  • 著者名/発表者名: Jacques Garrigue
  • 雑誌名: Mathematical Structures in Computer Science 巻: to appear
  • 査読あり
• [雑誌論文] Ambivalent types for principal type inference with GADTs (2013)
  • 著者名/発表者名: Jacques Garrigue, Didier Remy
  • 雑誌名: APLAS 2013, Springer Verlag LNCS 巻: 2301 ページ: 257-272
  • DOI: 10.1007/978-3-319-03542-0_19
  • ISBN: 9783319035413, 9783319035420
  • 査読あり
• [雑誌論文] Path resolution for recursive nested modules (2012)
  • 著者名/発表者名: Jacques Garrigue, Keiko Nakata
  • 雑誌名: Higher-Order and Symbolic Computation 巻: 24 号: 3 ページ: 207-237
  • DOI: 10.1007/s10990-012-9083-6
• [雑誌論文] A Syntactic Type System for Recursive Modules (2011)
  • 著者名/発表者名: H.Im, K.Nakata, J.Garrigue, S.Park
  • 雑誌名: ACM SIGPLAN Notices-OOPSLA'11 巻: (46)10 号: 10 ページ: 993-1012
  • DOI: 10.1145/2076021.2048141
  • 査読あり
• [雑誌論文] A Certified Implementation of ML with Structural Polymorphism (2010)
  • 著者名/発表者名: Jacques Garrigue
  • 雑誌名: APLAS 2010, Shanghai, Springer-Verlag LNCS 巻: 6461 ページ: 360-375
  • 査読あり
• [雑誌論文] A certified implementation of ML with structural polymorphism and recursive types
  • 著者名/発表者名: Jacques Garrigue
  • 雑誌名: Mathematical Structures in Computer Science 巻: (to appear)
• [学会発表] Ambivalent types for principal type inference with GADTs (2013)
  • 著者名/発表者名: Jacques Garrigue and Didier Remy
  • 学会等名: ￥em 11th Asian Symposium on Programming Languages and Systems
  • 発表場所: Melbourne (Springer-Verlag LNCS 8301, 257-272 DOI:10.1007/978-3-319-03542-0_19)
• [学会発表] On variance, injectivity, and abstraction (2013)
  • 著者名/発表者名: Jacques Garrigue
  • 学会等名: OCaml Workshop
  • 発表場所: Boston (査読無)
• [学会発表] Runtime types in Ocaml (2013)
  • 著者名/発表者名: Jacques Garrigue and Gregoire Henry
  • 学会等名: OCaml Workshop
  • 発表場所: Boston (査読無)
• [学会発表] On variance, injectivity, and abstraction (2013)
  • 著者名/発表者名: Jacques Garrigue
  • 学会等名: OCaml Workshop
  • 発表場所: Boston, USA
• [学会発表] Runtime types in OCaml (2013)
  • 著者名/発表者名: Jacques Garrigue and Gregoire Henry
  • 学会等名: OCaml Workshop
  • 発表場所: Boston, USA
• [学会発表] Path resolution for recursive nested modules (2013)
  • 著者名/発表者名: Jacques Garrigue
  • 学会等名: プログラミングおよびプログラミング言語研究会
  • 発表場所: 会津若松
• [学会発表] Tracing ambiguity in GADT type inference (2012)
  • 著者名/発表者名: Jacques Garrigue and Didier Remy
  • 学会等名: ACM SIGPLAN Workshop on ML
  • 発表場所: Copenhagen (査読無)
• [学会発表] More Logic More Types (2012)
  • 著者名/発表者名: Jacques Garrigue
  • 学会等名: ML Nagoya
  • 発表場所: 名古屋ルーセントタワー (査読無)
• [学会発表] Avoiding binders : rooted recursive modules and semantic polymorphism (2012)
  • 著者名/発表者名: Jacques Garrigue and Thomas Leventis
  • 学会等名: 第8回定理証明および定理証明系に関する研究集会
  • 発表場所: 千葉大学 (査読無)
• [学会発表] Tracing ambiguity in GADT type inference (2012)
  • 著者名/発表者名: Jacques Garrigue
  • 学会等名: ACM SIGPLAN Workshop on ML
  • 発表場所: Copenhagen, Denmark
• [学会発表] Adding GADTs to OCaml : a direct approach (2011)
  • 著者名/発表者名: J.Garrigue, J.Le Normand
  • 学会等名: ACM-SIGPLAN Workshop on ML
  • 発表場所: 学術総合センター(東京都)
  • 年月日: 2011-09-18
• [学会発表] Objective CamlへのGADTの導入 (2011)
  • 著者名/発表者名: J.Garrigue, J.Le Normand
  • 学会等名: 日本ソフトウェア科学会PPL2011
  • 発表場所: 定山渓
  • 年月日: 2011-03-10
• [学会発表] A syntactic type system for recursive modules (2011)
  • 著者名/発表者名: Hyonseung Im, Keiko Nakata, Jacques Garrigue and Sungwoo Park
  • 学会等名: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications
  • 発表場所: Portland, Oregon (査読有 DOI 10.1145/2048066.2048141)
• [学会発表] Adding GADTs to OCaml : a direct approach (2011)
  • 著者名/発表者名: Jacques Garrigue and Jacques Le Normand
  • 学会等名: ACM SIGPLAN Workshop on ML}
  • 発表場所: Tokyo (査読無)
• [学会発表] A certified implementation of ML with structural polymorphism (2010)
  • 著者名/発表者名: Jacques Garrigue
  • 学会等名: 8th Asian Symposium on Programming Languages and Systems
  • 発表場所: Shanghai (Springer-Verlag LNCS 6461, 360-375 査読有 DOI:10.1007/978-3-642-17164-2_25)
• [学会発表] First-class modules and composable signatures in Objective Caml 3.12. (2010)
  • 著者名/発表者名: Jacques Garrigue and Alain Frisch
  • 学会等名: ACM SIGPLAN Workshop on ML
  • 発表場所: Baltimore (査読無)
• [学会発表] an attempt at proving environmental bisimulations in Coq (2010)
  • 著者名/発表者名: Jacques Garrigue and Pierre-Marie Pedrot, Simpoule
  • 学会等名: 第6回定理証明および定理証明系に関する研究集会
  • 発表場所: 名古屋大学 (査読無)
• [備考]
  • URL: http://www.math.nagoya-u.ac.jp/~garrigue/
• [備考] A Certified Implementation of ML
  • URL: http://www.math.nagoya-u.ac.jp/~garrigue/papers/aplas2010.html
• [備考] Publications of Jacques Garrigue
  • URL: http://www.math.nagoya-u.ac.jp/~garrigue/papers/
• [備考]
  • URL: http://www.math.nagoya-u.ac.jp/~garrigue/papers/index.html
• [備考]
  • URL: http://www.math.nagoya-u.ac.jp/~garrigue/papers/