IsabelleによるCBC CasperのSafetyの証明をしました
日記です。 リポジトリ: LayerXcom/cbc-casper-proof 概要 (私は LayerX の人ではないですが)LayerX 社の人と色々あって CBC Casper というブロックチェーンのプロトコルの検証作業を行いました。(主に定理証明士としてのお手伝い) 半年くらいかかったけどやりたかった証明についにたどり着いたよという話。 CBC Casper って何 わからん。(無知) 何かブロックチェーンのプロトコルの名前らしい。Ethereum 財団が目をつけてるらしい。いわゆるビットコインとは違ってブロックを頑張ってマシンをぶん回してマイニングしたりしないらしい(ビットコインは PoW で CBC Casper は PoS)。 詳しいことは詳しい人に聞いたほうがいいよ(真理)。 cf: CBC Casper と形式的検証 Isabelle で検証って何するの ブロックチェー
Post correspondence problem - Wikipedia
Not to be confused with the other Post's problem on the existence of incomparable r.e. Turing degrees. The Post correspondence problem is an undecidable decision problem that was introduced by Emil Post in 1946.[1] Because it is simpler than the halting problem and the Entscheidungsproblem it is often used in proofs of undecidability. Definition of the problem[edit] Let be an alphabet with at leas
Write Yourself a Theorem Prover in 48 Hours (その1) - Qiita
ソフトウェア科学特論: 命題論理
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Criterion -- from Wolfram MathWorld
