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
|