Programming Books

6 Excellent Free Books to Learn Coq

Last Updated on May 22, 2022

4. Mathematical Components by Assia Mahboubi and Enrico Tassi with contributions by Yves Bertot and Georges Gonthie

Mathematical ComponentsMathematical Components is the name of a library of formalized mathematics for the Coq proof assistants. It covers a variety of topics, from the theory of basic data structures (e.g., numbers, lists, finite sets) to more advanced results in various flavors of algebra. This library constitutes the infrastructure for the machine checked proofs of the Four Color Theorem and of the Odd Order Theorem.

This book aims at providing an introducing to the design patterns used throughout this library, so as to ease its use for other projects. While there are several books around covering the usage of the Coq system and the theory it is based on, the Mathematical Components library uses a few design patterns that differ from the methodology propose in other sources. As a consequence, this book provides a slightly non-standard presentation of Coq, putting upfront the formalization choices and the proof style that are the pillars of the library.

Read the book


5. Programs and Proofs: Mechanizing Mathematics with Dependent Types by Ilya Sergey

Programs and ProofsThese lecture notes are the result of the author’s personal experience of learning how to structure formal reasoning using the Coq proof assistant and employ Coq in large-scale research projects.

The present manuscript offers a brief and practically-oriented introduction to the basic concepts of mechanized reasoning and interactive theorem proving.

The primary audience of this text are the readers with expertise in software development and programming and knowledge of discrete mathematics disciplines on the level of an undergraduate university program

Read the book


6. Computer Arithmetic and Formal Proofs by Sylvie Boldo and Guillaume Melquiond

Computer Arithmetic and Formal ProofsFloating-point arithmetic is ubiquitous in modern computing, as it is the tool of choice to approximate real numbers. Due to its limited range and precision, its use can become quite involved and potentially lead to numerous failures. One way to greatly increase confidence in floating-point software is by computer-assisted verification of its correctness proofs.

This book provides a comprehensive view of how to formally specify and verify tricky floating-point algorithms with the Coq proof assistant. It describes the Flocq formalization of floating-point arithmetic and some methods to automate theorem proofs. It then presents the specification and verification of various algorithms, from error-free transformations to a numerical scheme for a partial differential equation. The examples cover not only mathematical algorithms but also C programs as well as issues related to compilation.

Read the book


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. Please read our FAQ before making a comment.

0 Comments
Oldest
Newest Most Voted
Inline Feedbacks
View all comments