IsabelleによるCBC CasperのSafetyの証明をしました
日記です。 リポジトリ: LayerXcom/cbc-casper-proof 概要 (私は LayerX の人ではないですが)LayerX 社の人と色々あって CBC Casper というブロックチェーンのプロトコルの検証作業を行いました。(主に定理証明士としてのお手伝い) 半年くらいかかったけどやりたかった証明についにたどり着いたよという話。 CBC Casper って何 わからん。(無知) 何かブロックチェーンのプロトコルの名前らしい。Ethereum 財団が目をつけてるらしい。いわゆるビットコインとは違ってブロックを頑張ってマシンをぶん回してマイニングしたりしないらしい(ビットコインは PoW で CBC Casper は PoS)。 詳しいことは詳しい人に聞いたほうがいいよ(真理)。 cf: CBC Casper と形式的検証 Isabelle で検証って何するの ブロックチェー
(解説) はてなブックマークにおけるアクセス制御 - 半環構造に基づくモデル化 - Hatena Developer Blog
こんにちは、シニアアプリケーションエンジニアのid:taraoです。この記事ははてなデベロッパーアドベントカレンダー2015の10日目です。昨日はid:tapir320によるはてなの組織開発についてでした。 先月開催されたWebDB Forum 2015で、「はてなブックマークにおけるアクセス制御: 半環構造に基づくモデル化」というタイトルの発表をしました。 はてなブックマークにおけるアクセス制御 - 半環構造に基づくモデル化 from Lintaro Ina 発表資料には多くの方に興味をもっていただけたようですが、わかりにくい点も多かったのではないでしょうか。スポンサー企業としての技術報告セッションとはいえ学術会議での発表なので理論面と独自の工夫点にフォーカスした内容であったり、口頭での発表のしかたに大きく依存したスライドの遷移方法になっているので、この資料だけで細かいところまで理解しよ
Research papers - HaskellWiki
A lot of documentation exists about Haskell, and its foundations, in the form of research papers written by those investigating language design. An enormous research effort, by hundreds of researchers over the past 20 years, has gone into making Haskell such a great language. In general, if a feature is not well understood, it isn't going to become part of the language. Here is a selection of thos
なぜ関数プログラミングは重要か
John Hughes, Institutionen för Datavetenskap, Chalmers Tekniska Högskola, 41296 Göteborg, SWEDEN. rjmh@cs.chalmers.se この日本語訳は原著者の承諾を得て山下がここに公開するものです。 この訳文についての、御指摘などは山下伸夫(nobsun .at. sampou.org)までおねがい いたします。 翻訳最終更新日 : 2011-09-17 原文 "Why Functional Programming Matters" 日本語訳PostScript この論文は1984年以来何年ものあいだChalmers大学のメモとして回覧された。 1989年と1990年に幾分か改訂をしたのが[Hug89]と [Hug90]である。この版はもとのChalmer大学のメモ のnroff原稿をもとに
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Simon Peyton-Jones - Microsoft Research
