| Description |
1 online resource (xii, 424 pages) |
| Bibliography |
Includes bibliographical references (pages 413-417) and index. |
| Note |
Online resource; title from PDF title page (IEEE Xplore, viewed April 21, 2014). |
| Summary |
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. |
| Contents |
: 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. |
| Local Note |
MIT Press DTL OA MIT Titles |
| Subject |
Coq (Electronic resource)
|
|
Automatic theorem proving -- Computer programs.
|
|
Computer programming.
|
|
Automatic theorem proving -- Computer programs.
(OCoLC)fst00822778
|
|
Computer programming. (OCoLC)fst00872390
|
|
Engineering & Applied Sciences.
|
|
Computer Science.
|
| Indexed Term |
COMPUTER SCIENCE/General |
|
COMPUTER SCIENCE/Programming Languages |
| Genre/Form |
Electronic books.
|
| Other Form: |
Print version: Chlipala, Adam, 1981- Certified programming with dependent types. Cambridge, MA : The MIT Press, [2013] 9780262026659 (DLC) 2013012837 (OCoLC)844774277 |
| ISBN |
9780262317863 (electronic book) |
|
0262317869 (electronic book) |
| Standard No. |
9780262317870 |
| ISBN |
9780262026659 (hardcover ; alkaline paper) |
|
9780262317870 |
|
0262026651 (hardcover ; alkaline paper) |
|
0262317877 |
|
