GitHub - formal-land/coq-of-rust: Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦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
🦀 Translation of the Rust's core and alloc crates | Formal Land
We continue our work on formal verification of Rust programs with our tool coq-of-rust, to translate Rust code to the formal proof system Coq. One of the limitation we had was the handling of primitive constructs from the standard library of Rust, like Option::unwrap_or_default or all other primitive functions. For each of these functions, we had to make a Coq definition to represent its behavior.
Coqによる 証明駆動開発 超入門
証明駆動開発 とは 証明駆動開発 とは証明によってプログラムが期待通りの性質を有しているかを確かめながら開発する手法のこと。 ユニットテストの一部で使用可能な方法。 証明駆動開発 での流れは参考サイトに記載されているように以下の流れで行う。 1.対象プログラムが持つべき性質を洗い出す 2.Coqでプログラムを書く 3.書いたプログラムの性質を証明する 4.他の言語のコードに出力する 参考サイトに証明の仕方については記述されているため、このページでは 証明駆動開発 にのみ焦点を当てる。 参考になるサイト coqによる 証明駆動開発 とcoqideの使い方： http://d.hatena.ne.jp/zyxwv/20090922/1253643926coqtopの使い方： http://www.iij-ii.co.jp/lab/techdoc/coqt/coqtop-vimの使い方： htt
よく使う Coq.Logic の公理 - 簡潔なQ
Coq.Logic にはCoqの集合論モデルにおいて正しい公理や、それらの間の関係が記述されている。 ここではその一部を取り上げて、意味を説明する。 前提知識 公理を仮定しない状態では、 Coqの論理は直観主義論理である。 ある2つが「等しい」という命題が証明できる場合は限定される。 証明の文脈(Prop)における「AまたはB」と、値の文脈(Set/Type)における「AまたはB」は区別される。前者から情報を取り出すことはできないようになっている(マッチングの型検査で弾かれる。) 以下、公理の説明 古典論理 (classical logic) 場所: Coq.Logic.Classical 古典論理で証明できることは、例えば以下の内容がある。 排中律 ( P or not P ) 二重否定除去および背理法 ( if not not P, then P ) 決定性の値の取り出し (descr
Coq/SSReflect/MathCompで解析入門の1章の命題を全て証明
はじめにCoqで解析入門の1章にある命題を全て証明してみたので記事を書いてみます。 Coqでの証明大学で記号論理学の授業を受けたことはありますか？記号論理学では数学の命題を証明木を用いて形式的証明をしていましたがCoqでも形式的証明をします。流れは以下です。 数学の命題を論理記号で書きますゴールが表示されるので適切にCoqのTacticを使いますするとゴールが変わるので未証明のゴールがなくなるまで繰り返しTacticを使います Coqでの証明の魅力は 証明が正しいことをCoqが保証してくれること(Coqにバグがあるかもしれませんが多分)証明した定理が他の定理の証明に使えて楽しいところ などです。 やろうと思った背景大学1年生の頃、解析入門を前から読んで途中で理解できなくなって読み直すというのを繰り返していました。 いつか理解したいなと思っていたときに記号論理学の授業を受けて解析入門の証明も
最小共通祖先を求めるアルゴリズムの形式検証 | Wantedly Engineer Blog
競技プログラミングには概念を知っておかないと解きようがない、いわゆる覚えゲーのような問題が存在します。典型的な例が 10^9+7 といった素数で割った余りを求めろといったもので、普段業務で日常的に素数で割った余りを求めている人でもなければ、割り算がしたければフェルマーの小定理や拡張ユークリッドの互除法を使えば良いと直ぐには思い付けないのではないでしょうか。 最小共通祖先も覚えゲーで必要な概念の一種と言えます。これは読んで字のごとく、与えられた根付き木の下で2頂点に共通する祖先のうち、最も根から遠い頂点を指す概念で、例えば木の2頂点が与えられて、頂点間の経路について何かを求めろといった問題で威力を発揮することが多いです。これを用いて解ける例を挙げるとすると次の問題でしょうか。 https://atcoder.jp/contests/abc014/tasks/abc014_4 最小共通祖先を求
let多相を扱える型推論器をCoqで検証する - fetburner.core
以前から僕は単相の型推論アルゴリズムの健全性や完全性をCoqで検証していたのですが，最近*1let多相をサポートするように型推論器の実装と正当性の証明を修正したので記事にしておきましょう*2． 単相型と多相型 以前Coqで検証した型推論アルゴリズムは単相，つまり多相型の扱えないものでした．説明のためにOCamlのREPLのようなものがあると仮定すると，以前の型推論器はこのような動作をすることでしょう． # let s x y z = (x z) (y z);; (* Sコンビネータ *) val s : ('_a -> '_b -> '_c) -> ('_a -> '_b) -> '_a -> '_c = <fun> # let k x y = x;; (* Kコンビネータ *) val k : '_d -> '_e -> '_d = <fun> # s k;; - : ('_a -> '
ML のサブセットの型推論器を Coq で検証する - fetburner.core
この記事は言語実装 Advent Calendar 2020 の5日目の記事です． 一度でも型推論器を書いたことがあれば，そのあまりの邪悪さ，あるいはその複雑さに恐れ慄いたことでしょう． 参照を用いて単一化を実現しようものなら構文木は参照に汚染され，純粋関数型に実装しようものなら大量の型代入をどのような順序で適用したものか悩まされる． これは Hindley-Milner 型推論器を実装する上での宿命のようなものです． 本記事では，MLのサブセット——型付きλ計算をletと参照で拡張した，let多相をサポートする言語——の型推論器を Coq で実装し，その正当性を証明します． Coq で検証を行うことで我々は型推論器のバグへの恐怖とデバッグの労力から真に解放され，枕を高くして眠ることができることでしょう． もっとも、型付きλ計算を let 多相で拡張した言語の型推論器の正当性は実はすでに証
TopProver
Coq competition Coq をはじめとする証明支援システムを用いるコンテストサイトです 出題を希望して下さる方や、質問,要望,バグ報告などご用のある方は、@asi1024 までご連絡お願いします。 初心者の方は 環境準備: CoqIDE (公式サポートの対話型証明アシスタント) を使う場合 GitHub のリリースページ: The release page on GitHub CoqIDE を使わない場合 Coq のインストール: Install Coq with opam 対話型証明アシスタントの導入 Proof General (Emacs) vscoq (Visual Studio Code) 有名な教材: Software Foundations その他 FAQ 利用規約 採点環境の Coq のバージョンアップデートについて (2020/05/03)
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
Coqと少しの圏論が分かる人向けのhomotopy type theory(その1) -
The HoTT Book http://homotopytypetheory.org/book/ が完成したらしいけど、どっちかというと、数学者向けに書かれてて500ページもある。homotopy type theoryで今できてることって、CoqやAgdaで書いたら、せいぜい数千行とか、そんなもんじゃないかと思うので、長すぎる気がする 一応、HoTTに関わる知識は、型理論の他に、ホモトピー論や圏論(モナドとかHaskell関連で出てくる類の知識はあまり知らなくてもいいけど、higher categoryとか教科書に書いてなさそうな話題や、モデル圏とかを知ってるといい)があって、全部真面目に勉強しようと思うと、それぞれのテーマで一冊以上の本が書ける。ただ、実際には、ホモトピー論や圏論はアイデアや視点を提供しているだけで、あくまでCoqやAgdaで書かれてる部分が重要なので、ホモトピー論や
IIJ Research Laboratory
ネットワークの計測と解析 インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行う ために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術 速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの 基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで
Software Foundations
The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software. The principal novelty of the series is that every detail is one hundred percent formalized and machine-checked: the entire text of each volume, including the exercises, is literally a "proof script" for the Coq proof assistant. The exposition is intended for a broad range of readers, fro
Formalizing 100 Theorems
Theorems in the list which have not been formalized yet are in italics. Formalizations of constructive proofs are in italics too. The difficult proofs in the list (according to John all the others are not a serious challenge "given a week or two") have been underlined. The formalizations under a theorem are in the order of the list of systems, and not in chronological order. The List The Irrationa
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Logic: Logic in Coq
GitHub - jonsterling/coq-domains
GitHub - jldodds/coq-lean-cheatsheet: A quick reference for mapping Coq tactics to Lean tactics
GitHub - affeldt-aist/infotheo: A Coq formalization of information theory and linear error-correcting codes
GitHub - verse-lab/ceramist: Verified hash-based AMQ structures in Coq
UseAuto: Theory and Practice of Automation in Coq Proofs