题名	责任者	出版社	索书号
交互式定理证明与程序开发:Coq归纳构造演算的艺术:Coq'art: the calculus of inductive constructions	Yves Bertot，Pierre Casteran著	清华大学出版社	O141/26