Interactive theorem proving and program development : Coq'Art : the calculus of inductive constructions

著者

• Bertot, Yves
• Castéran, P. (Pierre)
• Huet, Gérard
• Paulin-Mohring, Christine

書誌事項

Interactive theorem proving and program development : Coq'Art : the calculus of inductive constructions

Yves Bertot, Pierre Castèran ; foreword by Gérard Huet and Christine Paulin-Mohring

Springer , [Amazon] [manufacture], c2010

• : pbk

タイトル別名

Texts in theoretical computer science : an EATCS series

注記

Reprint. Originally published: Springer, c2010 (Texts in theoretical computer science : an EATCS series)

"Printed in Japan 落丁、乱丁本のお問い合わせは Amazon.co.jp カスタマーサービスへ"--Last page (p. [478])

Bibliography: p. [453]-457

Includes indexes

詳細情報

• NII書誌ID(NCID): BC13857923
• ISBN:
  • 9783642058806
• 出版国コード: gw
• タイトル言語コード: eng
• 本文言語コード: eng
• 出版地: Berlin ; Heidelberg,[Japan]
• ページ数/冊数: xxv, 469 p.
• 大きさ: 23 cm
• 分類:
  • LCC : QA76.9.A96
  • DC22 : 511.3
• 件名:
  • LCSH : Automatic theorem proving
  • LCSH : Logic, Symbolic and mathematical