书名: 交互式定理证明与程序开发 : Coq归纳构造演算的艺术= Interactive theorem proving and program development : coq'art: the calculus of inductive constructions

ISBN: 978-7-302-20813-6

作 者: Yves Bertot, Pierre Casteran著 ; 顾明等译

出版社: 清华大学出版社

出版日期: 2010