プログラムの等価性と非干渉性に関する完全な関係的Hoareロジックの構築

本論文では、プログラムの等価性や非干渉性などの関係的性質を証明するための完全な関係的Hoareロジックを提案する。これには、プログラムの構造を上手く整列させるための新しいルールや、非決定性を扱うための拡張が含まれる。また、既存の関係的Hoareロジックでは扱えない例題に対しても、新しいルールを導入することで証明可能であることを示す。