Coverart for item
The Resource Certified programming with dependent types : a pragmatic introduction to the Coq proof assistant, Adam Chlipala, (electronic book)

Certified programming with dependent types : a pragmatic introduction to the Coq proof assistant, Adam Chlipala, (electronic book)

Label
Certified programming with dependent types : a pragmatic introduction to the Coq proof assistant
Title
Certified programming with dependent types
Title remainder
a pragmatic introduction to the Coq proof assistant
Statement of responsibility
Adam Chlipala
Creator
Subject
Language
eng
Member of
Cataloging source
COO
http://library.link/vocab/creatorDate
1981-
http://library.link/vocab/creatorName
Chlipala, Adam
Dewey number
005.1
Index
index present
LC call number
QA76.9.A96
Literary form
non fiction
Nature of contents
  • dictionaries
  • bibliography
http://library.link/vocab/subjectName
  • Automatic theorem proving
  • Computer programming
Label
Certified programming with dependent types : a pragmatic introduction to the Coq proof assistant, Adam Chlipala, (electronic book)
Instantiates
Publication
Bibliography note
Includes bibliographical references (pages [413]-417) and index
Contents
Machine generated contents note: 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
Control code
IEEEMIT872996245
Extent
1 online resource (xii, 424 pages)
Form of item
online
Isbn
9780262317870
Reproduction note
Electronic resource.
Specific material designation
remote
System control number
ocn872996245
Label
Certified programming with dependent types : a pragmatic introduction to the Coq proof assistant, Adam Chlipala, (electronic book)
Publication
Bibliography note
Includes bibliographical references (pages [413]-417) and index
Contents
Machine generated contents note: 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
Control code
IEEEMIT872996245
Extent
1 online resource (xii, 424 pages)
Form of item
online
Isbn
9780262317870
Reproduction note
Electronic resource.
Specific material designation
remote
System control number
ocn872996245

Library Locations

Processing Feedback ...