当前位置：
首页
>
出版信息
>
详细信息
快速检索
数据库：
各中心已购纸本教材
各中心已购电子教材
国内高校课程
国外著名大学课程
外文原版教材出版信息
外文影印版教材出版信息
名校购书信息
关键词：
Interactive Theorem Proving and Program Development
- Coq'art: The Calculus of Inductive Constructions
书目信息
ISBN：
9783540208549（13位）
中图分类号：
TP3
杜威分类号：
中文译名：
交互式定理证明与程序开发：Cog 艺术：归纳结构微积分
作者：
Y. Bertot
编者：
语种：
English
出版信息
出版社：
Springer
出版地：
出版年：
2004
版本：
版本类型：
原版
丛书题名：
卷期：
文献信息
关键词：
Computer Science
前言：
摘要：
内容简介：
Coq is an interactive proof assistant for the development of mathematical theories and formally certified software. It is based on a theory called the calculus of inductive constructions, a variant of type theory. This book provides a pragmatic introduc tion to the development of proofs and certified programs using Coq. With its large collection of examples and exercises it is an invaluable tool for researchers, students, and engineers interested in formal methods and the development of zero-fault softw
目次：
附录：
全文链接：
读者对象：
Grad. textbook
实体信息
页码：
500
装帧：
Hard
尺寸：
其它形态细节：
其它信息
原价：
EUR
64.9500
原版ISBN：
其它ISBN：
图书特色：
书评：
扩展信息
Isbn：
3540208542
issue：
2006JC02
相关附件