An Interaction-Based language and Its typing system

Proceedings of Parallel Architectures and Language，Europe ，Lecture Note in Computer Science

共著者：竹内格・本田耕平 連続相互通信を基本とした言語Ｌとその型システムを定義する。Ｌは、既存の形式系の集合・代数的なプロセス生成と並行合成ではなく、連続した通信を表現する三対の通信構成子によってプログラムを記述する。これらは、通信における型を明確に記述することにより、形式的操作意味論や論理に基づく型推論システムを定義した。また、型付けされたプログラムは、実行時に型誤りを生じない定理が示される。