Interactive theorem proving and program development
Subtitle: Coq'Art : the calculus of inductive constructions
By: Yves Bertot, Pierre Castéran ; foreword by Gérard Huet and Christine Paulin-Mohring.
Contributors: Castéran, P.
Series: Texts in theoretical computer science
Publisher: Springer
Published: 2004
Place of publication: Berlin; New York
Language: eng
Number of pages: 469
Subjects: Automatic theorem proving; Computer programming
Notes: Includes bibliographical references (p. [453]-457) and index.