テスト駆動開発から証明駆動開発へ #JTF2019 / July Tech Festa 2019
July Tech Festa 2019 で使用したスライドです。 近年、テストを書く文化は広く普及しており、開発フローにおいて自動テストを組み込むことはもはや常識となりました。しかしよく考えてみると、有限個のテストケースが保証しているのは、所詮「特定の有限個の入力に対する出力」にしか過ぎません。では「あり得る全ての入力」に対してプログラムの性質を保証することは果たして可能でしょうか？ この問いに対する答えのひとつが「定理証明」と呼ばれる手法です。定理証明では、数学的な「証明」をプログラム上でエンコードすることにより、真に「全ての入力」を扱うことができます。本セッションではこの定理証明を取り上げ、従来のテストとの考え方の違いや具体的な適用方法について、サンプルを交えつつ解説します。 イベント概要：https://2019.techfesta.jp/speakers#A10
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
Formal Reasoning About Programs
This is the web site for the early stages of a book introducing both machine-checked proof with the Coq proof assistant and approaches to formal reasoning about program correctness. Grab a Draft Source on GitHub Quasi-latest PDF draft Quasi-latest source-code tarball Quasi-latest source-code tarball, library only (warning: the author really does not recommend using it in serious projects!) Use in
Mathematical Components (the book)
About Mathematical Components is the name of a library of formalized mathematics for the Coq proof assistants. It covers a variety of topics, from the theory of basic data structures (e.g., numbers, lists, finite sets) to more advanced results in various flavors of algebra. This library constitutes the infrastructure for the machine checked proofs of the Four Color Theorem and of the Odd Order The
CoqのLtacでmap関数を実装する - 俺の Colimit を越えてゆけ
はじめに length関数を実装する Gallina 風の実装 Ltac から Gallina へ Gallina の項を Ltac 呼び出しの結果として受け取る 気持ち悪い点 map関数(Ltac引数)を実装する map関数(Gallina引数)を実装する 最後に 参考書籍 はじめに Ltac は、Coq において証明の探索を自動化するための Domain Specific Language です。Coq においてプログラムを記述する言語は Gallina と呼ばれていて、これは依存型を持つ普通の関数型言語で意味論も目的も Ltac とは全く別物です。 Gallina で map関数を実装することは Haskell や OCaml で map関数を実装するのとほとんど同じで普通のことです。一方、Ltac は証明の探索の自動化を目的としているので普通の関数型言語と同じようにとはいかないので
Use Coq in Your Browser: The Js Coq Theorem Prover Online IDE!
Welcome to the JsCoq Interactive Online System! Welcome to the JsCoq technology demo! JsCoq is an interactive, web-based environment for the Coq Theorem prover, developed at the Centre de Recherche en Informatique of MINES ParisTech (former École de Mines de Paris). Instructions: JsCoq is open source. If you find any problem or want to make any contribution, you are extremely welcome! We await you
リフレクションのしくみをつくる - Qiita
2015/08/11 2015/08/16 2015/09/12 「スモール SSReflect の製作」から改題 @suharahiromichi はじめに 命題(Prop型)をbool型の式に変換すること（とその逆）をリフレクションと呼びます。 例： x = y と x == y 命題をbool型の計算に変換することで、命題の証明が簡単になる場合があります。そのリフレクションを「狭い範囲」で行い、証明の効率化を図るのが、CoqのSmall Scale Reflection (SSReflect) 拡張です。 今回は、SSReflectのしくみを理解することを目的に、Starndard Coqで「SSReflectもどき」を作り、Leibniz同値関係とbool値等式のリフレクションができるまでを示します。 それを通して、Coqのコアーション(coersion)や、カノニカル・ストラクチ
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
Feit-Thompson true —
Feit-Thompson true Feit-Thompson theorem has been totally checked in Coq Thursday 20 September 2012, 18:16. We received following mail from Georges Gonthier (see below). It concludes the proof in Coq of the Feit-Thompson theorem. This theorem, also named the Odd Order Theorem, is the first main result in the classification of finite groups. This work was achieved by the team formed by addressees o
Category Theory in Coq
This is a quick page I've thrown together for my Coq library formalizing basic category theory. The development follows Steve Awodey's book on category theory; the files are named after chapters and subchapters of that book for easy reference. Getting It The gitweb is here. You might also want to look at the README Design Decisions One of the difficulties with putting together a formalization of c
Formal Verification of Memory Properties
We are interested in the formal verification of low-level software. For this purpose, we have developed in the Coq proof assistant formalizations of Separation logic (as presented in the survey by John C. Reynolds). We have applied these formalizations to several use-cases, including: the verification of the heap manager of the Topsy operating system (paper) the verification of arithmetic function
Asai Laboratory, Ochanomizu University
継続計算に対する仮想機械の導出 定理証明系Coqを使った各種継続計算の性質の証明 対称 λ 計算 shift/resetを含む部分評価器の実装 MinCamlコンパイラ，Caml Lightにおけるshift/resetの実装 証明木(ほか)の可視化 お茶大情報科学科の時間割自動作成 『四則演算インタプリタを作ろう！』 四則演算インタープリタをつくりましょう 末尾呼び出し(tail call)と継続渡し形式(Continuation Passing Style) lexer（字句解析器）と parser（構文解析器）の作成 (サンプルコード) 局所変数の導入 関数(closure)の追加 大域脱出(exit)の追加 再帰関数の追加 FelleisenのCオペレータ リストの追加 Promptの導入 control/prompt から shift/reset への拡張 対称 λ 計算 Coq
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Verified Functional Algorithms
Preuves de programmes en coq - Yves Bertot INRIA
Coq.io
Coq による定理証明 2013.12
http://blog.ezyang.com/2012/09/feit-thompson-true/
How to Make Ad Hoc Proof Automation Less Ad Hoc | Lambda the Ultimate
Vellvm: Formalizing the LLVM Intermediate Representation for Verified Program Transformations | Lambda the Ultimate
Typeclass
