Default pageYou Are All Set to Go! All you have to do now is upload your website files and start your journey. Check out how to do that below:
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
ATS で組み込みドライバを実装してみる③ - でんちゅーがらす
「――何かを怠けるのに、理由が要るかい？」 はい、ATSでRXの端子ドライバを書いてみる③。今回で最終回です。 今回は、今まで準備してきた道具を使って、端子を操作する簡単なプログラム（証明付き）を書いてみます。 仕様 まずは、どんなプログラムを書くのかを決めねばなりません。↓のようなものを目指します。 ① 起動する。 ② P00端子に500ミリ秒間Highを出力する。 ③ P00端子に250ミリ秒間Lowを出力する。 ④ P00端子に400ミリ秒間Highを出力する。 ⑤ P00端子にLowを出力する。 ⑥ 終了する。 端子の番号は（見てわかる通り）適当です。もし、この端子の先にLEDが繋がっていれば、それが2回点灯することになります。いわゆるLチカです。 では次に、この仕様を型によって表現します。そのためにいくつか新しい定義を行います。 出力履歴 datasort output_dura
Isabelleについて： 証明支援系は何を目指し、どこへ向かうのか - 檜山正幸のキマイラ飼育記 (はてなBlog)
昨日の記事「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」では、Isabelleのユーザーインターフェースが備えている特徴的な機能である「継続的チェッキング」だけを取り上げました。ここで改めて、証明支援系としてのIsabelleシステムを紹介しましょう。客観的な紹介ではなくて、僕の雑駁な印象記です。 内容： Isabelleの独自な世界 Isabelleの未来 Isabelleの独自な世界 「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」より： PIDE構想は、Isabelleプロジェクト／コミュニティを世の趨勢とは離れた孤立化へと導くのか、それとも、時代がPIDEの先進性にいずれ追いつき、PIDEがスタンダードな証明支援系UIとなるのか？ なかなかに興味深いですな。 Isabelleが世の趨勢と離れるのか？
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Files · masters/rusthornbelt · Iris / lambda-rust · GitLab
Featherweight VeriFast
FreeRTOS/FreeRTOS/Test/VeriFast at main · FreeRTOS/FreeRTOS
Beluga/Harpoon user’s manual — Beluga documentation
Beluga/Harpoon user’s manual — Beluga documentation
Push-button verification of systems software
GitHub - data61/PSL
GitHub - mephistopheles-8/atshtml: A static HTML eDSL for ATS2
Isabelle/C
PSL/slide/2019_ps.pdf at master · data61/PSL
GitHub - EugeneLoy/coq_jupyter: Jupyter kernel for Coq
ソフトウェア開発を工学にする形式手法の紹介 - formal_methods.pdf
GitHub - Rust-Proof/rustproof: rust verification condition generator
GitHub - leanprover/theorem_proving_in_lean: Theorem proving in Lean
Lean Web Editor