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