ソフトウェアの基礎
このページは Software Foundations の日本語翻訳版「ソフトウェアの基礎」です。 「ソフトウェアの基礎(Software Foundations)」シリーズでは、高信頼ソフトウェアに関する広範囲の数学的基礎を学びます。 このシリーズの特徴は、取り扱う内容がすべて形式化されて、さらに機械によって確かめられることです。 これは、それぞれのテキストがCoqのスクリプトファイルそのものとなっていることで実現されています。 読者は、学部生から博士課程の学生や研究者に至るまでの広範囲を想定しています。 論理学やプログラミング言語についての知識は仮定しませんが、ある程度の数学的素養は理解に有用です。 1学期分の講義として、論理の基礎に加えて、プログラミング言語の基礎または検証済み関数型アルゴリズム、あるいは両方の一部を扱うように設計されています。
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
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
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
GitHub - rudynicolop/TAPL-Coq: Coq implementations of and proofs of properties of typed-languages in Benjamin Pierce's Types and Programming Languages
Amazon.co.jp: Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化: 萩原学, アフェルト・レナルド: 本
Program Logics for Certified Compilers | Communications, information theory and security
