Certified programming with dependent types / Adam Chlipala

Public ISBD Titre : Certified programming with dependent types : a pragmatic introduction to the Coq proof assistant Type de document : texte imprimé Auteurs : Adam Chlipala (1981-....), Auteur Editeur : Cambridge (Mass.) : The MIT Press Année de publication : cop. 2013 Importance : 1 vol. (XII-424 p.) Présentation : couv. ill. en coul. Format : 24 cm ISBN/ISSN/EAN : 978-0-262-02665-9 Langues : Anglais Catégories : 68-XX Computer science :68-02 Research exposition (monographs, survey articles) 68-XX Computer science :68TXX Artificial intelligence:68T15 Theorem proving (deduction, resolution, etc.) Mots-clés : computer science  Coq Index. décimale : 68C Monographie Certified programming with dependent types : a pragmatic introduction to the Coq proof assistant [texte imprimé] / Adam Chlipala (1981-....), Auteur . - Cambridge (Mass.) : The MIT Press, cop. 2013 . - 1 vol. (XII-424 p.) : couv. ill. en coul. ; 24 cm. ISBN : 978-0-262-02665-9 Langues : Anglais Catégories : 68-XX Computer science :68-02 Research exposition (monographs, survey articles) 68-XX Computer science :68TXX Artificial intelligence:68T15 Theorem proving (deduction, resolution, etc.) Mots-clés : computer science  Coq Index. décimale : 68C Monographie

Exemplaires

Code-barres	Cote	Support	Localisation	Section	Disponibilité
21812	68C448	imprimé / autre	CRDM	68/INFORMATIQUE	Disponible

Handbook of practical logic and automated reasoning / John Harrison

Public ISBD Titre : Handbook of practical logic and automated reasoning Type de document : texte imprimé Auteurs : John Harrison, Auteur Editeur : Cambridge University Press Année de publication : 2009 Importance : xix - 681 p. ISBN/ISSN/EAN : 978-0-521-89957-4 Langues : Anglais Catégories : 03-XX Mathematical logic and foundations:03-00 General reference works (handbooks, dictionaries, bibliographies, etc.) 03-XX Mathematical logic and foundations:03BXX General logic:03B35 Mechanization of proofs and logical operations 68-XX Computer science :68-00 General reference works (handbooks, dictionaries, bibliographies, etc.) 68-XX Computer science :68TXX Artificial intelligence:68T15 Theorem proving (deduction, resolution, etc.) Mots-clés : mathematical logic  automated reasoning  automated theorem proving Index. décimale : 03C Monographie Handbook of practical logic and automated reasoning [texte imprimé] / John Harrison, Auteur . - [S.l.] : Cambridge University Press, 2009 . - xix - 681 p. ISBN : 978-0-521-89957-4 Langues : Anglais Catégories : 03-XX Mathematical logic and foundations:03-00 General reference works (handbooks, dictionaries, bibliographies, etc.) 03-XX Mathematical logic and foundations:03BXX General logic:03B35 Mechanization of proofs and logical operations 68-XX Computer science :68-00 General reference works (handbooks, dictionaries, bibliographies, etc.) 68-XX Computer science :68TXX Artificial intelligence:68T15 Theorem proving (deduction, resolution, etc.) Mots-clés : mathematical logic  automated reasoning  automated theorem proving Index. décimale : 03C Monographie

Exemplaires

Code-barres	Cote	Support	Localisation	Section	Disponibilité
19580	03C178	imprimé / autre	CRDM	03/MATHEMATICAL LOGIC AND FOUNDATIONS	Disponible

Interactive theorem proving and program development / Bertot, Yves

Public ISBD Titre : Interactive theorem proving and program development : Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohrin Type de document : texte imprimé Auteurs : Bertot, Yves ; Castéran, Pierre Editeur : Springer-Verlag Année de publication : 2004 Collection : Texts in Theoretical Computer Science. An EATCS Series Importance : xxv - 469 p. ISBN/ISSN/EAN : 978-3-540-20854-9 Langues : Anglais Catégories : 03-XX Mathematical logic and foundations:03BXX General logic:03B15 Higher-order logic and type theory 03-XX Mathematical logic and foundations:03BXX General logic:03B35 Mechanization of proofs and logical operations 68-XX Computer science :68TXX Artificial intelligence:68T15 Theorem proving (deduction, resolution, etc.) Mots-clés : type theory  theorem proving  proof assistant  program verification  coq Index. décimale : 68C Monographie Interactive theorem proving and program development : Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohrin [texte imprimé] / Bertot, Yves ; Castéran, Pierre . - [S.l.] : Springer-Verlag, 2004 . - xxv - 469 p. . - (Texts in Theoretical Computer Science. An EATCS Series) . ISBN : 978-3-540-20854-9 Langues : Anglais Catégories : 03-XX Mathematical logic and foundations:03BXX General logic:03B15 Higher-order logic and type theory 03-XX Mathematical logic and foundations:03BXX General logic:03B35 Mechanization of proofs and logical operations 68-XX Computer science :68TXX Artificial intelligence:68T15 Theorem proving (deduction, resolution, etc.) Mots-clés : type theory  theorem proving  proof assistant  program verification  coq Index. décimale : 68C Monographie

Exemplaires

Code-barres	Cote	Support	Localisation	Section	Disponibilité
16714	68C305	imprimé / autre	CRDM	68/INFORMATIQUE	Disponible

Mechanical theorem proving in geometries / Wu, Wen-tsün

Public ISBD Titre : Mechanical theorem proving in geometries : basic principles Type de document : texte imprimé Auteurs : Wu, Wen-tsün ; Jin, Xiaofan ; Dongming Wang, Traducteur Editeur : Springer-Verlag Année de publication : 1994 Collection : texts and monographs in symbolic computation Importance : xii - 288 p. ISBN/ISSN/EAN : 978-3-211-82506-8 Langues : Anglais Catégories : 03-XX Mathematical logic and foundations:03-02 Research exposition (monographs, survey articles) 03-XX Mathematical logic and foundations:03BXX General logic:03B35 Mechanization of proofs and logical operations 68-XX Computer science :68TXX Artificial intelligence:68T15 Theorem proving (deduction, resolution, etc.) Mots-clés : symbolic computation  irreducible decomposition  algebraic varieties  constructive algebraic geometry  polynomial equality relations  geometry theorem proving  mechanization  coordinate systems  algebraization  axiomatic geometry  computational geometry Index. décimale : 68C Monographie Mechanical theorem proving in geometries : basic principles [texte imprimé] / Wu, Wen-tsün ; Jin, Xiaofan ; Dongming Wang, Traducteur . - [S.l.] : Springer-Verlag, 1994 . - xii - 288 p.. - (texts and monographs in symbolic computation) . ISBN : 978-3-211-82506-8 Langues : Anglais Catégories : 03-XX Mathematical logic and foundations:03-02 Research exposition (monographs, survey articles) 03-XX Mathematical logic and foundations:03BXX General logic:03B35 Mechanization of proofs and logical operations 68-XX Computer science :68TXX Artificial intelligence:68T15 Theorem proving (deduction, resolution, etc.) Mots-clés : symbolic computation  irreducible decomposition  algebraic varieties  constructive algebraic geometry  polynomial equality relations  geometry theorem proving  mechanization  coordinate systems  algebraization  axiomatic geometry  computational geometry Index. décimale : 68C Monographie

Exemplaires

Code-barres	Cote	Support	Localisation	Section	Disponibilité
11825	68C01	imprimé / autre	CRDM	68/INFORMATIQUE	Disponible

---

page 1/1