非同期通信するプログラムを形式的証明から抽出してバグを防ぐ研究

点击翻译按钮获取中文摘要

ゲーデル・ダメット論理の証明から非同期通信する並行プログラムを抽出する方法をみつけて、FLOPS2012という国際学会で発表した。交付申請書に記載した研究目的にあるとおり、直観主義論理の証明からプログラムを抽出するプログラム抽出の技法を応用したといえる。ゲーデル・ダメット論理は直観主義論理の拡張であり、今回の研究で抽出したプログラムはもともと直観主義論理の証明から抽出できていた型付きラムダ計算の拡張である。さらに、研究目的にあるとおり、抽出されるプログラムは非同期通信する並列プログラムである。本研究の最も重要な結果は、無待機計算で解ける問題はゲーデル・ダメット論理をもとにしたプログラミング言語で解けるし、ゲーデル・ダメット論理をもとにして解ける問題は無待機計算で解けるという特徴付けの結果である。論理学への貢献はゲーデル・ダメット論理の計算的意味を明らかにしたことであり、計算機科学への貢献は無待機計算用のプログラミング言語を発見したことである。ゲーデル・ダメット論理の計算的意味が何かという問題は1991年にArnon Avronによって提起されて以来解かれないまま20年以上の時間が経過した。本研究ではこの古い問題を解けた。無待機計算は、理論計算機科学で、1990年代に注目された概念であり、2004年のゲーデル賞は無待機計算の位相幾何学的特徴付けという仕事に与えられた。本研究では、無待機計算のプログラミング言語による特徴付けを実現した。