An edition of Interactive Theorem Proving and Program Development
(2004)
Interactive Theorem Proving and Program Development
Coq'Art: The Calculus of Inductive Constructions
by Yves Bertot
Share
×Close
Coq is an interactive proof assistant for the development of mathematical theories and formally certified software. It is based on a theory called the calculus of inductive constructions, a variant of type theory. This book provides a pragmatic introduction to the development of proofs and certified programs using Coq. With its large collection of examples and exercises it is an invaluable tool for researchers, students, and engineers interested in formal methods and the development of zero-fault software.
Check nearby libraries
Buy this book
| Edition | Availability |
|---|---|
1
Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions
2004, Springer Berlin Heidelberg
electronic resource :
in English
3642058809 9783642058806
|
aaaa
|
Book Details
Table of Contents
A Brief Overview
Types and Expressions
Propositions and Proofs
Dependent Products
Everyday Logic
Inductive Data Types
Tactics and Automation
Inductive Predicates
Functions and Their Specifications
Extraction and Imperative Programming
A Case Study
The Module System
Infinite Objects and Proofs
Foundations of Inductive Types
General Recursion
Proof by Reflection
Appendix
Index.
Edition Notes
Online full text is restricted to subscribers.
Also available in print.
Mode of access: World Wide Web.
Classifications
The Physical Object
Edition Identifiers
Work Identifiers
Source records
Community Reviews (0)
Lists
| February 26, 2022 | Edited by ImportBot | import existing book |
| July 1, 2019 | Created by MARC Bot | import new book |