Choreographic Programming (CP) は、分散システムをデッドロックなく記述するためのプログラミングパラダイムであり、単一のプログラムから各エンドポイントのコードを生成することで通信の整合性が保証できるものである。

本研究では、CP をエフェクトシステムとコフェクトシステム基づき形式化する新しい計算体系を提案する。通信をエフェクト、複数のエンドポイントで利用可能な値 (multiply located values) をコフェクトとして捉え、それぞれエンドポイントの集合を添字とした型体系を構成した。この型システムでは、プログラムの各断片において通信に必要なエンドポイントとコンテキスト内の変数の所在をトラッキングすることでき、実行における種々の制約を表現することを可能となる。また、ネットワーク全体の評価規則を定義し、進行性と型保存性を証明することで、本体系においては常にデッドロックが発生しないことを示した。

さらに、本体系を Haskell 上で実装し、従来の添字を持たない単一モナドによる実装に比べてより柔軟に CP を記述できる点を確認した。