000			nam a22 7a 4500
999			_c28337 _d28337
008			170601b xxu||||| |||| 00| 0 eng d
020			_a9783540208549
082			_a004.015113 _bBER
100			_aBertot, Yves
245			_aInteractive theorem proving and program development : Coq'Art - the calculus of inductive constructions
260			_aBerlin _bSpringer _c2004
300			_axxv, 469 p. _c25 cm.
365			_aEURO _b74.95
650			_aLogic
650			_aMathematical
650			_aData Type
650			_aAutomation
650			_aModule System
650			_aData Structure
650			_aSearch Pattern
700			_aCasteran, Pierre
942			_cBK