MARC状态：待编 文献类型：中文图书 浏览次数：9
- 题名/责任者:
- 交互式定理证明与程序开发:Coq归纳构造演算的艺术/Yves Bertot，Pierre Casteran著 顾明等译
- 出版发行项:
- 北京:清华大学出版社,2010
- ISBN及定价:
- 978-7-302-20813-6/CNY59.00
- 载体形态项:
- 19,432页;26cm
- 并列正题名:
- Interactive theorem proving and program development:Coq'art: the calculus of inductive constructions
- 其它题名:
- Coq归纳构造演算的艺术
- 个人责任者:
- (德) 伯托特 (Bertot, Yves) 著
- 个人责任者:
- (德) 卡斯特兰 (Casteran, Pierre) 著
- 个人次要责任者:
- 顾明 译
- 学科主题:
- 定理证明-软件工具-教材
- 中图法分类号:
- O141-39
- 一般附注:
- 国外经典教材?计算机科学与技术
- 版本附注:
- 由Springer-Verlag授权出版
- 提要文摘附注:
- 本书内容包括：类型和表达式、命题和证明、依赖积、常用逻辑、归纳数据类型、证明策略和自动化证明、归纳谓词、函数及其规范、实例分析、模块系统等。
全部MARC细节信息>>