Skip to content
You are not logged in |Login  

LEADER 00000cam  2200613Ki 4500 
001    ocn872996245 
003    OCoLC 
005    20200419060618.2 
006    m     o  d         
007    cr ||||||||||| 
008    140309s2013    mau     ob    001 0 eng d 
019    881288988 
020    9780262317863|q(electronic book) 
020    0262317869|q(electronic book) 
020    |z9780262026659|q(hardcover ;|qalkaline paper) 
020    9780262317870 
020    |z0262026651|q(hardcover ;|qalkaline paper) 
020    0262317877 
024 3  9780262317870 
035    (OCoLC)872996245|z(OCoLC)881288988 
037    9153|bMIT Press 
037    9780262317870|bMIT Press 
040    COO|beng|epn|cCOO|dCUS|dIEEEE|dOCLCF|dCEF|dMERER|dVTS
       |dOCLCQ|dAU@|dMITPR|dYOU|dLEAUB|dEBLCP 
049    STJJ 
050  4 QA76.9.A96 
082 04 005.1|223 
100 1  Chlipala, Adam,|d1981- 
245 10 Certified programming with dependent types :|ba pragmatic 
       introduction to the Coq proof assistant /|cAdam Chlipala. 
264  1 Cambridge, MA :|bThe MIT Press,|c[2013] 
264  4 |c©2013 
300    1 online resource (xii, 424 pages) 
336    text|btxt|2rdacontent 
337    computer|bc|2rdamedia 
338    online resource|bcr|2rdacarrier 
504    Includes bibliographical references (pages 413-417) and 
       index. 
505 0  : 1. Introduction -- 1.1. Whence This Book? -- 1.2. Why 
       Coq? -- 1.2.1. Based on a Higher-Order Functional 
       Programming Language -- 1.2.2. Dependent Types -- 1.2.3. 
       An Easy-to-Check Kernel Proof Language -- 1.2.4. 
       Convenient Programmable Proof Automation -- 1.2.5. Proof 
       by Reflection -- 1.3. Why Not a Different Dependently 
       Typed Language? -- 1.4. Engineering with a Proof Assistant
       -- 1.5. Prerequisites -- 1.6. Using This Book -- 1.6.1. 
       Reading This Book -- 1.6.2. The Tactic Library -- 1.6.3. 
       Installation and Emacs Setup -- 2. Some Quick Examples -- 
       2.1. Arithmetic Expressions over Natural Numbers -- 2.1.1.
       Source Language -- 2.1.2. Target Language -- 2.1.3. 
       Translation -- 2.1.4. Translation Correctness -- 2.2. 
       Typed Expressions -- 2.2.1. Source Language -- 2.2.2. 
       Target Language -- 2.2.3. Translation -- 2.2.4. 
       Translation Correctness -- I. Basic Programming and 
       Proving -- 3. Introducing Inductive Types -- 3.1. Proof 
       Terms -- 3.2. Enumerations -- 3.3. Simple Recursive Types 
       -- 3.4. Parameterized Types -- 3.5. Mutually Inductive 
       Types -- 3.6. Reflexive Types -- 3.7. An Interlude on 
       Induction Principles -- 3.8. Nested Inductive Types -- 
       3.9. Manual Proofs about Constructors -- 4. Inductive 
       Predicates -- 4.1. Propositional Logic -- 4.2. What Does 
       It Mean to Be Constructive? -- 4.3. First-Order Logic -- 
       4.4. Predicates with Implicit Equality -- 4.5. Recursive 
       Predicates -- 5. Infinite Data and Proofs -- 5.1.Computing
       with Infinite Data -- 5.2. Infinite Proofs -- 5.3. Simple 
       Modeling of Nonterminating Programs -- II. Programming 
       with Dependent Types -- 6. Subset Types and Variations -- 
       6.1. Introducing Subset Types -- 6.2. Decidable 
       Proposition Types -- 6.3. Partial Subset Types -- 6.4. 
       Monadic Notations -- 6.5.A Type-Checking Example -- 7. 
       General Recursion -- 7.1. Well-Founded Recursion -- 7.2.A 
       Nontermination Monad Inspired by Domain Theory -- 7.3. Co-
       inductive Nontermination Monads -- 7.4.Comparing the 
       Alternatives -- 8. More Dependent Types -- 8.1. Length-
       Indexed Lists -- 8.2. The One Rule of Dependent Pattern 
       Matching in Coq -- 8.3.A Tagless Interpreter -- 8.4. 
       Dependently Typed Red-Black Trees -- 8.5.A Certified 
       Regular Expression Matcher -- 9. Dependent Data Structures
       -- 9.1. More Length-Indexed Lists -- 9.2. Heterogeneous 
       Lists -- 9.2.1.A Lambda Calculus Interpreter -- 9.3. 
       Recursive Type Definitions -- 9.4. Data Structures as 
       Index Functions -- 9.4.1. Another Interpreter Example -- 
       9.5. Choosing between Representations -- 10. Reasoning 
       about Equality Proofs -- 10.1. The Definitional Equality -
       - 10.2. Heterogeneous Lists Revisited -- 10.3. Type Casts 
       in Theorem Statements -- 10.4. Heterogeneous Equality -- 
       10.5. Equivalence of Equality Axioms -- 10.6. Equality of 
       Functions -- 11. Generic Programming -- 11.1. Reifying 
       Datatype Definitions -- 11.2. Recursive Definitions -- 
       11.2.1. Pretty-Printing -- 11.2.2. Mapping -- 11.3. 
       Proving Theorems about Recursive Definitions -- 12. 
       Universes and Axioms -- 12.1. The Type Hierarchy -- 
       12.1.1. Inductive Definitions -- 12.1.2. Deciphering 
       Baffling Messages about Inability to Unify -- 12.2. The 
       Prop Universe -- 12.3. Axioms -- 12.3.1. The Basics -- 
       12.3.2. Axioms of Choice -- 12.3.3. Axioms and Computation
       -- 12.3.4. Methods for Avoiding Axioms -- III. Proof 
       Engineering -- 13. Proof Search by Logic Programming -- 
       13.1. Introducing Logic Programming -- 13.2. Searching for
       Underconstrained Values -- 13.3. Synthesizing Programs -- 
       13.4. More on auto Hints -- 13.5. Rewrite Hints -- 14. 
       Proof Search in Ltac -- 14.1. Some Built-in Automation 
       Tactics -- 14.2. Ltac Programming Basics -- 14.3. 
       Functional Programming in Ltac -- 14.4. Recursive Proof 
       Search -- 14.5. Creating Unification Variables -- 15. 
       Proof by Reflection -- 15.1. Proving Evenness -- 15.2. 
       Reifying the Syntax of a Trivial Tautology Language -- 
       15.3.A Monoid Expression Simplifier -- 15.4.A Smarter 
       Tautology Solver -- 15.4.1. Manual Reification of Terms 
       with Variables -- 15.5. Building a Reification Tactic That
       Recurses under Binders -- IV. The Big Picture -- 16. 
       Proving in the Large -- 16.1. Ltac Antipatterns -- 16.2. 
       Debugging and Maintaining Automation -- 16.3. Modules -- 
       16.4. Build Processes -- 17. Reasoning about Programming 
       Language Syntax -- 17.1. Dependent de Bruijn Indices -- 
       17.2. Parametric Higher-Order Abstract Syntax -- 17.2.1. 
       Functional Programming with PHOAS -- 17.2.2. Verifying 
       Program Transformations -- 17.2.3. Establishing Term Well-
       Formedness -- 17.2.4.A Few Additional Remarks. 
520 8  The technology of mechanized program verification can play
       a supporting role in many kinds of research projects in 
       computer science, and related tools for formal proof-
       checking are seeing increasing adoption in mathematics and
       engineering. This book provides an introduction to the Coq
       software for writing and checking mathematical proofs. It 
       takes a practical engineering focus throughout, 
       emphasizing techniques that will help users to build, 
       understand, and maintain large Coq developments and 
       minimize the cost of code change over time. Two topics, 
       rarely discussed elsewhere, are covered in detail: 
       effective dependently typed programming (making productive
       use of a feature at the heart of the Coq system) and 
       construction of domain-specific proof tactics. Almost 
       every subject covered is also relevant to interactive 
       computer theorem proving in general, not just program 
       verification, demonstrated through examples of verified 
       programs applied in many different sorts of 
       formalizations. The book develops a unique automated proof
       style and applies it throughout; even experienced Coq 
       users may benefit from reading about basic Coq concepts 
       from this novel perspective. The book also offers a 
       library of tactics, or programs that find proofs, designed
       for use with examples in the book. Readers will acquire 
       the necessary skills to reimplement these tactics in other
       settings by the end of the book. All of the code appearing
       in the book is freely available online. 
588 0  Online resource; title from PDF title page (IEEE Xplore, 
       viewed April 21, 2014). 
590    MIT Press|bDTL OA MIT Titles 
630 00 Coq (Electronic resource) 
650  0 Automatic theorem proving|xComputer programs. 
650  0 Computer programming. 
650  7 Automatic theorem proving|xComputer programs.|2fast
       |0(OCoLC)fst00822778 
650  7 Computer programming.|2fast|0(OCoLC)fst00872390 
650  7 Engineering & Applied Sciences.|2hilcc 
650  7 Computer Science.|2hilcc 
653  0 COMPUTER SCIENCE/General 
653  0 COMPUTER SCIENCE/Programming Languages 
655  0 Electronic books. 
776 08 |iPrint version:|aChlipala, Adam, 1981-|tCertified 
       programming with dependent types.|dCambridge, MA : The MIT
       Press, [2013]|z9780262026659|w(DLC)  2013012837
       |w(OCoLC)844774277 
914    ocn872996245 
994    92|bSTJ 
Location Call No. Status
 University of Saint Joseph: Pope Pius XII Library - Internet  WORLD WIDE WEB E-BOOK MIT    Downloadable
Please click here to access this MIT resource