Formal Proof of the Congruence Theorem between Operational Semantics and Denotational Semantics on Traces of CSP in Isabelle/HOL

  • 0
    いいね
  • 0
    コメント

    並行システムの理論 CSP (Communicating Sequential Processes) の表示的意味論の1つであるトレース意味論と操作的意味論の等価性について,定理証明支援器 Isabelle/HOL による形式的証明に成功したので,概要をご紹介したいと思います.

    www.principia-m.com/ts/0131/index-jp.html

    この投稿は Theorem Prover Advent Calendar 20163日目の記事です。