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
Tsukuba Coq Users' Group
茨城県つくば市周辺の Coq ユーザのグループです。同人誌の発行等の活動をしています。 本 Coq による定理証明 2016.12 Coq による定理証明 2015.12 Coq による定理証明 2014.12 Coq による定理証明 2014.8 Coq による定理証明 2013.12 Coq による定理証明 - コンビネータ論理 C83版 Coq による定理証明 - Coq でスタック指向プログラミング 参加イベント コミックマーケット92 技術書典2 コミックマーケット91 コミックマーケット89 コミックマーケット87 コミックマーケット86 コミックマーケット85 メンバー 坂口 和彦 平井 洋一 石井 大海
CakeML
About CakeML is a functional programming language and an ecosystem of proofs and tools built around the language. The ecosystem includes a proven-correct compiler that can bootstrap itself. The CakeML project consists of the following components, all of which are free software. Language definition. The CakeML language is based on a substantial subset of Standard ML. Its formal semantics is specifi
ProofCafe - 名古屋を中心に活動する定理証明器・関数型言語のコミュニティ
開催勉強会 ProofCafeではいくつかの勉強会を定期開催しています。 詳細は個別のページをご覧ください。 Coqを用いたプログラムの証明について勉強する勉強会です。 コーヒーを飲みながら楽しく証明しましょう。 TAPL-nagoya Types and Programming Laungages(通称TAPL)の読書会です。 ScalaやF#などの静的型付け言語の基礎になっている型理論について学びます。 休日カフェタイム, KCTNagoya 圏論に関する勉強会です。 どえりゃあ Haskell Haskellに関する勉強会です。 サービス Software Foundations(和訳) Benjamin C. Pierce氏による同名のテキストの和訳です。関数プ ログラミグやラムダ計算についてCoqによる実例を交えながら丁寧 に説明されています。 Cochin Coqの定理検索サー
Vim で Coq 環境を整える - 反省はしても後悔はしない
はじめに 昨日、スタート Ssreflect というイベントに参加して、Coq + ssreflect のハンズオン的なものをやりました。 Coq 環境といえば、Emacs の ProofGeneral が非常に有名です。 しかし、私は Emacs は終了の仕方すら分からないレベルの初心者なので Emacs + ProofGeneral ではチュートリアルの例題を打ち込むだけでも非常に苦労しました。 証明も普段使い慣れている Vim で何とかできないかと思い調べたところ、そこそこ良さ気な環境を構築できたので紹介します。 使用するプラグイン 以下の2つをインストールします。NeoBundle のようなパッケージマネージャを使用するのをおすすめします。 jvoorhis/coq.vim vim-scripts/CoqIDE jvoorhis/coq.vim は Coq のシンタックスとインデン
IIJ Research Laboratory
ネットワークの計測と解析 インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行う ために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術 速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの 基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで
ホーム - Coq演習2014(仮)
Coq演習2014 について 世の中には締め切りがないとなかなか勉強できないという人がいます。そこで、Coqの証明課題に締め切りつきで取り組める企画というのがあれば、今まで興味があるが手を出せなかった人もCoqをはじめることができるのではないかと考えました。それがこの「Coq演習2014」です。 あと、まとまった資料を作ろうとするとだいたい先にやる気が切れてしまうので、資料は最低限のものだけに留めようと思います。できるだけ省パワーでやります。必要な情報は自力で収集しましょうというスタンスです。もちろん、質問には答えます。 この企画は担当のやる気がなくなったら終了(お流れ)になります。ごめんなさい。 形式 2学期制の大学の1学期分と考えて、1週間に1回の演習を13-15回程度行う形式でいこうかなと考えています。 これは単なる自主企画なので、実際の単位にはなりませんが、雰囲気を出すために評定を
Welcome! | The Coq Proof Assistant
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. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, the Verified Software Toolchain f
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Tutorial Materials for Programming Language Research
Amazon.com: Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant (The MIT Press): Chlipala, Adam: Books
Coq による定理証明 2013.12
ソフトウェアの基礎
Elimination with a Motive (Conor McBride)
Home