精密化計算とタイプ理論は,プログラムの仕様と検証をサポートする両方のフレームワークである。本論文では,相互作用定理証明器Coqにおける精密化計算の埋め込みを示し,2つの間の関係を明らかにした。結果として,Coqにおいて精密化計算を実行することができ,それらの仕様から形式的に検証されたプログラムの相互作用計算を可能にした。Copyright 2018 Elsevier B.V., Amsterdam. All rights reserved. Translated from English into Japanese by JST.【JST・京大機械翻訳】