机读格式显示(MARC)

• 000 01620nam2 2200385 4500

• 000 0000230801

• 001 0000152298

• 005 20110103162948.0

• 009 012009142104

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

• 035 __ |a (SG02)012007198777

• 100 __ |a 20110103d2010 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 教材 |A dinglizhengming

• 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 SG02 |c 20091229

• 801 _2 |a CN |b 261060 |c 20110103

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

• 991 __012010008058

• 995 __ |a 261060 |f O141-39/1

• 999 __ |t C |A zw |a 20110103 16:29:15 |I zw |i 20110103 16:29:4