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
Computation and Logic: Winter Semester 2016
お知らせ 宿題を遅れて提出する場合の最終期限は 2/3(金) 17:00 です．要再提出が残っている人もこの時刻までに解決してください． スライド8と配布資料その4をアップロードしました．(2017.1.23) 1/17(火)は、(講義ホームページにある)予定を変更して2回目の演習とします。過去の期末試験(ホームページからダウンロードしてください。)の問題も演習の範囲とします。(2017.1.9) 過去の期末試験(2012年度, 2013年度, 2014年度, 2015年度)をアップロードしました(テキストと同じパスワードでダウンロードしてください)．演習の追加題材とします．(2016.12.31) スライド7アップロード．宿題その7がでました．(2016.12.19) 宿題その6の問題 or_distributes_over_and_2 は or_distributes_over_and
An afternoon of DTT/theorem provers: Agda and Coq
Note from 23rd August, 2017 I found this draft blog post lying around, written in the spring of 2015 while I was working at Imperial College London as a Research Associate in the Mobility Reading Group with Nobuko Yoshida. This was the fruit of a discussion with Tiago Cogumbreiro where we were comparing Coq and Agda for theorem proving. I believe we had a few more “side-by-side” comparisons writte
Writing a Formally-Verified Porn Browser in Coq and Haskell
It’s uncommon to use formal verification when developing software. Most people are unfamiliar with the tools and techniques, or assume they’re only for specialized use. This article will show how to write a simple image browser with: Core data structures and operations formally verified using the Coq theorem prover. A Haskell web server that handles HTTP requests An HTML/CSS/Javascript frontend De
PowerPoint プレゼンテーション
Ruby Extension Library Verified using Coq Proof-assistant Tanaka Akira National Institute of Advanced Industrial Science and Technology (AIST) RubyKaigi 2017 2017-09-20 2 About This Talk • Formal verification for fast & safe program in C • Quality assurance other than test 3 Materials • Ruby • Coq • C • HTML escape • Intel SSE Do you know all of them? 4 Coq Proof-assistant • Proof assistant – Prog
CoqHammer - Learning-assisted automated reasoning for Coq
We present an architecture of a full hammer for dependent type theory together with its implementation for the Coq proof assistant. A key component of the hammer is a proposed translation from the Calculus of Inductive Constructions, with certain extensions introduced by Coq, to untyped first-order logic. The translation is "sufficiently" sound and complete to be of practical use for automated the
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
curry_howard
自動証明 auto 証明項を直接指定する exact refine 関数抽象を構築する intro move=> (SSReflect) Section 関数適用とその引数部分を構築する revert generalize move: (SSReflect) 関数適用とその関数部分を構築する apply let 式を構築する pose, set specialize have @var (SSReflect) eq_refl で等式を証明する reflexivity eq_ind_r で等式による書き換えを行う rewrite rewrite (SSReflect) match 式を構築する destruct case (SSReflect) simpl change unfold fold pattern clear rename move_after 数学的帰納法を適用する induc
定理証明支援の紹介 - Qiita
目的 定理証明支援とは何かと現状の整理。 定理証明支援とは 定理証明支援とは数学の定理を自動で証明することではなく、ステップバイステップでコンピュータに命令を送り、数学の定理を証明するのを助けるシステムである。 支援だから意味ないということでなく、最近の数学の証明は長くなり証明の検証が難しいのを助ける意味がある。定理証明支援の意義についてはこちらが詳しい。 また、信頼性が求めらる難しいアルゴリズムの検証、たとえばTLS(暗号通信)やRaft(分散合意アルゴリズム)のサーバーに利用されつつある。 ここでいう定理は大げさなものだけでなく、$1+1=2$、$0何か=0$、$ab=b*a$といった簡単なものを証明しながらどんどん積み上げていく。通常のプログラムと違うのは証明であるので使用する変数が整数ならそのすべての値について成り立つ定理を証明する。 定理を証明するのに使うツールは下記である。(他
Coming Soon
We're under construction. Please check back for an update soon.
Total Haskell is Reasonable Coq
We would like to use the Coq proof assistant to mechanically verify properties of Haskell programs. To that end, we present a tool, named hs-to-coq, that translates total Haskell programs into Coq programs via a shallow embedding. We apply our tool in three case studies -- a lawful Monad instance, "Hutton's razor", and an existing data structure library -- and prove their correctness. These exampl
Coqはチューリング完全 -- Ltacでbrainf*ckインタプリタを書いた - Qiita
この記事は、Theorem Prover Advent Calender https://qiita.com/advent-calendar/2017/theorem-prover のために書かれました。 Coqをある程度知っている人向けの小ネタです。 しばしばCoqの紹介において、「Coqでは停止するプログラムしか書けない」「(そのため)Coqはチューリング完全ではない」と言われることがあります。実はこれ、正しいと言えば正しいのですが、間違いと言えば間違いです。 確かに、Coqで再帰関数を定義するためのFixpoint, Program Fixpoint, Functionといったコマンドはどれも停止性を要求します。そのため、Coqから抽出したプログラムは無限ループを起こすことはなく、その意味で安全性が保証されることになります。 では、何が間違いか？ これは「Coqでは停止するプログラム
dbp.io :: How to prove a compiler correct
How to prove a compiler correct At POPL’18 (Principles of Programming Languages) last week, I ended up talking to Annie Cherkaev about her really cool DSL (domain specific language) SweetPea (which she presented at Off the Beaten Track 18, a workshop colocated with POPL), which is a “SAT-Sampler aided language for experimental design, targeted for Psychology & Neuroscience”. In particular, we were
Rust's ownership model formally proven with Coq
source tweet PDF paper In this paper, we give the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Our proof is extensible in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe extension to the language. We have carried out this verific
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
初めて学ぶCoq
Typeclasses: A Tutorial on Typeclasses in Coq
https://www.mimuw.edu.pl/~lukaszcz/coqhammer.pdf
vimでCoqを使えるようにする - Qiita
GitHub - sweirich/corespec: A Specification for Dependent Types in Haskell (Core)
