Alternative names
Important note: if you had never heard of Coq before reading the article on theregister.com, then your opinion on this matter is probably not relevant to us. Please consider staying out of this process, thank you very much! The name Coq comes from the French word for rooster, CoC (the Calculus of Constructions) and Thierry Coquand, one of the initial authors of Coq. But it is also close to the wor
ML のサブセットの型推論器を Coq で検証する - fetburner.core
この記事は言語実装 Advent Calendar 2020 の5日目の記事です． 一度でも型推論器を書いたことがあれば，そのあまりの邪悪さ，あるいはその複雑さに恐れ慄いたことでしょう． 参照を用いて単一化を実現しようものなら構文木は参照に汚染され，純粋関数型に実装しようものなら大量の型代入をどのような順序で適用したものか悩まされる． これは Hindley-Milner 型推論器を実装する上での宿命のようなものです． 本記事では，MLのサブセット——型付きλ計算をletと参照で拡張した，let多相をサポートする言語——の型推論器を Coq で実装し，その正当性を証明します． Coq で検証を行うことで我々は型推論器のバグへの恐怖とデバッグの労力から真に解放され，枕を高くして眠ることができることでしょう． もっとも、型付きλ計算を let 多相で拡張した言語の型推論器の正当性は実はすでに証
クイックソートは半順序でもソート可能であることをCoq/SSReflectで証明する - Qiita
はじめに 前回の記事で、全順序が仮定されているからこそうまくいくソートアルゴリズムを半順序で使用するとどうなるかを見ました。結果としてクイックソートなら半順序でもうまくソートできることを見ましたが、本記事では、これを定理証明支援系Coqを用いて、形式的に証明していきます。 定理証明支援系Coqに関して軽く説明しておくと、プログラムが正しく動くことを、数学的に検証できるツールとして使えるものです。 クイックソートを定義 SSReflectのpathライブラリには、標準のソート関数sortが定義されていますが、このアルゴリズムはマージソートなので、前回の記事で検証したように半順序では使えません。 そこでCoqでクイックソートを定義します。 まず定義の前に、ソートを行う要素の集合Tと、半順序関係Rを宣言しておきます。実際にはTは型で、RはただのT上の二項関係T -> T -> boolとして定義
ニコニコをCoqで証明してみた / Yosh さん - ニコナレ
2018年09月02日 10:042,24106ニコニコをCoqで証明してみた▲説明文を閉じるスライド制作者Yoshさんブログに貼り付け以下をコピーしてブログに貼り付けてくださいアカウントをお持ちの方ログインアカウントをお持ちでない方新規アカウント作成Now loading...エンコードが完了しました リロードしてください - / -コメントするコメント投稿するためにはログインしてくださいコメントリストページ一覧コメントページ123456789101112131415161718192021222324関連ナレッジニコニコ動画はなぜオワコン化しているのか ～…シリウスＹ さんねるねるねるねを練ったわけrerofumi さんデータでみるニコニコ動画の現状 -2018年5月myrmecoleon さん急上昇ナレッジninaさんの「【練習用】自分の声が、どんな声か…nina さんドワンゴプログ
Coqで学ぶ証明プログラミング！ テストだけでなく「証明」で安全性を保証する - エンジニアHub｜Webエンジニアのキャリアを考える！
Coqで学ぶ証明プログラミング！ テストだけでなく「証明」で安全性を保証する プログラミング言語「Coq」では、プログラムを「証明」して間違いを防ぐことができます。プログラムの正しさを保証できる一歩進んだエンジニアになりましょう！ coqtokyoを主催する今井宜洋さんの解説です。 みなさん、Coqってご存知ですか？ プログラムを証明して間違いを防ぐという優れものです。今回はそのCoqについて、coqtokyoという勉強会を主催している今井宜洋がお届けします。 プログラムをただ作るだけではなく、その正しさを保証できる一歩進んだエンジニアになってみましょう！ Coqって何？ プログラムを「証明する」ってどういうこと？ Coqを使ってみよう Coqのインストール方法 CoqIDE：Coqによる証明開発のフロントエンド Coqで関数プログラミング プログラムの仕様を記述しよう 証明開発モード ゴ
ML Day #1 - connpass
ML Day (ML勉強会） SML、OCaml、F#、Coq、IsabelleなどのML?だと思われる言語の勉強会です。 あなたがMLだと思ったものがMLです。 プログラミング言語の基礎理論から応用プログラミング、入門してみたなど 様々な発表を歓迎します！！！ また、最近関数型言語に関する勉強会があまり見られないので、MLの人に通じそうなネタ（Haskell、定理証明、それっぽい数学）等に関する発表も歓迎します！！！ 注意 運営側で発表の難易度は調整しないので分からないこともあるかもしれないと思って来て下さい ML=Meta LanguageですMailing ListでもMachine Learningでもないです 発表者募集 発表者を先着で募集中です。 発表枠に登録した方を順次管理者に登録するので、発表タイトル編集は各自で行ってください。発表者になってタイトルも決まったのに、しばらく
定理証明支援の紹介 - Qiita
目的 定理証明支援とは何かと現状の整理。 定理証明支援とは 定理証明支援とは数学の定理を自動で証明することではなく、ステップバイステップでコンピュータに命令を送り、数学の定理を証明するのを助けるシステムである。 支援だから意味ないということでなく、最近の数学の証明は長くなり証明の検証が難しいのを助ける意味がある。定理証明支援の意義についてはこちらが詳しい。 また、信頼性が求めらる難しいアルゴリズムの検証、たとえばTLS(暗号通信)やRaft(分散合意アルゴリズム)のサーバーに利用されつつある。 ここでいう定理は大げさなものだけでなく、$1+1=2$、$0何か=0$、$ab=b*a$といった簡単なものを証明しながらどんどん積み上げていく。通常のプログラムと違うのは証明であるので使用する変数が整数ならそのすべての値について成り立つ定理を証明する。 定理を証明するのに使うツールは下記である。(他
GitHub - pirapira/coq2rust: Coq to Rust program extraction. The whole tree is on the original Coq code base.
enum Empty_set<> { } enum Unit<> { Tt } enum Bool<> { True, False } fn xorb(b1: Bool, b2: Bool) -> Bool { match b1 { Bool::True => (match b2 { Bool::True => Bool::False, Bool::False => Bool::True }), Bool::False => b2 } } enum Nat<> { O, S(Box<Nat>) } enum Prod< a, b> { Pair(Box<a>, Box<b>) } fn fst<p,a2>(p: Prod<p,a2>) -> p { match p { Prod::Pair(box x,box y) => x } } enum List< a> { Nil, Cons(Bo
Coqで独習するならどのページがいい？と聞かれたときのメモ - 簡潔なQ
Download Coq(英語) ダウンロードしなければ何も始まらない。 Download | The Coq Proof Assistant ちなみにLinuxディストリならcoqideパッケージをインストールするのが吉 Coqの入門記事を書く会 そこそこ体系的な入門サイト 2010-09-02 - ひとり勉強会 2010-09-14 - ひとり勉強会 2010-09-19 - ひとり勉強会 2010-10-12 - ひとり勉強会 Coq 99 練習問題。直観主義論理における有名な証明を一通り解ける。 Functional Programming Memo: [Coq] Coq-99 : Part 1 anarchy proof 練習用サイト。途中から一気に難化するのが問題。 わからなかったら他の人の解答も見られる anarchy proof - Curry-Howard Isomorp
Certified Programming with Dependent Types
This is the web site for a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation. I'm following an unusual philosophy in this book, so it may be of interest even to long-time Coq users. At the same time, I hope that it provides an easier introduction for newcomers, since s
CCS Injection脆弱性(CVE-2014-0224)発見の経緯についての紹介 - OpenSSL #ccsinjection Vulnerability
菊池です。CCS Injection脆弱性(CVE-2014-0224)発見の経緯について紹介します。 バグの簡単な解説 OpenSSLがハンドシェーク中に不適切な状態でChangeCipherSpecを受理してしまうのが今回のバグです。 このバグはOpenSSLの最初のリリースから存在していました。 通常のハンドシェークでは、右の図のような順序でメッセージを交換します(RFC5246 The Transport Layer Security (TLS) Protocol Version 1.2 §7.3より作成)。 ChangeCipherSpecは必ずこの位置で行うことになっています。OpenSSLもChangeCipherSpecをこのタイミングで送信しますが、受信は他のタイミングでも行うようになっていました。これを悪用することで、攻撃者が通信を解読・改ざん可能です。 発見の困難さ
Idris: A Language for Type-Driven Development
Idris: A Language for Type-Driven Development Idris is a programming language designed to encourage Type-Driven Development. In type-driven development, types are tools for constructing programs. We treat the type as the plan for a program, and use the compiler and type checker as our assistant, guiding us to a complete program that satisfies the type. The more expressive the type is that we give
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
GitHub - WasmCert/WasmCert-Coq: A mechanisation of Wasm in Rocq
リストのconsの型をA -> list A -> list AではなくA -> list (list A) -> list Aにした型をHaskellとCoq/SSReflectで定義したい - Qiita
GitHub - Huxpro/WasmCert: A (in-development) Coq mechanization of WebAssembly specification.
GitHub - cpitclaudel/company-coq: A Coq IDE build on top of Proof General's Coq mode
GitHub - sweirich/corespec: A Specification for Dependent Types in Haskell (Core)
GitHub - CoqHott/DICoq: Dependent Interoperability for Coq
GitHub - ekmett/comonad-extras: Comonad transformers that require Haskell extensions
GitHub - ekmett/comonad-transformers: Haskell 98 comonad transformers - as of 4.0 these have merged into the comonad package.
