安全・高信頼ソフトウェアシステムのための高階・型付き・並行プログラミング言語理論

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

本研究の目的は以下のとおりであった。現代社会の基盤をなす科学技術である情報処理システム（いわゆる計算機プログラムを基礎とするが、それに限らず、より幅広い意味でのソフトウェアシステムを含む。）の安全性・信頼性ならびに生産性を高めるため、数理論理学に基づいてシステムを記述し正しさを検証するプログラミング言語理論を発展させ、狭義のプログラミング言語のみならず、より一般的な計算モデルにおける広義の「プログラム」としてのシステム記述に用いる。特に、最近の発展・普及が目覚ましい、高度な型システムや高階(higher-order)および並行(concurrent)・分散プログラムないしプログラミング言語に関する理論の研究を行う。当年度は以下を含む研究を研究協力者らとともに、他の研究とも連携して行なった。・構造化グラフの正規化の証明：関数的(functional)な表現が難しいとされるグラフ構造を関数的に表現する手法の一つであるOliveira-Cookの構造化グラフ(structured graph)において、表現（項）の冗長性を取り除くための正規化(normalization)の規則を定義・証明した。・複数参加者セッション型の一般プロセス型への変換：複数の参加者（プロセス）が通信を行う並行プロセス計算(concurrent process calculus)において、通信のプロトコル（順序等の手順）を表すセッション型(session type)から、プロセスの入出力の振る舞いを表すIgarashi-Kobayashiの一般型システム(generic type system, GTS)への変換を定義し、両者の関係を明らかにした。