テスト駆動開発から証明駆動開発へ #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
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
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
On type safety for core Scala: "From F to DOT: Type Soundness Proofs with Definitional Interpreters" | Lambda the Ultimate
On type safety for core Scala: "From F to DOT: Type Soundness Proofs with Definitional Interpreters" From F to DOT: Type Soundness Proofs with Definitional Interpreters by Tiark Rompf and Nada Amin: Scala's type system unifies aspects of ML-style module systems, object-oriented, and functional programming paradigms. The DOT (Dependent Object Types) family of calculi has been proposed as a new theo
リフレクションのしくみをつくる - 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)や、カノニカル・ストラクチ
Gradual Certified Programming in Coq
Expressive static typing disciplines are a powerful way to achieve high-quality software. However, the adoption cost of such techniques should not be under-estimated. Just like gradual typing allows for a smooth transition from dynamically-typed to statically-typed programs, it seems desirable to support a gradual path to certified programming. We explore gradual certified programming in Coq, prov
Introducing PeaCoq - COQ EN STOCK
What is PeaCoq? Over the past year, I have developed a Coq frontend called PeaCoq (not to be mistaken with Yves Bertot’s Pcoq). If you wish to play with it before or while reading this article, I made an online version available here. Note that it will reset after 15 minutes of inactivity, and that it might go down any time! There have been several attempts at improving user interfaces for proof a
Oregon Programming Languages Summer School
Oregon Programming Languages Summer School — July 16-28, 2012 Logic, Languages, Compilation, and Verification Speakers Organizers Curriculum Schedule Participants The program consists of 80 minute lectures presented by internationally recognized leaders in programming languages and formal reasoning research. Technical Lectures Logical relations — Amal Ahmed Lecture 1 part 1 part 2 part 3 Lecture 2
Coqの型クラスの使い方：バンドル方式とアンバンドル方式 - 檜山正幸のキマイラ飼育記 (はてなBlog)
「Coqで定理を記述してみる、型クラスとか使って」に次のような断り書きを入れました。 ミート半束のような代数構造をどう定義するのが良いのか、あんまり分かってないのですが、まーまー使える方法を紹介します。この方法には課題があることを注意しておきます。今回の目的ではうまくいきますが、より大規模な記述にはもっと効率的な方法が必要かも知れません。 代数構造を定義する別な方法である、スピターズ／ファンデル・ウィーゲンの方式をかいつまんで紹介します。 内容： Bundling is bad 追記： 方式の呼び名 オールインワン方式 バンドル方式 アンバンドル方式 何が違うの？ ソースコード Bundling is bad 「Coqで定理を記述してみる、型クラスとか使って」では、ミート半束と（最大元付き）順序集合を定義するために、「マグマのクラス」と「法則（公理系）を書いたクラス」を使いました。スピター
Coq/SSReflect/MathComp Tutorial
資料: slides (last version): slides addendum about groups: html, pdf (automatically generated) slides (previous versions): [2015-07-24 Fri]: 京都大学の集中講義で使った資料(約14時間): slides (addendum about groups) [2014-12-15 Mon]: 名古屋大学の集中講義 で使った資料(約9時間): slides (addendum about groups) [2014-09-07 Sun]: 日本ソフトウェア科学会 第31回大会のチュートリアル (定理証明支援系Coq入門) で使った資料(4時間): slides Coq/SSReflect/MathCompの設定 参考文献: ssr.bib, coq.bib, it
Programs and Proofs
Mechanizing Mathematics with Dependent Types Lecture notes with exercises Ilya Sergey These lecture notes are the result of the author's personal experience of learning how to structure formal reasoning using the Coq proof assistant and employ Coq in large-scale research projects. The present manuscript offers a brief and practically-oriented introduction to the basic concepts of mechanized reason
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Typeclasses: A Tutorial on Typeclasses in Coq
Verified Functional Algorithms
bitbucketの使い方
Preuves de programmes en coq - Yves Bertot INRIA
HoTT/Coq 覚書
