IsabelleによるCBC CasperのSafetyの証明をしました
日記です。 リポジトリ: LayerXcom/cbc-casper-proof 概要 (私は LayerX の人ではないですが)LayerX 社の人と色々あって CBC Casper というブロックチェーンのプロトコルの検証作業を行いました。(主に定理証明士としてのお手伝い) 半年くらいかかったけどやりたかった証明についにたどり着いたよという話。 CBC Casper って何 わからん。(無知) 何かブロックチェーンのプロトコルの名前らしい。Ethereum 財団が目をつけてるらしい。いわゆるビットコインとは違ってブロックを頑張ってマシンをぶん回してマイニングしたりしないらしい(ビットコインは PoW で CBC Casper は PoS)。 詳しいことは詳しい人に聞いたほうがいいよ(真理)。 cf: CBC Casper と形式的検証 Isabelle で検証って何するの ブロックチェー
Haskellで解くAtCoder
最近HaskellでAtCoderの問題を解いたりしているのでごく基本的な知見をまとめておく。 テクニック集 多くは割と色んな人がすでに言っていることではある。また、想定解法を正しく実装すれば以下のようなことを守らなくても時間内に収まるだろうが、GHCは最適化が効かなければ10倍遅くなる言語であるので普段から守っておくに越したことはないと思う。 環境: AtCoderのGHCは2019.04現在7.10なので注意が必要。そのうち上がるかもしれないけど。 Strict拡張がない BangPatterns拡張はある 環境構築がhaskell-platformらしいのでそれに入ってるライブラリしか使えない 文字列 基本はData.ByteString.Chan8 Stringは死んでも使わない(遅いので) Unicode文字列の扱いが必要(今の所みたことないけど)とかならtextを使うといいかも
定理証明リンク集
定理証明、特に定理証明支援系(Proof Assistant)はその存在こそ少しずつ浸透しつつあるような気がしないでもないけれど資料とか全然まとまってないのが不便だなと前々から思っていたのでリソースをまとめておきます。 これも追加してほしいみたいなのあったら教えてください。 Proof Assistants 始めるなら次の中から選ぶのがよいと思います。 Coq Calculus of constructionsベースの型システムとリッチなコマンドを備えた言語 このリストの中では最もコミュニティが大きい、入門書等も豊富 型システムと項を書くためのGallina, コンパイラへの命令を記述するためのVernacular, タクティクスの定義に使うLtacなどの言語が混ざって出てくるのが初心者には混乱必至 結構複雑な言語なので使いこなすのはそれなりに大変 Agda Martin-Löf type
一人CSアドベントカレンダー開催のお知らせ
これは一人Computer Scienceアドベントカレンダー 1日目の記事です。 概要的なもの 「一人アドベントカレンダーって面白そうだな、やってみたい」みたいなノリで登録したんですが、 25日毎日記事を同じテーマで投稿し続けるのどう考えてもめっちゃ大変なのでやはりここは自分が一番得意な分野で行くしかないかなとなりCS関係ということになりました。 上のQiitaのページでも書いてますが、キーワードとして"ラムダ計算・定理証明・Haskell・ML・圏論 とかなんかそのへん"を挙げていますので そのへんのお話になります。今のところは無難に定理証明を中心にテーマをいくつか選んでおいたので多分そのへんの話です。 スケジュール 最終的にはQiitaのカレンダー見ればわかることなんでいいんですが一応今後どういう感じで進めていくのかのスケジュール的なものをまとめておきます。 Isabelle編 Is
私と型システムとポエム
最近巷では俄に型システムについての言及が増え、型システムポエマーが増えてる気がするので自分もその時流に乗りたい。 完全にポエムだけどなんかあったら随時指摘ください。直します。 TL;DR 言いたいことはまとめると次 型システムは程度問題なのでちょうどいいところを探すべき 型は万能でも強さが正義でもない(だから未だに研究されてる) よく知りもしないくせに計算機科学を侮辱するのはやめろ 予防線 あくまでポエムですので中身はないです 私は型理論専攻で学位はとったものの研究者ではないのであまり信用しすぎないように 型システムの過去 型システムは大まかに次のような利点があるとされてきた(個人的主観) 「異常」なプログラムを検出する仕組み 静的解析による分かりやすいエラーメッセージ 型そのもののドキュメント性 IDEでのcompletionに貢献 最適化に貢献 (数学に正しく裏打ちされたsemanti
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
