タグ検索の該当結果が少ないため、タイトル検索結果を表示しています。
はじめに 前回の記事で、全順序が仮定されているからこそうまくいくソートアルゴリズムを半順序で使用するとどうなるかを見ました。結果としてクイックソートなら半順序でもうまくソートできることを見ましたが、本記事では、これを定理証明支援系Coqを用いて、形式的に証明していきます。 定理証明支援系Coqに関して軽く説明しておくと、プログラムが正しく動くことを、数学的に検証できるツールとして使えるものです。 クイックソートを定義 SSReflectのpathライブラリには、標準のソート関数sortが定義されていますが、このアルゴリズムはマージソートなので、前回の記事で検証したように半順序では使えません。 そこでCoqでクイックソートを定義します。 まず定義の前に、ソートを行う要素の集合Tと、半順序関係Rを宣言しておきます。実際にはTは型で、RはただのT上の二項関係T -> T -> boolとして定義
この記事は言語実装 Advent Calendar 2020 の5日目の記事です． 一度でも型推論器を書いたことがあれば，そのあまりの邪悪さ，あるいはその複雑さに恐れ慄いたことでしょう． 参照を用いて単一化を実現しようものなら構文木は参照に汚染され，純粋関数型に実装しようものなら大量の型代入をどのような順序で適用したものか悩まされる． これは Hindley-Milner 型推論器を実装する上での宿命のようなものです． 本記事では，MLのサブセット——型付きλ計算をletと参照で拡張した，let多相をサポートする言語——の型推論器を Coq で実装し，その正当性を証明します． Coq で検証を行うことで我々は型推論器のバグへの恐怖とデバッグの労力から真に解放され，枕を高くして眠ることができることでしょう． もっとも、型付きλ計算を let 多相で拡張した言語の型推論器の正当性は実はすでに証
はじめにCoqで解析入門の1章にある命題を全て証明してみたので記事を書いてみます。 Coqでの証明大学で記号論理学の授業を受けたことはありますか？記号論理学では数学の命題を証明木を用いて形式的証明をしていましたがCoqでも形式的証明をします。流れは以下です。 数学の命題を論理記号で書きますゴールが表示されるので適切にCoqのTacticを使いますするとゴールが変わるので未証明のゴールがなくなるまで繰り返しTacticを使います Coqでの証明の魅力は 証明が正しいことをCoqが保証してくれること(Coqにバグがあるかもしれませんが多分)証明した定理が他の定理の証明に使えて楽しいところ などです。 やろうと思った背景大学1年生の頃、解析入門を前から読んで途中で理解できなくなって読み直すというのを繰り返していました。 いつか理解したいなと思っていたときに記号論理学の授業を受けて解析入門の証明も
2019年7月29日、Opt Technologiesが主催するイベント「Fun Fun Functional (2) 関数型言語Lightning Talks!!」が開催されました。関数型プログラミングについて楽しく学び、知見を共有することを目的に開催されている本勉強会。今回は6名のエンジニアが、関数型プログラミング言語にまつわるユニークな発表を行いました。プレゼンテーション「OCamlとCoqでブロックチェーンプログラミング 」に登壇したのは、yoshihiro503氏。 OCamlとCoqでブロックチェーンプログラミング yoshihiro503氏（以下、yoshihiro503）：みなさんこんにちは。こういう鶏のアイコンのyoshihiro503です。今日「OCamlは良いぞ！」という話をします。株式会社ドワンゴのDMC開発部に所属しています。 簡単に自己紹介を
楊井人文 Yanai Hitofumi on Twitter: "【要検証】この毎日新聞の記事はその多くを前川喜平氏の証言を疑問視することなく依拠しているようですが、法律、事実面から疑問がいくつもあります。 1)前川氏が1997年に名称変更申請を受理しなかったと証言するが、かかる「不受理」は行政… https://t.co/2coQ8W5kCN"
【要検証】この毎日新聞の記事はその多くを前川喜平氏の証言を疑問視することなく依拠しているようですが、法律、事実面から疑問がいくつもあります。 1)前川氏が1997年に名称変更申請を受理しなかったと証言するが、かかる「不受理」は行政… https://t.co/2coQ8W5kCN
先週の土日にこのオンラインセミナーに参加してみた。 定理証明支援系 Coq チュートリアル - connpass 定理証明は、名前は聞くけど触ったことはなくて、興味はあるけど本を買うほどのモチベーションはないし、誰か詳しい人が要点だけ教えてくれたりしないかな〜。と思っていたところ、まさにぴったりのイベントが。なんていうか、昔ならこういうのは東京まで行かないと参加できなかった気がするけど、家からオンラインで参加できるようになったのは嬉しいね。 日程は5時間 x 2日という長丁場で、説明だけでなく練習問題もあるのでとっても疲れた！でもこういうのって自分で手を動かさないと「わかったような気になった」だけで終わりがちだから、演習があるのはとてもありがたい。 Coqの感想 これまでいろんなプログラミング言語を触ってきたけど、証明とプログラムが一体になった環境は新鮮で面白かった。「整数」「文字列」みた
GitHub - ms-jpq/coq_nvim: Fast as FUCK nvim completion. SQLite, concurrent scheduler, hundreds of hours of optimization.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session. Dismiss alert
最近、定理証明支援のCoqを入門している。というのは、以前の職場にいたときの職場でもCoqをやっている先輩がいて、今回の職場でも定理証明支援系を使っている同僚がいて、しかも最近自分はプログラミング言語実装をやっているためか、Coqや依存型について聞かれることがあるので、一念発起して取り組み始めた。 しかし、案の定、何から始めたらいいのかわからず入門に躓いてしまい、かなり難しいと感じた。しかも一番最初に読み始めた本が、Certified Programming with Dependent Typeという初心者向けではない本だったため、事態は混迷を極めていた。 そんな難関を乗り越えて2ヶ月、ようやく基本的な証明をできるまでたどり着いたので、メモ代わりにどう入門すればよいか残しておこうと思う。 1. 関数型のプログラミング言語を学ぶ 自分は関数型プログラミング言語の処理系を設計・実装したことが
Gopiandcode > logs > Bloom filters debunked: Dispelling 30 Years of bad math with Coq!
There's this rather nifty feature of modern web browsers (such as Firefox or Chrome) where the browser will automatically warn the user if they happen to navigate to a "malicious" URL: While conceptually simple, this feature actually requires more engineering effort than one would expect - in particular, tracking the set of known malicious URLs in a practical manner turns out to be somewhat diffic
ArtSalt on Twitter: "【急募】｢安倍総理のいいところがわかるエピソード｣ランサーズが募集。800文字以上250円の高収入案件、急げ https://t.co/PdgyyDbN2S https://t.co/uY0cOq1Rsy"
【急募】｢安倍総理のいいところがわかるエピソード｣ランサーズが募集。800文字以上250円の高収入案件、急げ https://t.co/PdgyyDbN2S https://t.co/uY0cOq1Rsy
今年はそれらしきアドベントカレンダーが無いので，この記事は ML アドベントカレンダー 2020 の4日目の記事と言い張ってみます． ML って本を正せば定理証明支援系由来ですし．最後にちょっと OCaml を使ってますし． Coq によって検証された正規表現エンジンは既に存在していて，探せば他にもいくつもあると思うのですが， それらの実装は主として検証の簡単さに重きが置かれており，OCaml のコードを extract して使ってみると実用に堪えないものが多いように思います． 本記事では，以前 OCaml で書いた効率的な実装を Coq に移植して検証します． 加えて，extract によって OCaml のコードを再び生成し， AtCoder の問題に投げてみても TLE にならないことを確認します． 本記事で実装する正規表現エンジンと，その正当性の証明は GitHub に存在します．
はじめに CoqをDocker上にインストールしたのでその手順をまとめます。 CoqのコードはOCamlに変換できるので、変換したコードをOCamlから呼び出してみます。 Dockerのインストールは済んでいる前提で進めていきます。 OPAMのインストール OCaml、CoqをインストールするためにまずOPAMをインストールします。 OPAMはOCamlのパッケージマネージャです。 OPAMをインストールするとOCamlは自動的に入りますが古いバージョンなので新しいバージョンを別にインストールします。 Alpine Linuxのコンテナを起動します。
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session. Dismiss alert
GitHub - jldodds/coq-lean-cheatsheet: A quick reference for mapping Coq tactics to Lean tactics
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session. Dismiss alert
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
クイックソートは半順序でもソート可能であることをCoq/SSReflectで証明する - Qiita
ML のサブセットの型推論器を Coq で検証する - fetburner.core
Coq/SSReflect/MathCompで解析入門の1章の命題を全て証明
OCamlとCoqでブロックチェーンプログラミング
『定理証明支援系 Coq チュートリアル』に参加した - yhara.jp
天下一品のスニーカー「le coq sportif」から爆誕
Coqに入門した感想 - 未完成な論を綴るブログ
効率的な正規表現エンジンを Coq で検証する - fetburner.core
Docker上にOCaml+Coqの環境を構築して動かしてみるまで - Qiita
GitHub - jonsterling/coq-domains
note.com/higashino_atsuko
diamond.jp
tomowo.hatenablog.jp
diamond.jp
news.yahoo.co.jp
kuromaron.hatenablog.com