Certified Programming with Dependent Types
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.
Table of contents
-
Introduction
-
Some Quick Examples
-
Introducing Inductive Types
-
Inductive Predicates
-
Infinite Data and Proofs
-
Subset Types and Variations
-
General Recursion
-
More Dependent Types
-
Dependent Data Structures
-
Reasoning About Equality Proofs
-
Generic Programming
-
Universes and Axioms
-
Proof Search by Logic Programming
-
Proof Search in Ltac
-
Proof by Reflection
-
Proving in the Large
-
A Taste of Reasoning About Programming Language Syntax
| Pages : | 368 |
| Size : | 4.3 MB |
| File type : | |
| Downloads: | 61 |
| Created: | 2022-02-01 |
| License: | CC BY-NC-ND |
| Author(s): | by Adam Chlipala |
Others Programming Tutorials
Effective AWK Programming, 5th Edition
Programming Computer Vision with Python
Principles of Programming Languages
Certified Programming with Dependent Types
Is Parallel Programming Hard, And, If So, What Can You Do About It?
Others related eBooks about Certified Programming with Dependent Types
Think DSP: Digital Signal Processing in PythonThis book is an introduction to signal processing and system analysis using a computational approach, using Python as the programming language. The premise of this book (like the others in the Think X series) is that if you know how to program, you can use that skill to learn other things. By the ...
COBOL in 21 daysThis tutorial present an easy way to learn COBOL in a few days,free training courses in PDF for beginners and intermediate level users....
How to Make Mistakes in PythonDownload free course How to Make Mistakes in Python, pdf file on 82 pages by Mike Pirnat....
Introduction to Spring MVCThis pdf tutorial is a step-by-step guide on how to develop a web application from scratch using the Spring Framework.Free training course material under 68 pages by Thomas Risberg, Rick Evans and Portia Tung....
Visual Basic .NET Programming TutorialDownload free Visual Basic tutorial course in PDF, training file in 51 chapters and 149 pages. Free unaffiliated ebook created from Stack OverFlow contributor....
A Practical Introduction to Python ProgrammingThis book is for anyone who wants to understand Python programming. It is degigned as partly a tutorial and partly a reference of Python....
Prolog tutorial in PDFDownload free Prolog tutorial course in PDF, training file in 17 chapters and 51 pages. Free unaffiliated ebook created from Stack OverFlow contributor....
Essential C++This book written to provide clear and concise explanation of topics for programmers both starting to learn the C++ programming language as well as those diving in more complex topics. Most examples are linked to online playground that allows you to change the code and re-run it....
Learning .NET EPPlusDownload free course Learning .NET EPPlus, pdf file on 39 pages by Stack Overflow Community....
Android™ Notes for ProfessionalsThe fast-growing popularity of Android smartphones and tablets creates a huge opportunities for developers. If you're an experienced developer, you can start creating robust mobile Android apps right away with this professional guide....