2013年度前期・数理解析・計算機数学 II
[ ホーム | 講義 ] 2013年度前期・数理解析・計算機数学 II (同 概論II) レポート課題 レポート課題 提出期限 2013年8月2日(金) 講義予定 シラバス 第1回 4月12日 Coq で関数型プログラミング 講義メモ 資料 EmacsでCoqを使う 設定ファイル coq.emacs (.emacs にコピーす る) 第2回 4月19日 Coqの論理 講義メモ 第3回 4月26日 述語論理と帰納法 講義メモ 第4回 5月10日 帰納的な定義と多相性 講義メモ 第5回 5月17日 プログラムの証明1 講義メモ 第6回 5月24日 プログラムの証明1 5月25日 14時半〜17時半 多元307号室 (ご興味の方) Proof Cafe: 先輩達によるCoqの勉強会 第7回 5月31日 プログラムの証明2 講義メモ 6月7日 名大際のため休講 第8回 6月14日 数学的な証明 講
IIJ Research Laboratory
ネットワークの計測と解析 インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行う ために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術 速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの 基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで
Asai Laboratory, Ochanomizu University
継続計算に対する仮想機械の導出 定理証明系Coqを使った各種継続計算の性質の証明 対称 λ 計算 shift/resetを含む部分評価器の実装 MinCamlコンパイラ，Caml Lightにおけるshift/resetの実装 証明木(ほか)の可視化 お茶大情報科学科の時間割自動作成 『四則演算インタプリタを作ろう！』 四則演算インタープリタをつくりましょう 末尾呼び出し(tail call)と継続渡し形式(Continuation Passing Style) lexer（字句解析器）と parser（構文解析器）の作成 (サンプルコード) 局所変数の導入 関数(closure)の追加 大域脱出(exit)の追加 再帰関数の追加 FelleisenのCオペレータ リストの追加 Promptの導入 control/prompt から shift/reset への拡張 対称 λ 計算 Coq
CS 3234 Home Page
CS 3234 - Logic and Formal Systems, Semester 1 2010-2011 Module Calendar News Brief Description Material Assignments Labs, Coq Homework and Quizzes More Module Information Calendar For lecture, tutorial, lab, office hour, quiz, exam times, and assignment and homework submission deadlines, see the calendar below. News Notes on Traditional Logic, second set of slides, first assignment and first Coq
はてなグループの終了日を2020年1月31日(金)に決定しました - はてなの告知
はてなグループの終了日を2020年1月31日(金)に決定しました 以下のエントリの通り、今年末を目処にはてなグループを終了予定である旨をお知らせしておりました。 2019年末を目処に、はてなグループの提供を終了する予定です - はてなグループ日記 このたび、正式に終了日を決定いたしましたので、以下の通りご確認ください。 終了日: 2020年1月31日(金) エクスポート希望申請期限:2020年1月31日(金) 終了日以降は、はてなグループの閲覧および投稿は行えません。日記のエクスポートが必要な方は以下の記事にしたがって手続きをしてください。 はてなグループに投稿された日記データのエクスポートについて - はてなグループ日記 ご利用のみなさまにはご迷惑をおかけいたしますが、どうぞよろしくお願いいたします。 2020-06-25 追記 はてなグループ日記のエクスポートデータは2020年2月28
はてなグループの終了日を2020年1月31日(金)に決定しました - はてなの告知
はてなグループの終了日を2020年1月31日(金)に決定しました 以下のエントリの通り、今年末を目処にはてなグループを終了予定である旨をお知らせしておりました。 2019年末を目処に、はてなグループの提供を終了する予定です - はてなグループ日記 このたび、正式に終了日を決定いたしましたので、以下の通りご確認ください。 終了日: 2020年1月31日(金) エクスポート希望申請期限:2020年1月31日(金) 終了日以降は、はてなグループの閲覧および投稿は行えません。日記のエクスポートが必要な方は以下の記事にしたがって手続きをしてください。 はてなグループに投稿された日記データのエクスポートについて - はてなグループ日記 ご利用のみなさまにはご迷惑をおかけいたしますが、どうぞよろしくお願いいたします。 2020-06-25 追記 はてなグループ日記のエクスポートデータは2020年2月28
Coq Tips
以下、Parameters A B C P Q R : Prop. を仮定。 目次 前件 (仮定) が……の場合 仮定が False の場合・仮定に矛盾がある場合 仮定が否定の場合 (~A の形) 仮定が含意の場合 (A -> B の形) 仮定が連言の場合 (A /\ B の形) 仮定が選言の場合 (A \/ B の形) 仮定が全称量化子 (forall) の場合 仮定が存在量化子 (exists) の場合 後件 (ゴール) が……の場合 ゴールが True の場合 ゴールが False・否定の場合 ゴールが含意の場合 (A -> B の形) ゴールが連言の場合 (A /\ B の形) ゴールが選言の場合 (A \/ B の形) ゴールが全称量化子 (forall) の場合 ゴールが存在量化子 (exists) の場合 ゴールが恒真命題 (トートロジー)
Coq クィックリファレンス
Coq クィックリファレンス 書きかけだけれど、たぶん永遠に書きかけなので、とりあえず書いたところだけ公開。 基礎知識 Gallina の構文と Vernacular コマンド オプション モジュール Prop vs. Set vs. Type タクティク リファレンス 証明の補助: idtac, fail, move, clear, set, remember, pose, rename, intro, assert, cut, lapply, specialize, generalize 項による証明: exact, refine, apply 否定と矛盾: absurd, contradict, contradiction 帰納法と場合分け: fix, cofix, elim, induction, case (case_eq), destruct, intros, decompos
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
はてなグループの終了日を2020年1月31日(金)に決定しました - はてなの告知
はてなグループの終了日を2020年1月31日(金)に決定しました 以下のエントリの通り、今年末を目処にはてなグループを終了予定である旨をお知らせしておりました。 2019年末を目処に、はてなグループの提供を終了する予定です - はてなグループ日記 このたび、正式に終了日を決定いたしましたので、以下の通りご確認ください。 終了日: 2020年1月31日(金) エクスポート希望申請期限:2020年1月31日(金) 終了日以降は、はてなグループの閲覧および投稿は行えません。日記のエクスポートが必要な方は以下の記事にしたがって手続きをしてください。 はてなグループに投稿された日記データのエクスポートについて - はてなグループ日記 ご利用のみなさまにはご迷惑をおかけいたしますが、どうぞよろしくお願いいたします。 2020-06-25 追記 はてなグループ日記のエクスポートデータは2020年2月28
Certified Programming with Dependent Types
Certified Programming with Dependent Types Introduction Some Quick Examples Introducing Inductive Types Inductive Predicates Infinite Data and Proofs Subset Types and Variations General Recursion More Dependent Types Dependent Data Structures Reasoning About Equality Proofs Generic Programming Universes and Axioms Proof Search by Logic Programming Proof Search in Ltac Proof by Reflection Proving i
2009年度後期・数理解析・計算機数学 III
[ ホーム | 講義 ] 2009年度後期・数理解析・計算機数学 III (同 概論III) レポート課題 プログラミング課題 提出期限 2010年1月15日(金) レポート課題 提出期限 2010年2月8日(月) 講義予定 シラバス (修正版) 第1回 10月7日 Objective Camlプログラミングの基礎: 定義と型 講義メモ 資料 EmacsでOCamlを使う (修正版) 第2回 10月14日 多相型と汎関数 第3回 10月21日 関数グラフの描画 関数描画ライブラリー plot.ml plot.mli 再帰関数 10月28日は出張で休講 第4回 11月4日 リストと構造的帰納法 第5回 11月11日 再帰的アルゴリズム1 講義メモ 第6回 11月18日 再帰的アルゴリズム2 講義メモ 第7回 11月25日 GUIとグラフィックス 講義メモ 第8回 12月2日 Coqで関数型プ
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
ソフトウェアの基礎
ProofCafe/Coq01 - ocaml-nagoya