日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

Aπ 計算の Coq による形式化
安武 祥平

渡部 卓雄

アクターモデルは並行計算のモデルのひとつであり，互いに非同期メッセージをやりとりするアクターと呼ばれる計算主体によって計算システムを表現する．アクターモデルのもつ性質には，アクターの名前の一意性と新鮮性，およびアクターの永続性が含まれる．これらの性質を π 計算の型システムとして導入し，アクターモデルを形式化した
Aπ 計算が Agha らによって提案されている．A π計算の型システムにおける健全性とは，型付けされた項はアクターモデルとしてのふるまいを示すということであるが，その証明は形式的に与えられていない．本研究では，Aπ計算およびその型システムの定義をみなおすことで，型システムの健全性について定理証明支援系 Coq を用いた形式的な証明を与える．

The Actor model is a model of concurrent computation based on autonomous computing entities called
actors that communicate through asynchronous message passing. The properties of the Actor model include uniqueness and freshness of actor names and persistency of actors. Agha et al. proposed a typed
asynchronous variant of π-calculus called Aπ-calculus whose type system imposes these three properties.
In Aπ-calculus, the soundness of the type system means that a typed term certainly behaves as an actor
configuration. In this paper, by reconsidering the definitions of the terms and types of Aπ-calculus, we givea formal proof of the soundness using Coq.

は喫緊の課題であると考えられる．

1 はじめに形式的検証の研究に先立ち，アクターモデルの形式

アクターモデル [1] は並行計算のモデルのひとつで的意味論については古くから研究が行なわれてきた．

あり，互いに非同期メッセージをやりとりするアク

例えば Clinger による Powerdomain を用いた表示的ターと呼ばれる計算主体 (computing entity) によっ

意味 [5] や，Agha による操作的意味 [1] とその発展 [2]て計算システムを表現する．他の並行計算モデル，例がある．これらの研究では，公平性やいくつかの等価えば π 計算などと比較すると，アクターモデルは実性についての成果があるものの，プロセス代数を元に装しやすく，またプログラミングも比較的容易である

発展してきた π 計算等に比べると発展途上であるとと考えられる．実際，アクターモデルやその発展形で言わざるを得ない．

ある並行オブジェクト計算モデル [12] にもとづく言語

一方，形式的検証についてはアクターで記述されたは多数提案・実装されてきており，それらの研究成果システムのモデル検査を可能にするモデル記述言語

をもとに現在 Scala や Erlang, Akka 等，アクター

Rebeca [11]，証明支援系を含むプログラミング言語

モデルを並行計算の基盤としたプログラミング言語

Athena を用いた検証例 [10]，および Coq を用いたアやライブラリが実用に供されている．そのため，アククターモデルの定式化と検証例 [7] など，最近になっターモデルによって構成されたシステムの形式的検証ていくつかの研究成果が出ている．本研究はアクターで構成されたシステムの Coq による形式的検証のた

A formalization of Aπ-calculus using Coq
Shohei Yasutake, 東京工業大学大学院情報理工学研究科, Dept. of Computer Science, Tokyo Institute ofTechnology.

めの枠組みを提供することを目的としている．
アクターモデルのもつ性質には，アクターの名前は一意であるという性質 (名前の一意性)，メッセージ

として送られてきた名前でアクターを作ることはでた，窓口の集合のことを窓口集合 (receptionist set)

きないという性質 (名前の新鮮性)，アクターにはいという．

つでもメッセージを送ることができるという性質 (ア2. 1. 2 アクターモデルの性質クターの永続性) が含まれる．これらの性質をみたす

アクターモデルが満たすべき性質として，以下が項を構成するよう π 計算に型システムを導入し，アある．

クターモデルを形式化した Aπ 計算が Agha らによっ

一意性 (uniqueness property)て提案されている [3]．

Aπ 計算の型システムにおける健全性とは，型付けアクターの名前は一意である．
新鮮性 (freshness property)

された項はアクターモデルとしての振る舞いを示す

アクターが作られるとき，作られるアクターのということであるが，その証明は形式的に与えられて名前はまだどのアクターの名前でもない．アクいない．本研究では，Aπ 計算およびその型システム

ターは，メッセージとして送られてきた名前でアの定義を見直すことで，型システムの健全性についてクターを作ることはできない．

定理証明支援系 Coq を用いた形式的な証明を与える．

永続性 (persistence property)
アクターは消えない．一旦アクターが作られる

2 背景知識と，いつでもそのアクターにメッセージを送るこ

2. 1 アクターモデルとができる．

アクターモデルは非同期メッセージ通信に基づいた並行計算のモデルである．アクターと呼ばれる計算主

2. 2 π 計算体があり，それらは名前 (またはアドレス) と内部状

π 計算は，Milner らによって提唱された並行計算態をもっている．各アクターは並列に動作し，非同期のモデルである [9]．プロセスと呼ばれるオブジェクにメッセージを送り合うことでコミュニケーションをト同士が通信しデータを受け渡していくことで計算をとる．

進める．また，アクターモデルとは異なり，メッセー

アクターは，メッセージの内容に応じて一定の動作を行う．これを振る舞い (behavior) という．振る舞
いには以下の様なものがある．

ジを送受信する際にはプロセス間で同期をとる必要がある．

π 計算の抽象構文は 図 1 のようになっている．こ• 他のアクターにメッセージを送信する．

こで，P, P1 , P2 , ... はプロセスの式，x, y, ... は名前で• 新しいアクターを作る．

ある．

• 自らの振る舞いを変える．
2. 1. 1 配置

P ::= 0

何もしない

アクターモデルにおける配置 (configuration) とは，| x(y).P

x から値を受け取り，P 中の y に束縛する

アクターモデルの世界におけるその時点での状態を| x̄⟨y⟩.Px へ y を送る

切り取ったものを表すための概念である．配置はア| P1 |P2

P1 , P2 を並列に実行させる

クターとその振る舞い，まだ受け取られていないメッ| (νx)P

P 中に現れる x を束縛するセージの集合から表される．

| !P

P を繰り返す

配置内の，配置外からのメッセージを受け取ることのできるアクターを，窓口 (receptionist) という．
アクターは，送り先の名前 (アドレス) を知ることで，その名前のアクターにメッセージを送れるようになる，よって窓口は外部のアクターに自身の名前を知られているアクターと言い換えることができる．ま図 1: π 計算の文法表 1: カリー・ハワード同型対応

P ::= 0 | x(y).P | x̄y | (νx)P | P1 |P2| case x of (y1 : P1 , ..., yn : Pn )論理

コンピュータプログラム

命題 P型P

命題 P の証明型 P を持つ項

命題 P ⇒ Q型 P -> Q (P から Q への関数)

命題 P ∧ Q

P, Q の直和型セス) にメッセージを送ったあとにさらに何かを実行

命題 P ∨ Q

P, Q の直積型

できないこと，名前の場合分けが書けること，振る舞| ((ũ, ṽ)u1 (z).P )(x̃, ỹ)
図 2: Aπ 計算の配置の文法
通常の π 計算と異なる点は，他のアクター (プロいの雛形からアクターを作るための文法があること，

2. 3 定理証明支援系 Coqの 3 つである．

Coq はフランス国立情報学自動制御研究所で開発されている定理証明支援系である [6]．Coq を用いる

3. 2 型システムの導入

ことで，プログラムがある仕様を満たすということ

Aπ 計算の文法のみでは，アクターモデルの性質や，数学的な定理などに対して形式的かつ厳密な証明は満たさないような配置も書けてしまう．例えば，を与えることができる．Coq によって証明されたもx(u).P |x(v).Q は Aπ 計算の文法で書けるが，x とのとしては，四色定理が有名である [8]．

いう名前のアクターが 2 つ作られるので，一意性を2. 3. 1 カリー・ハワード同型対応満たしていない．また，x(u).(u(v).P |x(v).Q) も Aπ

Coq における定理証明は，カリー・ハワード同型計算の文法で書けるが，メッセージとして送られてき対応という理論に基づいている．カリー・ハワード同た名前でアクターが作られているので，新鮮性に反型とは，論理における命題と証明という構造と，コンする．

ピュータプログラムにおける型と項という構造が直また，アクターモデルでは，1 回の通信で複数の名接的に対応しているという理論である．これにより，前を送信することができるが，Aπ 計算では 1 回の通ある命題を証明することが，命題に対応する型と，そ信で一つの名前しか送ることはできない．複数の名前の型を持つ項を作ることに帰着される．

を送信するには，その数だけ連続して通信する必要がカリー・ハワード同型対応では，表 1 に示すような対応関係がある．

ある．しかし，アクターモデルではこのような複数の名前を含むメッセージの受け渡しはアトミックに行なわれ，即座に次のメッセージを受け取れる状態になら3 Aπ 計算なければいけない．そこで，いつでもメッセージを送

本節では，アクターモデルの振る舞いを強制する信できるという永続性を弱め，アクターはメッセージために非同期 π 計算に型を付けた Aπ 計算についての送信先のアクターの処理が終わるまで待てるよう説明する．まず Aπ 計算における配置の定義をする．にする (いつかは必ず送れる)．そしてアトミックに次に型システムを導入するが，その際に仮名関数と行うことのできない処理の最中はメッセージを送れいう関数を導入し，型付け規則を定義する．最後にないということを，正規の名前を隠して一時的な名

この型システムにおける健全性について述べる．ま前を使って処理を行うことで実現させる．ここで，仮た，Aπ 計算の定義および使われている記号は，文献の名前をとった後，元の名前とは異なる名前になって[3] で用いられているものを用いる．

しまうと，そのアクターにメッセージを送ろうとしているアクターはメッセージを送れなくなってしまい，3. 1 配置

永続性に反する．仮の名前をとったときには必ず元のAπ 計算における配置の文法は，図 2 のようになっ名前に戻るという制約が必要である．ている．

以上のような性質を満たすようにするため，型シス

テムを導入し，Aπ 計算に制約を与える．

3. 2. 1 仮名関数
仮の名前は必ず正規の名前に戻るという制約を型システムを用いて与えるためには，仮の名前をとったと(f1 ⊕f2 )(x) =きに正規の名前を覚えておく必要がある．そこで仮のf1 (x)
f2 (x)x ∈ ρ1 かつ f1 (x) ̸= ⊥，または x ∈ ρ1 かつ x ∈/ ρ2 のとき
その他

名前から元の正規の名前にマッピングする関数を導入

定義 3.4 (仮名関数の定義域の制限). f : ρ1 → ρ∗1 , ρ ⊂する．これを 仮名関数 (temporary name mapping

ρ1 である f, ρ に対して定義域の制限を表す二項演算function) と呼ぶ．

子 f |ρ : ρ → ρ∗ を以下のように定義する．

定義 3.1 (仮名関数). 仮名関数 f は，集合 X から集合 X ∗ への写像である．ただし，N を名前全体の集合として，⊥, ∗ ∈/ N , X ⊂ N , X ∗ = X ∪ {⊥, ∗} で(f |ρ)(x) =ある．
仮名関数の入力と返り値の関係は，以下のような意味を持つ．

f (x)

f (x) ∈ ρのとき

∗

その他

3. 2. 3 仮名関数が満たすべき性質
仮名関数 f はその定義から，以下を満たすべきである．

f (x) = ⊥x が正規の名前のとき• f (x) ̸= x

f (x) = ∗x が環境から隠されている• f (x) = f (y) ∈/ {⊥, ∗} ⇒ x = y

名前であるとき• f ∗ (f (x)) = ⊥アクター y の仮の名前がf (x) ̸= x は，仮の名前から正規の名前を得たと

f (x) = y ∈/ {⊥, ∗}x であるとき

き，それは仮の名前と同名ではないという性質である．f (x) = f (y) ∈/ {⊥, ∗} ⇒ x = y は，正規のアク3. 2. 2 仮名関数の構築

ターは 2 個以上の仮の名前をとれないという性質で仮名関数は以下に示す ch 関数，仮名関数の合成，ある．f ∗ (f (x)) = ⊥ は，仮の名前のアクターはさら仮名関数の制限のいずれかで作ることができる．
定 義 3.2 (ch). ch は 名 前 の 組 を と り，仮 名 関 数に仮の名前を持つことはできないという性質である．
また，互換性という性質を定義する．

を返す関数である．組の長さは任意である．組を定義 3.5 (互換性 (compatible)). 二つの仮名関数⟨x1 , x2 , ..., xn ⟩ としたとき，ch(⟨x1 , x2 , ..., xn ⟩) は以

f1 , f2 が以下の性質を満たすとき，f1 , f2 は互換性を下のような仮名関数となる．

持つという．また，この性質を満たすという述語を

ch(⟨x1 , x2 , ..., xn ⟩)(xi ) =compatible(f1 , f2 ) と書く．

xi+1

1 ≤ i < n のとき⊥

i = n のとき

定義 3.3 (仮名関数の合成). f1 : ρ1 → ρ∗1 ，f2 :• f1 ⊕ f2 = f2 ⊕ f1
• f1 ⊕ f2 が仮名関数の性質を満たす
3. 3 型付け規則

ρ2 → ρ∗2 とする．仮名関数の合成を表す二項演算子

Aπ 計算が先に述べた性質を満たすようにするため

f1 ⊕ f2 : ρ1 ∪ ρ2 → (ρ1 ∪ ρ2 )∗ を以下のように定義すの型付け規則は 図 3 のようになっている．配置 P ，る．

P の窓口集合 ρ ，P 中の仮の名前から正規の名前への写像 f : ρ → ρ∗ で， ρ; f ⊢ P が成り立つとき，Pは正しく型付けされている．

(Nil)∅; {} ⊢ 0(Msg)∅; {} ⊢ x̄y

ρ; f ⊢ Pρ − {x} = ẑ

y∈/ρ

f=

ch(⟨x⟩+̃⟨ẑ⟩)x ∈ ρのとき

ch(⟨ẑ⟩)

その他{x} ∪ ẑ; ch(⟨x⟩+̃⟨ẑ⟩) ⊢ x(y).P∀1 ≤ i, j ≤ n, i ̸= j, ρi ; fi ⊢ Pi

compatible(fi , fj )(∪i ρi ); (fi ⊕ f2 ⊕ ... ⊕ fn ) ⊢ case x of (y1 : P1 , ..., yn : Pn )
ρ1 ; f1 ⊢ P1

ρ2 ; f2 ⊢ P2

ρ1 ∩ ρ2 = ϕ

ρ1 ∪ ρ2 ; f1 ⊕ f2 ⊢ P1 |P2
ρ; f ⊢ P
ρ − {x}; f |(ρ − {x}) ⊢ (νx)P{ũ}; ch(ũ) ⊢ u1 (z).Plen(x̃) = 2 ⇒ x1 ̸= x2{x̃}; ch(x̃) ⊢ ((ũ, ṽ)u1 (z).P )(x̃, ỹ)(Act)(Case)(Comp)(Res)(Inst)

図 3: 型付け規則

3. 4 型システムの健全性
Aπ 計算の型システムにおける健全性は，この型システムを満たした Aπ 計算の配置はアクターモデルとしての振る舞いを示すということを表した性質である．単純型付きλ計算における型システムの健全性の3. f (x) = f (y) ̸= {⊥, ∗} ⇒ x = y• ρ′ ; f ′ ⊢ P ならば， ρ = ρ′ かつ f = f ′ (型付けの一意性)
それぞれは以下の意味を持っている．
窓口集合の健全性

ような，正しく型付けされるならば stuck 状態になら窓口集合に属するアクターはメッセージとして送ないという性質とは少し異なることに注意されたい．

られてきた名前で作られたものではなく，かつ環Aπ 計算の型システムの健全性は以下のように定義されている．

境から隠されたものでもない．
仮名の取り方の健全性

定理 3.1 (Aπ 計算の健全性). 配置 P について，アクターが仮の名前をとったとき，それは同名

ρ; f ⊢ P で型付けできたとき，以下の 3 つの性質をのものではなく，さらに仮の名前を持つこともな満たす．

い．また，アクターが複数の仮の名前を持つこと• ρ は P 中に現れる自由名の部分集合である (窓口集合の健全性)• 以下の 3 つを満たす (仮名の取り方の健全性)
1. f (x) ̸= x
2. f ∗ (f (x)) = ⊥はない．
型付けの一意性
配置に型が付いたとき，その型付けは一意である．

みであるが，この中で使われている ch 関数は入力

4 Coq による形式化の要素数が 0 個，1 個，2 個のものしかない．よっ

本節では，3 節で述べた Aπ 計算についてどのようて，ch 関数はこの 3 パターンに限定でき，それぞれに Coq で記述していくかについて説明する．まず仮ch0 , ch1 , ch2 と書くこととする．また，仮名関数の定名関数およびその性質についての Coq での表現を述

義域の制限を行う二項演算子 (|) の第二引数は要素がべる．次に型付け規則を Coq で使いやすくための規

1 個の場合しかなく，要素を 1 個に限定して定義する

則の具体化を説明し，最後に型システムの健全性のと，証明が簡単になる．よって，仮名関数の定義域のCoq での証明方針を述べる．

制限は，以下の定義を用いる．
定義 4.5 (仮名関数の定義域の制限). f : ρ → ρ∗ , x ∈4. 1 仮名関数ρ である f, x に対して定義域の制限を表す二項演算

仮につけた名前から正規の名前を得る 仮名関数の子 f |x : ρ − x → (ρ − x)∗ を以下のように定義する．

Coq での定義について述べる．
仮名関数 f の型は X → X ∗ であり，定義域と値域の集合は ⊥ と ∗ を除くと等しくなっている．Coq
では簡単にするためにその情報を捨て，任意の name(f |x)(y) =∗f (y) = x のとき

f (y)

その他

型の値から任意の option star 型への関数とした．

ま た ，ch0 , ch1 , ch2 , ⊕, | に つ い て 仮 名 関 数 の 性

定義域の範囲に入っていない入力は None を返すこと

質 を 満 た す こ と を 証 明 し た ．そ の 際 ，ch2 はを想定している，

引 数 で あ る 2 つ の 名 前 が 異 な る こ と を ，⊕ はこの変更により，以下の述語が必要となる．f :∗X → X ということを，in range in domain(f ) をin domain in range, f un exclusive が成り立つという前提を加えている．

満たすことで表している．
定義 4.1 (in domain). 名前 x ，仮名関数 f について，x ∈ domain(f ) を in domain(f, x) で表す．た4. 2 型付け規則
Aπ 計算の型付け規則には，Coq 上で定義しにくだし domain(f ) は f の定義域である．

い，またはそのままでは証明を進めにくいものがあ

定義 4.2 (in range). 名前 x ，仮名関数 f についる．実際に Coq で型付け規則を定義する前に，型付て，x ∈ range(f ) を in range(f, x) で表す．ただし

け規則を再定義する．

range(f ) は f の値域である．

4. 2. 1 Act 規則の分割

定 義 4.3 (in range in domain). あ る 仮 名 関 数

型付け規則 Act はアクターが作られる際に考えらf が ，任 意 の 名 前 x に つ い て in range(f, x) ⇒れるパターンを複数まとめたものであり，このままのin domain(f, x) を満たすということを定義を用いると証明を進めることが難しくなってしまin range in domain(f ) で表す．

う．そこで，具体化のため，図 4 のように ρ の要素

また，2 つの 仮名関数の定義域が重なっていないことを表す述語 f un exclusive を定義する．
定義 4.4 (f un exclusive). 2 つの 仮名関数 f : X →数によって場合分けを行い 4 つに分割する．
ここで，ch 関数の入力としてとりうる組は要素数が 0，1，2 のものしかないことに注意されたい．

X ∗ , g : Y → Y ∗ について，X ∩ Y = ∅ であるとい4. 2. 2 Case 規則の分割う述語を f un exclusive と定義する．

型付け規則 Case は，前提の数がパターンの数に4. 1. 1 仮名関数の構築依存して変動するので，Coq で定義しにくい．よっ

仮名関数は ch 関数，仮名関数の合成，仮名関数のて 図 5 のように Case をパターンが 0 個の場合と定義域の制限，のいずれかで作ることができる．こi + 1 に分割し，帰納的に定義する．これで，Case

こで，ch 関数が使われている型付け規則は Act の規則の前提の数はパターンの数によらず一定となる．

∅; ch0 ⊢ P(Act-empty){x}; ch1 (x) ⊢ x(y).P{x}; ch1 (x) ⊢ Px ̸= y(Act-x){x}; ch1 (x) ⊢ x(y).P{z}; ch1 (z) ⊢ Px ̸= zy ̸= z(Act-z){x, z}; ch2 (x, z) ⊢ x(y).P{x, z}; ch2 (x, z) ⊢ Px ̸= zx ̸= yy ̸= z(Act-xz){x, z}; ch2 (x, z) ⊢ x(y).P
図 4: 型付け規則 Act の分割(Case-nil)∅; {} ⊢ case x of ()ρ; f ⊢ case x of (y1 : P1 , ..., yi : Pi )ρ′ ; f ′ ⊢ Pcompatible(f, f ′ )ρ ∪ ρ′ ; f ⊕ f ′ ⊢ case x of (y : P, y1 : P1 , ..., yi : Pi )(Case-cons)

図 5: 型付け規則 Case の分割
また，この定義によって作られる型付けも二つに分割する必要がある．図 7 のようになる．

(...((ρ1 ∪ ρ2 ) ∪ ρ3 )... ∪ ρn ) ∪ ρ; (...((f1 ⊕ f2 ) ⊕ f3 )... ⊕fn ) ⊕ f ⊢ case x of (y : P, y1 : P1 , ..., yn : Pn )4. 3 健全性の証明

において，元の定義では f, f1 , f2 , ..., fn が相互に互健全性の証明は関数の同値性についての議論が必要

換性を持つことを条件としているが，f, f1 , ..., fn がとなるので，関数の外延的同値という公理を用いる．

相互に互換性を持つことは自明ではない．よって以下

これは以下のような公理であり，Coq の標準ライブの補題が必要となる．

ラリで提供されているものを使用した．

補題 4.1. 仮名関数 f, f1 , f2 について，f と f1 ⊕ f2

公理 4.1 (関数の外延的同値). 関数 f, g が任意の入が互換性を持ち，f1 と f2 もまた互換性を持つとき，力に対して等しい結果を返すならば f, g は等しい．

f, f1 , f2 は相互に互換性を持つ．
この補題によって，f, f1 , ..., fn が相互に互換性を持つことが帰納的に保証される．

また，以下の 3 つの補題を証明しておくと，健全性の証明を行いやすい．
補題 4.2 (定義域と値域の一致). ρ; f ⊢ P ならば，

4. 2. 3 Res 規則

in range in domain(f ) が成り立つ．

仮名関数の定義域の制限を行う二項演算子の定義

補題 4.3 (仮名関数の定義域と窓口集合の一致). ρ; f ⊢を変更したことに合わせて，型付け規則 Res は 図 6

P ならば，任意の名前 x について in domain(f, x)のようになる．

であるとき，かつそのときに限り，x ∈ ρ が成り立つ．

4. 2. 4 Inst 規則の分割補 題 4.4 (f un exclusive に お け る 集 合 の 一 致).

Coq による定義では振る舞いの雛形からアクターρ1 ; f1 ⊢ P1 かつ ρ2 ; f2 ⊢ P2 であり ρ1 ∩ ρ2 ̸= ∅を作る配置を二つに分割している．よって型付け規則

ならば，f un exclusive(f1 , f2 ) を満たす．

ρ; f ⊢ P(Res)ρ − {x}; f |x ⊢ (νx)P
図 6: 型付け規則 Res{u}; ch1 (u) ⊢ u(z).P{x}; ch1 (x) ⊢ ((⟨u⟩, ṽ)u(z).P )(⟨x⟩, ỹ){u1 , u2 }; ch2 (u1 , u2 ) ⊢ u1 (z).Px1 ̸= x2{x1 , x2 }; ch2 (x1 , x2 ) ⊢ ((⟨u1 , u2 ⟩, ỹ)u1 (z).P )(⟨x1 , x2 ⟩, ỹ)(Inst-1)(Inst-2)

図 7: 型付け規則 Inst の分割健全性は，以上の公理と補題を利用して，型付け規則の構造に関する帰納法で証明できる．Coq による定義と証明の全文は GitHub リポジトリ [4] に公開している．

5 まとめ
Aπ 計算における型システムの定義を Coq で証明を行いやすいように再定義し，Aπ 計算の型付けの健全性を形式的に証明した．これによって Aπ 計算の型システムが確かにアクターとしての振る舞いを強制することを示した．
今後の課題としては，Aπ 計算における型保存性の証明が上げられる．Aπ 計算の操作的意味論は π 計算と同様にラベル付き遷移 (labeled transition system)を用いており，Aπ 計算における型保存性は Aπ 計算の正しく型がついた配置は遷移を行っても正しく型がつく，というものである．この操作的意味論の Coqでの形式化および型保存性の証明が課題として残っている．
謝辞 本研究の一部は JSPS 科研費 24500033 の助成を受けている．

参 考 文 献[ 1 ] Agha, G.: Actors: A Model of Concurrent Computation in Distributed Systems, MIT Press, 1986.
[ 2 ] Agha, G., Mason, I. A., Smith, S. F., and Talcott, C.: A foundation for actor computation, Journal of Functional Programming, Vol. 7, No. 1(1997),

pp. 1–72.
[ 3 ] Agha, G. and Thati, P.: An Algebraic Theoryof Actors and Its Application to a Simple ObjectBased Language, From Object-Orientation to Formal Methods, Lecture Notes in Computer Science,Vol. 2635, Springer-Verlag, 2004, pp. 26–57.
[ 4 ] A formalization of Aπ-calculus, https://github.com/amutake/a-pi.
[ 5 ] Clinger, W. D.: Foundations of Actor Semantics,
Technical Report AITR-633, AI Lab., MIT, 1981.
[ 6 ] The Coq Proof Assistant, http://coq.inria.
fr/.
[ 7 ] Garnock-Jones, T., Tobin-Hochstadt, S., andFelleisen, M.:
The Network as a Language
Construct, Programming Languages and Systems(ESOP 2014), Lecture Notes in Computer Science,Vol. 8410, Springer-Verlag, 2014, pp. 473–492.
[ 8 ] Gonthier, G.: A computer-checked proof of theFour-Colour Theorem, 2004.
[ 9 ] Milner, R.: Communicating and Mobile Systems: The π-calculus, Cambridge University Press,New York, NY, USA, 1999.
[10] Musser, D. R. and Varela, C. A.: Structured
Reasoning About Actor Systems, Workshop on Programming based on Actors, Agents, and Decentralized Control (AGERE!@SPLASH 2013), ACM, oct2013, pp. 37–48.
[11] Sirjani, M. and Jaghoori, M. M.: Ten Yearsof Analyzing Actors: Rebeca Experience, Formal
Modeling: Actors, Open Systems, Biological Systems, Agha, G., Danvy, O., and Meseguer, J.(eds.),
Lecture Notes in Computer Science, Vol. 7000,Springer-Verlag, 2011, pp. 20–56.
[12] Yonezawa, A., Briot, J.-P., and Shibayama, E.:
Object-Oriented Concurrent Programming in ABCL/1, OOPSLA ’86 Conference Proceedings on
Object-Oriented Programming Systems, Languages
and Applications, 1986, pp. 258–268.