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
ssreflectインストール方法まとめ(Windowsもあるよ!) - みずぴー日記
「春は証明をはじめる季節」と某氏*1がよくわからないことを言いだしたので、Modern Coqことssreflectの勉強会を開催しました。(スタートssreflect #1) 勉強会にはだいたい30人くらいの方が参加し*2、全員がssreflectを使った証明を実際に行いました。そのため、30個の様々な環境にssreflectがインストールされたわけなので、その結果をまとめておきます。 元データ https://docs.google.com/spreadsheets/d/1X_vRVO3eizebOyG4tjcChzUZofrE9AGWwMEqUCyKKHs/edit?pli=1#gid=0 Windowsの場合 自分でビルドするのは地獄の道らしいので、コンパイル済みのバイナリを使います。ssreflectはMicrosoft製なだけあって、Windowsが一番インストールが楽ですね:
MSR-INRIAMathematical Components - Microsoft Research Inria Joint Centre
Language theory and mathematical logic provide powerful tools for reasoning about, verifying and generating programs. Research in formal methods focuses on three main targets: ... Andrea Asperti University of Bologna (Visiting Professor) Jeremy Avigad Carnegie Mellon University (Invited) Bruno Barras Inria Saclay - Île-de-France Yves Bertot INRIA Sophia Antipolis - Méditerranée Guillaume Cano Inri
A Small Scale Reflection Extension for the Coq system
MSR - INRIA - Microsoft Research - Inria Joint Centre (Parc Orsay Université 28, rue Jean Rostand 91893 Orsay Cedex FRANCE - France) 65197Inria - Institut National de Recherche en Informatique et en Automatique (Domaine de Voluceau Rocquencourt - BP 105 78153 Le Chesnay Cedex - France) 300009Microsoft Research Laboratory Cambridge (Royaume-Uni) 301681Microsoft Corporation [Redmond, Wash.] (États-U
SSReflect CheatSheet - Proving - kik
...; last 3 [tactic1 | tactic2 | tactic3] || tactic4
ssreflect ライブラリ紹介(eqType編) - 菊やんの雑記帳
この記事はTheorem Proving Advent Calendar 2011の13日目の記事です。 ssreflectライブラリ紹介 この前はssreflectのtacticの紹介をやったので、ライブラリの紹介をします。ライブラリの概要は http://coqfinitgroup.gforge.inria.fr/ssreflect-1.3/ を見れば何か数学寄りだなというのが分かると思いますが、まあ完全に数学寄りです。しかもtrunkでは http://coqfinitgroup.gforge.inria.fr/ のように大変膨大になっております。 eqType というわけで、一番根っこの部分にあるeqTypeを今回のメインにしましょう。 Coqを使い始めると、まあ誰でもこんな感じに書きたくなるでしょう。 Definition nat_gt0 := { x : nat | x > 0
tree@SSReflect
tree@SSReflect 「Ssreflect って何ですか?」 「ごめんね，正直言って，よくわかってないんだ」 「は ?」 「あ，いや，えーと，決定可能な命題が? reflection でいい感じに扱える? みたいな?」 「は ?」 Ssreflect なるものの存在を知ったのは随分と前，学部を卒業した頃には既に知っていたような記憶があるから，修士を終えて半年経った今から数えれば，少なくとも 2 年以上は昔の話になる． しかし，そこに付随する記憶は決して 「Ssreflect 使いこなしてーの証明バリバリQ.E.D!」 といったものではなく ， 「インストールできねぇ」 の一言に尽きる．とにかくインストールできなかったので，何度も挑戦した挙句早々と諦めた，そんな記憶しかない．上手くいったことが一度でもあれば使った記憶があるだろうから，使った記憶が無いということで，対偶取ってそういうこ
Ssreflect拡張 - Coq - Wikipedia
Coqは、証明支援システムの一つ。Coqの核はプログラミング言語Gallina（英語版）を用いる。フランス国立情報学自動制御研究所のPI.R2チーム(PPS研究所内にある)が、エコール・ポリテクニーク、フランス国立工芸院、パリ第7大学、パリ第11大学と(かつてリヨン高等師範学校とも)共同して開発している。Hugo Herbelinが事実上の開発代表者である。 特徴[編集] CoqはCalculus of constructions（英語版）という高階型システム(Thierry CoquandとGérard Huetが1984年に創始したもので、英語ではCoCと略せてシステム名Coqに至る)に基づく。正しい証明は正しく型がつくラムダ式であるというカリー＝ハワード同型対応を利用しているので、Coqの証明言語は型付きラムダ計算の一種である。1991年以降Coqが用いているCalculus of
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
SSReflectノート (暫定版) - Qiita
スタックコンパイラの証明 - Qiita