2013 Fiscal Year Final Research Report
Mechanically certified proof of a type checker for an advanced type system
| 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
|
| 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.
|
-
-
-
-
-
-
-
-
-
[Presentation] A syntactic type system for recursive modules2011
Author(s)
Hyonseung Im, Keiko Nakata, Jacques Garrigue and Sungwoo Park
Organizer
ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications
Place of Presentation
Portland, Oregon (査読有 DOI 10.1145/2048066.2048141)
Year and Date
20111000
-
-
-
-
-
