並行分離論理

logic

RustBeltはIrisという高階並行分離論理のフレームワークの上でLifetime logicという専用の論理を定義している。
Lifetime LogicではRustのMIRを模した言語でプログラムを書くことができる。このプログラムに対して並行性まわりのミスがないことを証明する。
Iris自体はCoq+ssreflectの上で動く。

— Masaki Hara (@qnighy) June 26, 2018

参考文献