Discovery Sagaサイレントキーワード俯瞰

本研究の目的は、論理学、特に論理学の一分野である証明論の手法を用いて、新しいマルチ・パラダイム・プログラム言語の計算モデルの理論を確立し、これに基づいて論理的マルチ・パラダイム・プログラム言語の設計を行うことにある。特に、証明論における証明の正規化概念が、論理的新世代プログラム言語(タイプ付関数型言語、論理言語、代数的仕様言語(項書換え言語))の計算概念と密接に関係していることに着目して、新しいマルチ・パラダイム・プログラム言語の計算理論を論理学における証明の正規化問題に還元して、新しい形の証明の正規化定理を与えることにより、新しいプログラム言語の計算モデルを確立する、という手法をとった。まず、強力なタイプ付関数型言語(MLやTheory of Constructions等)と項書き換えシステムに基づく代数的仕様言語(OBJ等)とを統合したマルチ・パラダイム言語の計算モデルを上の証明論的手法を用いて確立し、このマルチ・パラダイム言語がAbstract Data Type言語として非常に有用な性質を持つことを示した。又、我々が確立した計算モデルを基にして、このマルチ・パラダイム言語の実装を行い、PTA(Rewriting Technigues and Application)国際会議等の場でデモンストレーションを行なった。我々の確立したマルチ・パラダイム言語の計算モデルの理論をHuet-CoguentのTheory of CostructionsとGoguen等のOBJとの統合言語に適用することにより、OBJのフレームワークを用いてADTの代数的仕様を与え、Theory of Constructionsのタイプ推論を用いて、仕様の検証の証明を与えることができる。又上の言語は、Girardの線形論理をベースに置くことにより並行計算プログラム言語としての特徴も持つこととなる。特に、自己言及的述語を含む述語論理を線形論理上で与え(これをmobile linear logicと呼ぶ)ることにより、milnerのπ計算の表現力を持つ言語が確立さらた。