| Project/Area Number |
22700028
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
GARRIGUE Jacques 名古屋大学, 多元数理科学研究科, 准教授 (80273530)
|
|---|
| Project Period (FY) |
2010-04-01 – 2014-03-31
|
| Project Status |
Completed (Fiscal Year 2013)
|
| Budget Amount *help |
¥3,250,000 (Direct Cost: ¥2,500,000、Indirect Cost: ¥750,000)
Fiscal Year 2013: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2012: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2011: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2010: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
|
|---|
| Keywords | 型推論 / アルゴリズムの証明 / モジュールの証明 / 国際情報交換 / モジュール / 交際情報交換 / プログラミング言語論 / プログラムパラダイム / 定理証明支援系 |
|---|
| Research Abstract |
The only way to be completely certain of the correctness of a program is to prove it formally using a mechanical theorem prover. In this research, I aimed at formally proving the correctness of a type checker for a part of the OCaml functional programming language, to include it in a fully certified interpreter.
Concretely, based on the Engineering Metatheory approach, I formalized a small language including structural polymorphism, which allows to type OCaml objects and polymorphic variants, and proved its type soundness, the soundness and completeness of its type inference, and the correctness of its evaluation through a stack-based interpreter. Moreover, we obtained some concrete proofs concerning the so-called "relaxed value restriction" required for the typing of side-effects, and the coherence check for structural recursive type definitions.
|
