Programming Books

6 Excellent Free Books to Learn Coq

Last Updated on May 22, 2022

Coq is a dependently typed language. This means that the types of the language may depend on the values of variables. In this respect, it is similar to other related languages such as Agda, Idris, F*, Lean, and others. Via the Curry-Howard correspondence, programs, properties and proofs are formalized in the same language.

Coq is developed in OCaml and shares some syntactic and conceptual similarity with it. Coq is a language containing many fascinating but difficult topics.

Here’s our recommended free books to learn Coq.


1. Reference Manual by the Coq development team

Coq Reference ManualThis is the reference manual of Coq. Coq is an interactive theorem prover. It lets you formalize mathematical concepts and then helps you interactively generate machine-checked proofs of theorems.

Machine checking gives users much more confidence that the proofs are correct compared to human-generated and -checked proofs.

Read the manual


2. Software Foundations by Various Authors

Software Foundations: Volume 1 - Logical FoundationsThe Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software.

The principal novelty of the series is that every detail is one hundred percent formalized and machine-checked: the entire text of each volume, including the exercises, is literally a “proof script” for the Coq proof assistant.

The exposition is intended for a broad range of readers, from advanced undergraduates to PhD students and researchers. No specific background in logic or programming languages is assumed, though a degree of mathematical maturity is helpful. A one-semester course can expect to cover Logical Foundations plus most of Programming Language Foundations or Verified Functional Algorithms, or selections from both.

There are 4 volumes:

  • Volume 1 – Logical Foundations is the entry-point to the series. It covers functional programming, basic concepts of logic, computer-assisted theorem proving, and Coq.
  • Volume 2 – Programming Language Foundations surveys the theory of programming languages, including operational semantics, Hoare logic, and static type systems.
  • Volume 3 – Verified Functional Algorithms shows how a variety of fundamental data structures can be specified and mechanically verified.
  • Volume 4 – QuickChick: Property-Based Testing in Coq introduces tools for combining randomized property-based testing with formal specification and proof in the Coq ecosystem.

Read the books


3. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant by Adam Chlipala

Certified Programming with Dependent Types

This book is about certified programming using Coq.

This concept of certification, a standard one in the programming languages and formal methods communities, has to do with the idea of a certificate, or formal mathematical artifact proving that a program meets its specification.

This book is licensed under a Creative Commons Attribution-Noncommercial-NoDerivative Works 3.0 Unported License.

Read the book


Next page: Page 2 – Mathematical Components and more books

Pages in this article:
Page 1 – Reference Manual
Page 2 – Mathematical Components and more books


All books in this series:

Free Programming Books
AdaALGOL-like programming language, extended from Pascal and other languages
AgdaDependently typed functional language based on intuitionistic Type Theory
ArduinoInexpensive, flexible, open source microcontroller platform
AssemblyAs close to writing machine code without writing in pure hexadecimal
AwkVersatile language designed for pattern scanning and processing language
BashShell and command language; popular both as a shell and a scripting language
BASICBeginner’s All-purpose Symbolic Instruction Code
CGeneral-purpose, procedural, portable, high-level language
C++General-purpose, portable, free-form, multi-paradigm language
C#Combines the power and flexibility of C++ with the simplicity of Visual Basic
ClojureDialect of the Lisp programming language
ClojureScriptCompiler for Clojure that targets JavaScript
COBOLCommon Business-Oriented Language
CoffeeScriptTranscompiles into JavaScript inspired by Ruby, Python and Haskell
CoqDependently typed language similar to Agda, Idris, F* and others
CrystalGeneral-purpose, concurrent, multi-paradigm, object-oriented language
CSSCSS (Cascading Style Sheets) specifies a web page’s appearance
DGeneral-purpose systems programming language with a C-like syntax
DartClient-optimized language for fast apps on multiple platforms
DylanMulti-paradigm language supporting functional and object-oriented coding
ECMAScriptBest known as the language embedded in web browsers
EiffelObject-oriented language designed by Bertrand Meyer
ElixirRelatively new functional language running on the Erlang virtual machine
ErlangGeneral-purpose, concurrent, declarative, functional language
F#Uses functional, imperative, and object-oriented programming methods
FactorDynamic stack-based programming language
ForthImperative stack-based programming language
FortranThe first high-level language, using the first compiler
GoCompiled, statically typed programming language
GroovyPowerful, optionally typed and dynamic language
HaskellStandardized, general-purpose, polymorphically, statically typed language
HTMLHyperText Markup Language
IconWide variety of features for processing and presenting symbolic data
JArray programming language based primarily on APL
JavaGeneral-purpose, concurrent, class-based, object-oriented, high-level language
JavaScriptInterpreted, prototype-based, scripting language
JuliaHigh-level, high-performance language for technical computing
KotlinMore modern version of Java
LabVIEWDesigned to enable domain experts to build power systems quickly
LaTeXProfessional document preparation system and document markup language
LispUnique features - excellent to study programming constructs
LogoDialect of Lisp that features interactivity, modularity, extensibility
LuaDesigned as an embeddable scripting language
MarkdownPlain text formatting syntax designed to be easy-to-read and easy-to-write
Objective-CObject-oriented language that adds Smalltalk-style messaging to C
OCamlThe main implementation of the Caml language
PascalImperative and procedural language designed in the late 1960s
PerlHigh-level, general-purpose, interpreted, scripting, dynamic language
PHPPHP has been at the helm of the web for many years
PostScriptInterpreted, stack-based and Turing complete language
PrologA general purpose, declarative, logic programming language
PureScriptSmall strongly, statically typed language compiling to JavaScript
PythonGeneral-purpose, structured, powerful language
QMLHierarchical declarative language for user interface layout - JSON-like syntax
RDe facto standard among statisticians and data analysts
RacketGeneral-purpose, object-oriented, multi-paradigm, functional language
RakuMember of the Perl family of programming languages
RubyGeneral purpose, scripting, structured, flexible, fully object-oriented language
RustIdeal for systems, embedded, and other performance critical code
ScalaModern, object-functional, multi-paradigm, Java-based language
SchemeA general-purpose, functional language descended from Lisp and Algol
ScratchVisual programming language designed for 8-16 year-old children
SQLAccess and manipulate data held in a relational database management system
Standard MLGeneral-purpose functional language characterized as "Lisp with types"
SwiftPowerful and intuitive general-purpose programming language
TclDynamic language based on concepts of Lisp, C, and Unix shells
TeXMarkup and programming language - create professional quality typeset text
TypeScriptStrict syntactical superset of JavaScript adding optional static typing
ValaObject-oriented language, syntactically similar to C#
VHDLHardware description language used in electronic design automation
VimLPowerful scripting language of the Vim editor
XMLRules for defining semantic tags describing structure ad meaning
Subscribe
Notify of
guest

This site uses Akismet to reduce spam. Learn how your comment data is processed.

0 Comments
Inline Feedbacks
View all comments