2010 Fiscal Year Annual Research Report
進んだ型システムを持ったプログラミング言語における型検証器の機械的な証明
| Project/Area Number |
22700028
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
J Garrigue 名古屋大学, 多元数理科学研究科, 准教授 (80273530)
|
|---|
| Keywords | プログラミング言語論 / プログラムパラダイム / 定理証明支援系 |
|---|
| Research Abstract |
この一年で、研究計画にあった検証された型推論およびインタープリタの値多相性への拡張を進めるのと同時に、前段階での結果をAPLASという上海で開催された国際学会で発表した。分かりやすくするための証明の修正も行った。
また、フランスのENSリヨンから来たPierre-Marie Pedrotと一緒に、同じ定理証明支援系Coqの中で住井英二郎氏の「環境相模倣」という証明法を実現する実験を行った。環境相模倣を使うと比較的簡単にプログラムの同値性が証明できるので、最適化の正しさなどが証明できると期待されている.検証されたインタープリタなどは証明のために効率が悪くなる恐れがあるので、こういう方法でより効率の良いプログラムの正しさが証明できるはずだ。
さらに、カナダのConcordia大学から来たJacques Le Normandと一緒にObjective CamlにGADTを追加した。GADTは「拡張された代数的データ型」という意味で、通常のプログラミング言語の中で証明にあるような依存性のある場合分けを可能にする。型システムを拡張しているので、ある意味で「検証された型推論」という目的をさらに難しくしているが、同時にGADTを使うことで通常のプログラミング言語でも一部の性質の証明が可能になるという利点がある。全ての性質をCoqで証明するのは難しいので、停止性等が求められていないコードについて必要な性質だけをGADTで証明し、Coqで書かれたコードと安全にリンクするというアプローチが考えられる.
|
Research Products
(3 results)
