Bertot,, Yves
Interactive theorem proving and program development : Coq'Art - the calculus of inductive constructions / Yves Bertot, Pierre Castéran ; foreword by Gérard Huet and Christine Paulin-Mohring
Interactive theorem proving and program development : Coq'Art - the calculus of inductive constructions / Yves Bertot, Pierre Castéran ; foreword by Gérard Huet and Christine Paulin-Mohring
. - Berlin : Springer, cop. 2004
. - XV, 469 p. 24 cm
. - (Texts in theoretical computer science)
3-540-20854-2 Encadernado
519.6