HOME > Detail View

Detail View

Interactive theorem proving and program development : Coq'Art : the calculus of inductive constructions

Interactive theorem proving and program development : Coq'Art : the calculus of inductive constructions (Loan 7 times)

Material type
단행본
Personal Author
Bertot, Yves. Casteran, P. (Pierre)
Title Statement
Interactive theorem proving and program development : Coq'Art : the calculus of inductive constructions / Yves Bertot, Pierre Casteran ; foreword by Gerard Huet and Christine Paulin-Mohring.
Publication, Distribution, etc
Berlin ;   New York :   Springer ,   c2004.  
Physical Medium
xxv, 469 p. : ill. ; 25 cm.
Series Statement
Texts in theoretical computer science
ISBN
3540208542 (hd. bd.) 9783540208549
Bibliography, Etc. Note
Includes bibliographical references (p. [453]-457) and index.
Subject Added Entry-Topical Term
Automatic theorem proving. Computer programming.
000 01182camuu22003137a 4500
001 000045335418
005 20070313094237
008 040304s2004 gw a b 001 0 eng c
010 ▼a 2004103364
015 ▼a GBA4X5631 ▼2 bnb
020 ▼a 3540208542 (hd. bd.)
020 ▼a 9783540208549
035 ▼a (KERIS)REF000012152584
040 ▼a YUS ▼c YUS ▼d OHX ▼d AZS ▼d UKM ▼d OCLCQ ▼d DLC ▼d 211009
042 ▼a pcc
050 0 0 ▼a QA76.9.A96 ▼b B47 2004
082 0 0 ▼a 004/.015113 ▼2 22
090 ▼a 004.015113 ▼b B547i
100 1 ▼a Bertot, Yves.
245 1 0 ▼a Interactive theorem proving and program development : ▼b Coq'Art : the calculus of inductive constructions / ▼c Yves Bertot, Pierre Casteran ; foreword by Gerard Huet and Christine Paulin-Mohring.
260 ▼a Berlin ; ▼a New York : ▼b Springer , ▼c c2004.
300 ▼a xxv, 469 p. : ▼b ill. ; ▼c 25 cm.
440 0 ▼a Texts in theoretical computer science
504 ▼a Includes bibliographical references (p. [453]-457) and index.
650 0 ▼a Automatic theorem proving.
650 0 ▼a Computer programming.
700 1 ▼a Casteran, P. ▼q (Pierre)
945 ▼a KINS

Holdings Information

No. Location Call Number Accession No. Availability Due Date Make a Reservation Service
No. 1 Location Science & Engineering Library/Sci-Info(Stacks2)/ Call Number 004.015113 B547i Accession No. 121142514 Availability Available Due Date Make a Reservation Service B M

Contents information

Table of Contents

1 A Brief Overview.- 2 Types and Expressions.- 3 Propositions and Proofs.- 4 Dependent Products, or Pandora's Box.- 5 Everyday Logic.- 6 Inductive Data Types.- 7 Tactics and Automation.- 8 Inductive Predicates.- 9 Functions and Their Specifications.- 10 Extraction and Imperative Programming.- 11 A Case Study.- 12 The Module System.- 13 Infinite Objects and Proofs.- 14 Foundations of Inductive Types.- 15 General Recursion.- 16 Proof by Reflection.- Insertion Sort.- References.- Coq and Its Libraries.- Examples from the Book.


Information Provided By: : Aladin

New Arrivals Books in Related Fields

김종원 (2020)