PPL2015 Poster

Actario: Coqによるアクターモデルの形式化とErlangへのコード抽出 (ポスター)

安武祥平，渡部卓雄
第17回プログラミングおよびプログラミング言語ワークショップ(PPL 2016), Mar. 4-6, 2015.

概要

定理証明支援系Coqによるアクターモデルの形式化手法を提案し、Actarioというライブラリとして実装した。 Actarioではアクターモデルの構文と意味論を提供している。アクターの名前が階層構造を持つように設計し、この意味論において初期状態から任意の遷移によって動的に生成されるアクターの名前が重複しないことの証明を行った。 また、ActarioにはErlangへのコード抽出の機構も含まれている。これは既存のコード抽出の機構をErlangについて拡張したCoqプラグインになっており、Actarioを用いて書かれたアクターシステムのコードが抽出できるようになっている。