4 résultat(s) recherche sur le mot-clé 'type theory'

an Introduction to mathematical logic and type theory / P. B. Andrews

Public ISBD Titre : an Introduction to mathematical logic and type theory : to truth through proof Type de document : texte imprimé Auteurs : P. B. Andrews Mention d'édition : 2nd ed. Editeur : Springer-Verlag Année de publication : 2002 Collection : Applied Logic Series num. 27 Importance : xviii - 408 p. ISBN/ISSN/EAN : 978-1-4020-0763-7 Note générale : commande M. Borer Langues : Anglais Catégories : 03-XX Mathematical logic and foundations:03-01 Instructional exposition (textbooks, tutorial papers, etc.) 03-XX Mathematical logic and foundations:03BXX General logic:03B10 Classical first-order logic 03-XX Mathematical logic and foundations:03BXX General logic:03B15 Higher-order logic and type theory Mots-clés : propositional logic  type theory  first-order logic Index. décimale : 03C Monographie an Introduction to mathematical logic and type theory : to truth through proof [texte imprimé] / P. B. Andrews  . -  2nd ed. . - [S.l.] : Springer-Verlag, 2002 . - xviii - 408 p.. - (Applied Logic Series; 27) . ISBN : 978-1-4020-0763-7 commande M. Borer Langues : Anglais Catégories : 03-XX Mathematical logic and foundations:03-01 Instructional exposition (textbooks, tutorial papers, etc.) 03-XX Mathematical logic and foundations:03BXX General logic:03B10 Classical first-order logic 03-XX Mathematical logic and foundations:03BXX General logic:03B15 Higher-order logic and type theory Mots-clés : propositional logic  type theory  first-order logic Index. décimale : 03C Monographie

Exemplaires

Code-barres	Cote	Support	Localisation	Section	Disponibilité
17760	03C167	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

Basic proof theory / Troelstra, A.

Public ISBD Titre : Basic proof theory Type de document : texte imprimé Auteurs : Troelstra, A. ; Schwichtenberg, H. Mention d'édition : 2nd ed. Editeur : Cambridge : Cambridge University Press Année de publication : 2000 Collection : Cambridge Tracts in Computer Sciences num. 43 Importance : xii - 417 p. ISBN/ISSN/EAN : 978-0-521-77911-1 Langues : Anglais Catégories : 03-XX Mathematical logic and foundations:03-01 Instructional exposition (textbooks, tutorial papers, etc.) 03-XX Mathematical logic and foundations:03-02 Research exposition (monographs, survey articles) 03-XX Mathematical logic and foundations:03BXX General logic:03B40 Combinatory logic and lambda-calculus 03-XX Mathematical logic and foundations:03BXX General logic:03B45 Modal logic 03-XX Mathematical logic and foundations:03BXX General logic:03B70 Logic in computer science 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F03 Proof theory, general 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F05 Cut-elimination and normal-form theorems 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F30 First-order arithmetic and fragments 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F35 Second- and higher-order arithmetic and fragments 03-XX Mathematical logic and foundations:03GXX Algebraic logic:03G30 Categorical logic, topoi 68-XX Computer science :68NXX Software:68N17 Logic programming Mots-clés : apartness  e-logic  multi-succedent intuitionistic sequent calculus  kleene-style sequent calculus  logic programming  connections with computer science  first-order arithmetic  modal logic  hilbert-style system  resolution  second-order heyting arithmetic  linear logic  coherence theorem  categorical logic  formulas-as-types relation  combinatory logic  type theory  interpolation  strong normalization  cut elimination  gentzen type system  sequent calculus  natural deduction system  intuitionistic logic  classical logic  minimal logic  proof theory Index. décimale : 03C Monographie Basic proof theory [texte imprimé] / Troelstra, A. ; Schwichtenberg, H.  . -  2nd ed. . - Cambridge : Cambridge University Press, 2000 . - xii - 417 p.. - (Cambridge Tracts in Computer Sciences; 43) . ISBN : 978-0-521-77911-1 Langues : Anglais Catégories : 03-XX Mathematical logic and foundations:03-01 Instructional exposition (textbooks, tutorial papers, etc.) 03-XX Mathematical logic and foundations:03-02 Research exposition (monographs, survey articles) 03-XX Mathematical logic and foundations:03BXX General logic:03B40 Combinatory logic and lambda-calculus 03-XX Mathematical logic and foundations:03BXX General logic:03B45 Modal logic 03-XX Mathematical logic and foundations:03BXX General logic:03B70 Logic in computer science 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F03 Proof theory, general 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F05 Cut-elimination and normal-form theorems 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F30 First-order arithmetic and fragments 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F35 Second- and higher-order arithmetic and fragments 03-XX Mathematical logic and foundations:03GXX Algebraic logic:03G30 Categorical logic, topoi 68-XX Computer science :68NXX Software:68N17 Logic programming Mots-clés : apartness  e-logic  multi-succedent intuitionistic sequent calculus  kleene-style sequent calculus  logic programming  connections with computer science  first-order arithmetic  modal logic  hilbert-style system  resolution  second-order heyting arithmetic  linear logic  coherence theorem  categorical logic  formulas-as-types relation  combinatory logic  type theory  interpolation  strong normalization  cut elimination  gentzen type system  sequent calculus  natural deduction system  intuitionistic logic  classical logic  minimal logic  proof theory Index. décimale : 03C Monographie

Exemplaires

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

The evolution of Principia mathematica / Bernard Linsky

Public ISBD Titre : The evolution of Principia mathematica : Bertrand Russell's manuscripts and notes for the second edition Type de document : texte imprimé Auteurs : Bernard Linsky, Auteur Editeur : Cambridge (GB) : Cambridge University Press Année de publication : 2011 Importance : vii - 407 p. Format : 26 cm ISBN/ISSN/EAN : 978-1-107-00327-9 Langues : Anglais Catégories : 00-XX General:00AXX General and miscellaneous specific topics:00A30 Philosophy of mathematics 01-XX History and biography:01A60 20th century 03-XX Mathematical logic and foundations:03A05 Philosophical and critical Mots-clés : 20th century logic  type theory  ramified theory of types  Russell  Ramsey Index. décimale : 01C Histoire des Mathématiques The evolution of Principia mathematica : Bertrand Russell's manuscripts and notes for the second edition [texte imprimé] / Bernard Linsky, Auteur . - Cambridge (GB) : Cambridge University Press, 2011 . - vii - 407 p. ; 26 cm. ISBN : 978-1-107-00327-9 Langues : Anglais Catégories : 00-XX General:00AXX General and miscellaneous specific topics:00A30 Philosophy of mathematics 01-XX History and biography:01A60 20th century 03-XX Mathematical logic and foundations:03A05 Philosophical and critical Mots-clés : 20th century logic  type theory  ramified theory of types  Russell  Ramsey Index. décimale : 01C Histoire des Mathématiques

Exemplaires

Code-barres	Cote	Support	Localisation	Section	Disponibilité
20778	01C106	imprimé / autre	CRDM	01/HISTOIRE DES MATHEMATIQUES	Disponible