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