SUHARA Hiromichi さんが書き込みました。

2018/01/19 20:04

keigoi さん了解しました。morita さんがとてもよろこぶと思います。

keigoi さんが書き込みました。

2018/01/19 14:37

時間があれば Verifast についても紹介させてください。 Hoare logic + separation logic で C言語の検証ができるのが良いです。Coq が使える方なら使えるのではないかと思います。

SUHARA Hiromichi さんが書き込みました。

2018/01/14 22:42

型付ラムダ計算ならPLFのSmallstepから、Hoare論理ならLFのImpからになりそうですが、今回（第72回）は導入とすすめかたの相談からしたいと思います。 #ProofCafe

SUHARA Hiromichi さんが書き込みました。

2018/01/14 22:36

Software Foundations は英語の最新版を使いたいとおもいます。日本語版は古すぎて実行できないです。 https://softwarefoundations.cis.upenn.edu/ #ProofCafe

SUHARA Hiromichi さんが書き込みました。

2018/01/02 12:37

ホーア論理の資料をアップしました。 #ProofCafe

SUHARA Hiromichi さんが書き込みました。

2018/01/02 12:36

ホーア論理の資料をアップしました。

SUHARA Hiromichi さんが書き込みました。

2017/12/31 18:07

suharahiromichi さんが 第72回 ProofCafe を公開しました。