A Proof for Log Matching Property of Raft - 俺の Colimit を越えてゆけ
背景 Log Matching Property の証明 データ構造と述語の定義 AppendEntries 関数の性質 leader の log に関する性質 Log Matching Property の証明 参考資料 背景 分散合意アルゴリズム Raft は kubernetes のクラスターの構成情報を保存する etcd の内部で使われておりお世話になっている方も多いアルゴリズムだと思います。 この記事では Raft の満たす重要な性質である Log Matching Property について証明します。 元々、『Raft を TLA+ で検証する』というタイトルの記事を書こうと考えて Raft の考案者 Diego Ongaro の博士論文を読み始めました（その記事は後日公開予定です）。 アルゴリズムは論文の 3 章に書かれているのですが、そこで Raft が常に成り立つことを
テスト駆動開発から証明駆動開発へ #JTF2019 / July Tech Festa 2019
July Tech Festa 2019 で使用したスライドです。 近年、テストを書く文化は広く普及しており、開発フローにおいて自動テストを組み込むことはもはや常識となりました。しかしよく考えてみると、有限個のテストケースが保証しているのは、所詮「特定の有限個の入力に対する出力」にしか過ぎません。では「あり得る全ての入力」に対してプログラムの性質を保証することは果たして可能でしょうか？ この問いに対する答えのひとつが「定理証明」と呼ばれる手法です。定理証明では、数学的な「証明」をプログラム上でエンコードすることにより、真に「全ての入力」を扱うことができます。本セッションではこの定理証明を取り上げ、従来のテストとの考え方の違いや具体的な適用方法について、サンプルを交えつつ解説します。 イベント概要：https://2019.techfesta.jp/speakers#A10
論理の限量子の使い方が嫌でも分かってしまう話 - 檜山正幸のキマイラ飼育記 (はてなBlog)
論理の限量子 -- つまり全称限量子（記号は'∀'）と存在限量子（記号は'∃'）-- の使い方が分からない、という質問・相談を受けることがあります。なかでも、「∀と∃の順序を交換してイイの？ それともダメなの？」はFAQ〈Frequently Asked Question〉でして、ここ1年でも4回聞かれた気がする。 内容： like関係 like関係の記述・表現 有向グラフ 表〈テーブル〉 碁盤目 他の例も 誰からも好かれる人 好きな人はいますか？ 好きな人は一人だけ 言霊は困るんだけど like関係 論理式の意味や使い方を、日常生活や自然言語の比喩的事例を使って説明するのはヨロシクナイと僕は思っています。しかし、最初のとっかかりに関しては、比喩的事例も致し方ないですね。人間関係の記述を例題にします。 A, B, C, D の4つの要素を持つ集合Xを考えます。 X = {A, B, C,
存在記号の除去規則について考える - 檜山正幸のキマイラ飼育記 (はてなBlog)
「全称記号の導入規則について考える」の続編として、存在記号の除去規則について考えます。 存在記号の除去規則の背景は比較的に簡単な事実です。にも関わらず、記号を換えたり書き方を縦にしたり横にしたりのどうでもいいワチャワチャが事情を見えにくくしています。この記事によって、ワチャワチャな作業（記法のあいだの翻訳）に慣れて、その“どうでもよさ”（記法が変わっても内実は変わらないこと）を感じていただければ幸いです。 内容： 存在記号の除去規則 限量随伴性 引き戻しと存在限量子の随伴性 随伴性を証明に利用する 随伴性からサイド証明へ メタ循環構造 存在記号の除去規則 標準的な自然演繹における「存在記号の除去規則」は次の形に書かれます。 P(a) : : ∃x.P Q -------------[∃除去] Q僕は、自然演繹に愚痴を言い、悪態をついてます（「自然演繹はちっとも自然じゃない -- 圏論による
Coq Winter School 2018
COURSE 2018 From Monday January 22 to Friday January 26, 2018, Yves Bertot will be teaching a course entitled “SOFTWARE VERIFICATION AND COMPUTER PROOF” in the context of the international computer science master at the university of Nice, in Sophia Antipolis. This course is also supported by Université Côte d’Azur PROGRAM 1/ Basic programming with Coq’s functional programming language. Course not
Formal Reasoning About Programs
This is the web site for the early stages of a book introducing both machine-checked proof with the Coq proof assistant and approaches to formal reasoning about program correctness. Grab a Draft Source on GitHub Quasi-latest PDF draft Quasi-latest source-code tarball Quasi-latest source-code tarball, library only (warning: the author really does not recommend using it in serious projects!) Use in
Mathematical Components (the book)
About Mathematical Components is the name of a library of formalized mathematics for the Coq proof assistants. It covers a variety of topics, from the theory of basic data structures (e.g., numbers, lists, finite sets) to more advanced results in various flavors of algebra. This library constitutes the infrastructure for the machine checked proofs of the Four Color Theorem and of the Odd Order The
Reddit - Dive into anything
The Haskell programming language community. Daily news and info about all things Haskell related: practical stuff, theory, types, libraries, jobs, patches, releases, events and conferences and more...
CoqのLtacでmap関数を実装する - 俺の Colimit を越えてゆけ
はじめに length関数を実装する Gallina 風の実装 Ltac から Gallina へ Gallina の項を Ltac 呼び出しの結果として受け取る 気持ち悪い点 map関数(Ltac引数)を実装する map関数(Gallina引数)を実装する 最後に 参考書籍 はじめに Ltac は、Coq において証明の探索を自動化するための Domain Specific Language です。Coq においてプログラムを記述する言語は Gallina と呼ばれていて、これは依存型を持つ普通の関数型言語で意味論も目的も Ltac とは全く別物です。 Gallina で map関数を実装することは Haskell や OCaml で map関数を実装するのとほとんど同じで普通のことです。一方、Ltac は証明の探索の自動化を目的としているので普通の関数型言語と同じようにとはいかないので
Use Coq in Your Browser: The Js Coq Theorem Prover Online IDE!
Welcome to the JsCoq Interactive Online System! Welcome to the JsCoq technology demo! JsCoq is an interactive, web-based environment for the Coq Theorem prover, developed at the Centre de Recherche en Informatique of MINES ParisTech (former École de Mines de Paris). Instructions: JsCoq is open source. If you find any problem or want to make any contribution, you are extremely welcome! We await you
Globularの威力をお見せしよう - 檜山正幸のキマイラ飼育記 (はてなBlog)
Globularはとっつきにくいソフトウェアなので、使い方を伝えるには、最初から順番に説明する必要があるでしょう。しかし、タクサンの画面キャプチャを撮ってマウス操作の説明を付けていく気力は湧きません（大変過ぎる！）。とりあえず、Globularのデモンストレーションとして、“それなりの内容の定理”を証明したサンプルをお見せします。誰でもアクセス可能なので体験して悟ってください(苦笑)。 http://globular.science/1601.004v2 （Chrome推奨） 「証明の過程を追体験する」の節だけは、頑張って手取り足取りな解説を書いたので、そのとおりに操作してみると雰囲気が伝わるでしょう。 このサンプルの内容はというと： 「絵算の威力をお見せしよう」において、ラルフ・ヒンズ（Ralf Hinze）の論文にある命題を2つ選んで絵に描きました。選んだ2つの命題は、論文の入り口にあ
絵算ベースの証明支援系 Globular - 檜山正幸のキマイラ飼育記 (はてなBlog)
絵算ベースの証明支援系であるGlobularがWebサービスとして公開されています。 http://globular.science/ ブラウザー（Chrome推奨）上で動くJavaScriptプログラムが証明支援系の実体です。 証明支援系とは言っても、CoqやAgdaなどとはだいぶ趣が異なります。100%グラフィカルで、テキストによる表現や命令は一切使いません。パッと見ただけでは、何をするものか見当が付かないのではないでしょうか。 このソフトウェアを開発したのは、アブラムスキーとクック（この記事に二人の写真あり）が率いるオックスフォードのQuantum Groupで、開発の中心人物はジェイミー・ヴィカリー（Jamie Vicary）です。 Quantum Groupは、数年前から同種のソフトウェア（diagrammatic proof assistant）としてQuantomaticも提
The Lean Theorem Prover
The Lean Theorem Prover Leonardo de Moura (Microsoft Research), Soonho Kong (CMU), Jeremy Avigad (CMU), Floris van Doorn (CMU), Jakob von Raumer (KIT), Rob Lewis (CMU), Haitao Zhang, Daniel Selsam (Stanford) CICM, 2015/07/09 http://leanprover.github.io Many thanks to Cody Roux Georges Gonthier Grant Passmore Nikhil Swamy Assia Mahboubi Bas Spitters Steve Awodey Ulrik Buchholtz Tom Ball Parikshit K
リフレクションのしくみをつくる - Qiita
2015/08/11 2015/08/16 2015/09/12 「スモール SSReflect の製作」から改題 @suharahiromichi はじめに 命題(Prop型)をbool型の式に変換すること（とその逆）をリフレクションと呼びます。 例： x = y と x == y 命題をbool型の計算に変換することで、命題の証明が簡単になる場合があります。そのリフレクションを「狭い範囲」で行い、証明の効率化を図るのが、CoqのSmall Scale Reflection (SSReflect) 拡張です。 今回は、SSReflectのしくみを理解することを目的に、Starndard Coqで「SSReflectもどき」を作り、Leibniz同値関係とbool値等式のリフレクションができるまでを示します。 それを通して、Coqのコアーション(coersion)や、カノニカル・ストラクチ
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
TechCrunch | Startup and Technology News
Verified Functional Algorithms
Agda による型推論器の定式化
bitbucketの使い方
Amazon.co.jp: Type Theory and Formal Proof: An Introduction (English Edition): Nederpelt, Rob, Geuvers, Herman: Digital Ebook Purchas
Preuves de programmes en coq - Yves Bertot INRIA