Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions / Yves Bertot, Pierre Castéran

Auteur: Bertot, Yves (1964-) - AuteurCo-auteur: Castéran, Pierre - AuteurAuteur secondaire : Huet, Gérard (1947-) - Préfacier ; Paulin-Mohring, Christine (1962-) - PréfacierType de document: MonographieCollection: Texts in theoretical computer science, An EATCS seriesLangue: anglaisPays: AllemagneÉditeur: Berlin : Springer-Verlag, 2004Description: 1 vol. (XXV-469 p.) : couv. ill. en coul., ill. ; 25 cm ISBN: 3540208542 ; rel. Bibliographie: Bibliogr. p. [453]-457. Index. Sujets MSC: 68T15 Computer science -- Artificial intelligence -- Theorem proving (deduction, resolution, etc.)
03B15 Mathematical logic and foundations -- General logic -- Higher-order logic and type theory
03B35 Mathematical logic and foundations -- General logic -- Mechanization of proofs and logical operations
03B70 Mathematical logic and foundations -- General logic -- Logic in computer science
68N18 Computer science -- Software -- Functional programming and lambda calculus
Location Call Number Status Date Due
Salle R 02977-01 / 68 BER (Browse Shelf) Available

Bibliogr. p. [453]-457. Index

There are no comments for this item.

Log in to your account to post a comment.
Languages: English | Français | |