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:
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が世の趨勢と離れるのか？
静的解析の限界、現実世界との境界
2018年に静的解析をとにかく強力につけまくるのは多分あんまりコストに見合わないのでよくない じゃあ静的解析を窓から投げ捨ててよいかというとそれはただの愚行 (以下、静的解析を普通に使えてる人には自明なことしか言いません) 私が最初に静的解析の限界を感じたのは多分依存型で遊んでいたとき 依存型の力はすごくて、まぁそれもそのはず命題論理から述語論理に進んで元への言及ができるので見かけ上表現力はとんでもなく上がるわけです。例えば「ある方程式を満たす解のみを受け取って何かする」みたいな関数が型として表現できるようになる。 一見すると最強に見えるんだけどこれは実質定理証明をすることなので、制限の強い型をつければつけるほど実装で苦しむ羽目になるということを割とすぐ痛感することになった。 例えば head : Vect (Suc n) a -> a で長さ1以上のvectorの先頭を安全に取り出す関数
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
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
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
Amazon.co.jp: Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化: 萩原学, アフェルト・レナルド: 本
