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/SSReflect/MathCompで解析入門の1章の命題を全て証明
はじめにCoqで解析入門の1章にある命題を全て証明してみたので記事を書いてみます。 Coqでの証明大学で記号論理学の授業を受けたことはありますか？記号論理学では数学の命題を証明木を用いて形式的証明をしていましたがCoqでも形式的証明をします。流れは以下です。 数学の命題を論理記号で書きますゴールが表示されるので適切にCoqのTacticを使いますするとゴールが変わるので未証明のゴールがなくなるまで繰り返しTacticを使います Coqでの証明の魅力は 証明が正しいことをCoqが保証してくれること(Coqにバグがあるかもしれませんが多分)証明した定理が他の定理の証明に使えて楽しいところ などです。 やろうと思った背景大学1年生の頃、解析入門を前から読んで途中で理解できなくなって読み直すというのを繰り返していました。 いつか理解したいなと思っていたときに記号論理学の授業を受けて解析入門の証明も
Coq Tutorial at Proof Summit 2011
This document discusses the Coq proof assistant. It provides examples of defining concepts like booleans, natural numbers, and functions in Coq. It demonstrates tactics for proving properties like De Morgan's laws. It also shows how to define recursive functions over natural numbers like addition and equality testing. The document aims to introduce basic concepts and usage of the Coq system throug
Coqで学ぶ証明プログラミング！ テストだけでなく「証明」で安全性を保証する - エンジニアHub｜Webエンジニアのキャリアを考える！
Coqで学ぶ証明プログラミング！ テストだけでなく「証明」で安全性を保証する プログラミング言語「Coq」では、プログラムを「証明」して間違いを防ぐことができます。プログラムの正しさを保証できる一歩進んだエンジニアになりましょう！ coqtokyoを主催する今井宜洋さんの解説です。 みなさん、Coqってご存知ですか？ プログラムを証明して間違いを防ぐという優れものです。今回はそのCoqについて、coqtokyoという勉強会を主催している今井宜洋がお届けします。 プログラムをただ作るだけではなく、その正しさを保証できる一歩進んだエンジニアになってみましょう！ Coqって何？ プログラムを「証明する」ってどういうこと？ Coqを使ってみよう Coqのインストール方法 CoqIDE：Coqによる証明開発のフロントエンド Coqで関数プログラミング プログラムの仕様を記述しよう 証明開発モード ゴ
Verlang と Coq の Extraction について - Qiita
この記事は Theorem Prover Advent Calendar 2014 の5日目の記事です。 昨日は notogawa さんの ブラウザ上でAgdaを試せるサイトを作ってみた でした。Try Agda、前に見せていただいたときよりかなり綺麗になっててビビりました。自分の ProveEverywhere はやるやる言いながら放置なので、ダメですね… さて、本題ですが、Coq には Extraction という、Coq のコードを別の言語に変換する機能があり、この機能によってコードを検証済みの部品として実際のプログラムに使えるようになっています。標準では OCaml, Haskell, Scheme への変換が可能になっています。 この記事では、Verlang という、Coq の Extraction 対象に Erlang のコア言語である Core Erlang を加えるパッチ
Coq/SSReflect/MathCompの設定
[2023-02-24 Fri]: Ubuntu 22.04.1 LTS, Coq 8.16.1, MathComp 1.16 [2023-01-06 Fri]: Ubuntu 22.04.1, opam 2.1.4, ocaml 4.14.1, Coq 8.16.1, ProofGeneral 4.6, MathComp 1.15.0, MathComp-Analysys 0.6.0 [2022-09-09 Fri]: Ubuntu 22.04.1, Coq 8.15, MathComp 1.15 (opam), ProofGeneral 4.6 [2022-08-03 Wed]: Windows 11, Coq 8.15, MathComp 1.15 (WSL 2) [2022-03-01 Tue]: Windows 11 21H2, Coq 8.15, MathComp 1.14 (
Coq のカリー・ハワード同型周辺について - Qiita
Coq のカリー・ハワード同型周辺についてメモ．間違いあればご指摘ください． Coq と CoC Coq は元々，Thierry Coquand 氏により提案された Calculus of Constructions (CoC) という型システムの実装として生まれました． その後 CoC は，帰納的データ型などが追加された Calculus of Inductive Constructions (CIC) に拡張され，現在の Coq は CIC の実装となっています． CoC/CIC は，基本的には型システムを定義しただけのものなのですが，実は Coq の証明システムはこの型システムがベース となっています． これは一体どういうことか，次からの節で，直観的な例を通して見ていくことにします． プログラム ≈ 証明 一般に，プログラムの型システムは，次の図みたいな推論木を組み立ててプログラムの
Reddit - Dive into anything
Computer Science Theory and Application. We share and discuss any content that computer scientists find interesting. People from all walks of life welcome, including hackers, hobbyists, professionals, and academics.
A Tale of Two Provers
A Tale of Two Provers Verifying Monoidal String Matching in Liquid Haskell and Coq Niki Vazou University of Maryland Leonidas Lampropoulos University of Pennsylvania Jeff Polakow Awake Networks Abstract We demonstrate for the first time that Liquid Haskell, a refinement type checker for Haskell programs, can be used for arbitrary the- orem proving by verifying a parallel, monoidal string matching
Using Coq to Write Fast and Correct Haskell
Using Coq to Write Fast and Correct Haskell John Wiegley BAE Systems USA john.wiegley@baesystems.com Benjamin Delaware Purdue University USA bendy@purdue.edu Abstract Correctness and performance are often at odds in the field of sys- tems engineering, either because correct programs are too costly to write or impractical to execute, or because well-performing code involves so many tricks of the tr
Cosette: An Automated SQL Solver
Cosette is an automated prover for checking equivalences of SQL queries. It formalizes a substantial fragment of SQL in the Coq Proof Assistant and the Rosette symbolic virtual machine. It returns either a formal proof of equivalance or a counterexample for a pair of given queries. Checking SQL Equivalences in Cosette You can try the Cosette demo online, using Cosette Web API or download its sourc
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
テスト駆動開発から証明駆動開発へ #JTF2019 / July Tech Festa 2019
ソフトウェアの基礎(beta) — ソフトウェアの基礎 1.0.2 documentation
GitHub - coq/coq: Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Community | The Coq Proof Assistant
http://www.psg.cs.titech.ac.jp/files/ppl2016_actario_poster.pdf
GitHub - tcarstens/verlang
collacoq
GitHub - krtx/agda-handson: agda handson
