並行プログラムについての理論に対する単純明快なアプローチは、並行プログラムの動作を個別スレッドのアトミックアクションのすべての可能なインターリービングのセットとして定義することです。しかし、インターリービングについての理論は、インターリービングが可能な数が急速に増加するため、人間とコンピューターの両方にとって難しすぎます。

pomset 言語やイベント構造など、並行性の非インターリービングモデルは、プログラムの動作セットのよりコンパクトな表現を提案することで、この問題に対処しようとします。近年、緩和メモリモデルのコンテキスト、並行プログラムのモデルチェック、およびモデルベースのミューテーション解析などにおいて、非インターリービングの並行性モデルが改めて着目されるようになりました。

このプロジェクトは、Coq Proof Assistant における非インターリービング並行性モデルの機械化理論を開発することを目標としています。ライブラリは、興味を持つ研究者がこれらのモデルのプロパティを正式に証明し、理論の新しいアプリケーションを開発する上で役立つはずです。

プロジェクトのリポジトリ