机读格式显示(MARC)

• 000 01377nam0 2200313 450

• 001 0000804612

• 000 559941

• 005 20100328105800.0

• 010 __ |a 978-7-302-20813-6 |d CNY59.00

• 100 __ |a 20091229d2010 em y0chiy0110 ea

• 101 1_ |a chi |c ger

• 102 __ |a CN |b 110000

• 105 __ |a y z 000yy

• 106 __ |a r

• 200 1_ |a 交互式定理证明与程序开发 |9 jiao hu shi ding li zheng ming yu cheng xu kai fa |e Coq归纳构造演算的艺术 |d Interactive theorem proving and program development |e Coq'art: the calculus of inductive constructions |f Yves Bertot，Pierre Casteran著 |g 顾明等译 |z eng

• 210 __ |a 北京 |c 清华大学出版社 |d 2010

• 215 __ |a 19,432页 |d 26cm

• 300 __ |a 国外经典教材?计算机科学与技术

• 305 __ |a 由Springer-Verlag授权出版

• 330 __ |a 本书内容包括：类型和表达式、命题和证明、依赖积、常用逻辑、归纳数据类型、证明策略和自动化证明、归纳谓词、函数及其规范、实例分析、模块系统等。

• 510 1_ |a Interactive theorem proving and program development |e Coq'art: the calculus of inductive constructions |z eng

• 517 1_ |a Coq归纳构造演算的艺术 |9 Coq gui na gou zao yan suan de yi shu

• 606 0_ |a 定理证明 |x 软件工具 |j 教材

• 690 __ |a O141-39 |v 4

• 701 _0 |c (德) |a 伯托特 |9 bai tuo te |c (Bertot, Yves) |4 著

• 701 _0 |c (德) |a 卡斯特兰 |9 ka si te lan |c (Casteran, Pierre) |4 著

• 702 _0 |a 顾明 |9 gu ming |4 译

• 801 _0 |a CN |b NLIC |c 20100328

• 905 __ |a NLIC |d O141-39/1