Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions (Texts in Theoretical Computer Science. An EATCS Series)

Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions (Texts in Theoretical Computer Science. An EATCS Series)
お得情報
  • Amazonマーケットプレイス
    ¥ 14,508 より
  • 購入3
  • クリック28
  • 言及数8ブログ
  • ブックマーク0users
「Interactive Theorem Proving and Program Developmen...」をAmazonで購入する
amazon.co.jp 詳細ページへ

商品の紹介

It is based on a theory called the calculus of inductive constructions, a variant of type theory. This book provides a pragmatic introduction to the development of proofs and certified programs using Coq.

「Interactive Theorem Proving and Program Developmen...」を含むはてなダイアリーの人気ブログ この商品についてブログを書く

  • Coq | 今回は、入門記事書きはちょっと休憩して、Coqの解説記事などを集める会です。英語言語そのものを浅く/深く眺めていく、という方向のテキスト3つ:Coq in a Hurry「忙しい人のためのCoq入門」。比較的よくまとまっている気がしました。Coq Proof Assistant: A Tutorial 本家のチュートリアルInteractive Theorem Proving and 続きを読む

    2010-10-12 - ひとり勉強会hzkr2010/10/139 users
  • Coq | 前からずっと取り組んでいた「Coqで単純型付きラムダ計算を証明してみよう」が一段落しました。 動機let多相の実装はしたから、次は証明だろ 最近、流行っているCoqを覚えたい 扱えるラムダ式型は、Bool型と関数型のみ。 Inductive type : Set := | BoolT : type | FunT : type -\u003e type -\u003e type. 式は、変数参照、真偽値、ラ 続きを読む

    Coqでラムダ計算を証明してみた - みずぴー日記mzp2009/11/238 users
  • Coq in a Hurry ではこの後 Inductive Types の話になりますが、難しすぎてついてゆけないのでInteractive Theorem Proving and Program Development (Coq'Art) isbn:3540208542という本を読んでゆきます。この本は重くて固くて取っ付きにくいですが、基本的な事から順番に書いてあるので、他のチュートリアルより 続きを読む

    Coq で遊ぶその4: Coq の変な所色々。簡約。宣言と定義。型。 - 言語ゲー...propella2009/02/155 users

「Interactive Theorem Proving and Program Developmen...」が好きな人は、こんな商品も購入しています

他の商品を探す