ソフトウェアの基礎
このページは Software Foundations の日本語翻訳版「ソフトウェアの基礎」です。 「ソフトウェアの基礎(Software Foundations)」シリーズでは、高信頼ソフトウェアに関する広範囲の数学的基礎を学びます。 このシリーズの特徴は、取り扱う内容がすべて形式化されて、さらに機械によって確かめられることです。 これは、それぞれのテキストがCoqのスクリプトファイルそのものとなっていることで実現されています。 読者は、学部生から博士課程の学生や研究者に至るまでの広範囲を想定しています。 論理学やプログラミング言語についての知識は仮定しませんが、ある程度の数学的素養は理解に有用です。 1学期分の講義として、論理の基礎に加えて、プログラミング言語の基礎または検証済み関数型アルゴリズム、あるいは両方の一部を扱うように設計されています。
2020年度後期・数理解析・計算機数学 II
[ ホーム | 講義 ] 2020年度後期・数理解析・計算機数学 II (同 概論II) レポート課題 レポート課題 提出期限 2021年1月27日(水) (1月13日10時45分訂正) 講義予定 シラバス 1回目（10月7日1限）の教室は多元109号室に変更 2回目以降も多元109号室で講義を行う 第1回10月 7日 Coq/SSReflectの論理 講義メモ 資料 EmacsでCoqを使う 設定ファイル coq.emacs (.emacs にコピーす る) 第2回10月14日 述語論理とSSReflectのタクティック 講義メモ 第3回10月21日 再帰的な定義と帰納法 講義メモ 第4回10月28日 帰納的な定義と多相性 講義メモ 第5回11月4日 Mathcomp, 自己反映と単一化 講義メモ ssrbool_doc.pdf, ssrnat_doc.pdf (R. Affeldt の
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をベースとしたハードウェア表現および生成プラットフォーム"Kami"を試す - FPGA開発日記
MITのプログラム言語を研究しているグループの検証プラットフォーム「Kami」の論文を読んでいる。 KamiとはCoqをベースとしたDSLで、ハードウェアを表現するための言語およびそのプラットフォーム。KamiはCoqのハードウェア記述から検証、ハードウェア生成までを行うことを目的とする。 論文は以下に掲載されている。30ページもあり長い。 Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification http://plv.csail.mit.edu/kami/papers/icfp17.pdf とりあえず動かしてみる。以下のリポジトリを使おう。 github.com # Revision : ed1d6cd $ git clone git@github.com:
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
The Pip Protokernel
GitHub - rudynicolop/TAPL-Coq: Coq implementations of and proofs of properties of typed-languages in Benjamin Pierce's Types and Programming Languages
Files · masters/rusthornbelt · Iris / lambda-rust · GitLab
http://staff.ustc.edu.cn/~fuming/research/certiucos/paper.pdf
Featherweight VeriFast
Separation Logic Foundations
Verifiable C
GitHub - uw-unsat/nickel
The Tactician
GitHub - sifive/Kami: Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older version from MIT
GitHub - maruyama097/coq-tutorial: coq-tutorial
GitHub - EugeneLoy/coq_jupyter: Jupyter kernel for Coq
A Formal C Memory Model for Separation Logic - Journal of Automated Reasoning
Iris Project
Verifiable C
Amazon.co.jp: Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化: 萩原学, アフェルト・レナルド: 本
