型システムの正しさ
no immediate deadlock(output の義務のケース)
? + x:[?]/Oo├ P のときに、P が簡約できなければ、
P は実際に x への output を実行している
subject reduction
プロセスを簡約しても、同様の型付けを維持できる
?
deadlock-freedom(output の義務のケース)
? + x:[?]/Oo├ P のときに、P を簡約していけば、
P は実際に x への output を実行する
前のスライド
次のスライド
最初のスライドに戻る
グラフィックスの表示