ソフトウェアの基礎 1.0.2 documentation
索引
索引
目次
前書き
Basics_J: 関数プログラミングとプログラムの証明
Lists_J: 直積、リスト、オプション
Poly_J:多相性と高階関数
Gen_J: 帰納法の仮定の一般化
Prop_J: 命題と根拠
Logic_J: Coqにおける論理
Rel_J:関係の性質
SfLib_J: Software Foundations ライブラリ
Imp_J: 単純な命令型プログラム
ImpParser_J: Coqでの字句解析と構文解析
Equiv_J: プログラムの同値性
ImpList_J: Imp のリスト拡張
Hoare_J: ホーア論理
HoareAsLogic_J: 論理としてのホーア論理
Smallstep_J: スモールステップ操作的意味論
Types_J: 型システム
Stlc_J: 単純型付きラムダ計算
Typechecking_J: STLCの型チェッカ
MoreStlc_J: 単純型付きラムダ計算についてさらに
Records_J: STLCにレコードを追加する
References_J: 変更可能な参照の型付け
Subtyping_J :サブタイプ
RecordSub_J: レコードのサブタイプ
Norm_J: STLCの正規化
UseTactics_J:Coq用タクティックライブラリのご紹介
UseAuto_J: Coqの証明自動化の理論と実際
LibTactics_J: 使いやすい汎用タクティックのコレクション
PE_J: 部分評価
Postscript_J: あとがき
検索
モジュール、クラス、または関数名を入力してください