From b1d0952a5b70baf3e60e9581da8a912a33182082 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Wed, 28 Dec 2016 03:36:16 -0500
Subject: [PATCH] books/bookvolbib Mahboubi Mathematical Components
Goal: Proving Axiom Correct
\index{Mahboubi, Assia}
\index{Tassi, Enrico}
\index{Bertot, Yves}
\index{Gonthier, Georges}
\begin{chunk}{axiom.bib}
@book{Mahb16,
author = "Mahboubi, Assia and Tassi, Enrico and Bertot, Yves and
Gonthier, Georges",
title = "Mathematical Components",
year = "2016",
publisher = "math-comp.github.io/mcb",
url = "https://math-comp.github.io/mcb/book.pdf",
abstract =
"{\sl Mathematical Components} is the name of a library of formalized
mathematic for the COQ system. It covers a veriety of topics, from the
theory of basic data structures (e.g. numbers, lists, finite sets) to
advanced results in various flavors of algebra. This library
constitutes the infrastructure for the machine-checked proofs of the
Four Color Theorem and the Odd Order Theorem.
The reason of existence of this books is to break down the barriers to
entry. While there are several books around covering the usage of the
COQ system and the theory it is based on, the Mathematical Components
library is build in an unconventional way. As a consequence, this book
provides a non-standard presentation of COQ, putting upfront the
formalization choices and the proof style that are the pillars of the
library.
This book targets two classes of public. On one hand, newcomers, even
the more mathematically inclined ones, find a soft introduction to the
programming language of COQ, Gallina, and the Ssreflect proof
language. On the other hand accustomed COQ users find a substantial
accound of the formalization style that made the Mathematical
Components library possible.
By no means does this book pretend to be a complete description of COQ
or Ssreflect: both tools already come with a comprehensive user
manual. In the course of the book, the reader is nevertheless invited
to experiment with a large library of formalized concepts and she is
given as soon as possible sufficient tools to prove non-trivial
mathematical results by reusing parts of the library. By the end of
the first part, the reader has learnt how to prove formally the
infinitude of prime numbers, or the correctnes of the Euclidean's
division algorithm, in a few lines of proof text.",
paper = "Mahb16.pdf"
}
\end{chunk}
---
books/bookvol13.pamphlet | 4 ++-
books/bookvolbib.pamphlet | 49 +++++++++++++++++++++++++++++++++++
changelog | 3 ++
patch | 55 ++++++++++++++++++++++++++++++++++++++-
src/axiom-website/patches.html | 2 +
5 files changed, 110 insertions(+), 3 deletions(-)
diff --git a/books/bookvol13.pamphlet b/books/bookvol13.pamphlet
index 3e06868..e73acea 100644
--- a/books/bookvol13.pamphlet
+++ b/books/bookvol13.pamphlet
@@ -779,7 +779,9 @@ downloaded files in Pier15.tgz.
Spitters\cite{Spit11} Type Classes for Mathematics in Coq. Also see
\verb|http://www.eelis.net/research/math-classes/|
-\addcontentsline{toc}{chapter}{Bibliography}
+Mahboubi\cite{Mahb16} Mathematical Components. This book contains a
+proof of the Euclidean algorithm using COQ.
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\cleardoublepage
\phantomsection
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 6653e5f..12c22b6 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -5503,6 +5503,55 @@ Martin, U.
\end{chunk}
+\index{Mahboubi, Assia}
+\index{Tassi, Enrico}
+\index{Bertot, Yves}
+\index{Gonthier, Georges}
+\begin{chunk}{axiom.bib}
+@book{Mahb16,
+ author = "Mahboubi, Assia and Tassi, Enrico and Bertot, Yves and
+ Gonthier, Georges",
+ title = "Mathematical Components",
+ year = "2016",
+ publisher = "math-comp.github.io/mcb",
+ url = "https://math-comp.github.io/mcb/book.pdf",
+ abstract =
+ "{\sl Mathematical Components} is the name of a library of formalized
+ mathematic for the COQ system. It covers a veriety of topics, from the
+ theory of basic data structures (e.g. numbers, lists, finite sets) to
+ advanced results in various flavors of algebra. This library
+ constitutes the infrastructure for the machine-checked proofs of the
+ Four Color Theorem and the Odd Order Theorem.
+
+ The reason of existence of this books is to break down the barriers to
+ entry. While there are several books around covering the usage of the
+ COQ system and the theory it is based on, the Mathematical Components
+ library is build in an unconventional way. As a consequence, this book
+ provides a non-standard presentation of COQ, putting upfront the
+ formalization choices and the proof style that are the pillars of the
+ library.
+
+ This book targets two classes of public. On one hand, newcomers, even
+ the more mathematically inclined ones, find a soft introduction to the
+ programming language of COQ, Gallina, and the Ssreflect proof
+ language. On the other hand accustomed COQ users find a substantial
+ accound of the formalization style that made the Mathematical
+ Components library possible.
+
+ By no means does this book pretend to be a complete description of COQ
+ or Ssreflect: both tools already come with a comprehensive user
+ manual. In the course of the book, the reader is nevertheless invited
+ to experiment with a large library of formalized concepts and she is
+ given as soon as possible sufficient tools to prove non-trivial
+ mathematical results by reusing parts of the library. By the end of
+ the first part, the reader has learnt how to prove formally the
+ infinitude of prime numbers, or the correctnes of the Euclidean's
+ division algorithm, in a few lines of proof text.",
+ paper = "Mahb16.pdf"
+}
+
+\end{chunk}
+
\index{Medina-Bulo, I.}
\index{Palomo-Lozano, F.}
\index{Alonso-Jim\'enez, J.A.}
diff --git a/changelog b/changelog
index fdbf037..bcf2dc0 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,6 @@
+20161227 tpd src/axiom-website/patches.html 20161227.01.tpd.patch
+20161227 tpd books/bookvol13 add Mahboubi Mathematical Components
+20161227 tpd books/bookvolbib Mahboubi Mathematical Components
20161225 tpd src/axiom-website/patches.html 20161225.01.tpd.patch
20161225 tpd books/bookvolbib minor typo fix
20161218 tpd src/axiom-website/patches.html 20161218.01.tpd.patch
diff --git a/patch b/patch
index c099009..335b1b5 100644
--- a/patch
+++ b/patch
@@ -1,5 +1,56 @@
-books/bookvolbib minor typo fix
+books/bookvolbib Mahboubi Mathematical Components
+
+Goal: Proving Axiom Correct
+
+\index{Mahboubi, Assia}
+\index{Tassi, Enrico}
+\index{Bertot, Yves}
+\index{Gonthier, Georges}
+\begin{chunk}{axiom.bib}
+@book{Mahb16,
+ author = "Mahboubi, Assia and Tassi, Enrico and Bertot, Yves and
+ Gonthier, Georges",
+ title = "Mathematical Components",
+ year = "2016",
+ publisher = "math-comp.github.io/mcb",
+ url = "https://math-comp.github.io/mcb/book.pdf",
+ abstract =
+ "{\sl Mathematical Components} is the name of a library of formalized
+ mathematic for the COQ system. It covers a veriety of topics, from the
+ theory of basic data structures (e.g. numbers, lists, finite sets) to
+ advanced results in various flavors of algebra. This library
+ constitutes the infrastructure for the machine-checked proofs of the
+ Four Color Theorem and the Odd Order Theorem.
+
+ The reason of existence of this books is to break down the barriers to
+ entry. While there are several books around covering the usage of the
+ COQ system and the theory it is based on, the Mathematical Components
+ library is build in an unconventional way. As a consequence, this book
+ provides a non-standard presentation of COQ, putting upfront the
+ formalization choices and the proof style that are the pillars of the
+ library.
+
+ This book targets two classes of public. On one hand, newcomers, even
+ the more mathematically inclined ones, find a soft introduction to the
+ programming language of COQ, Gallina, and the Ssreflect proof
+ language. On the other hand accustomed COQ users find a substantial
+ accound of the formalization style that made the Mathematical
+ Components library possible.
+
+ By no means does this book pretend to be a complete description of COQ
+ or Ssreflect: both tools already come with a comprehensive user
+ manual. In the course of the book, the reader is nevertheless invited
+ to experiment with a large library of formalized concepts and she is
+ given as soon as possible sufficient tools to prove non-trivial
+ mathematical results by reusing parts of the library. By the end of
+ the first part, the reader has learnt how to prove formally the
+ infinitude of prime numbers, or the correctnes of the Euclidean's
+ division algorithm, in a few lines of proof text.",
+ paper = "Mahb16.pdf"
+}
+
+\end{chunk}
+
-Goal: Axiom Maintenance
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 62ad770..b6f4abe 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5612,6 +5612,8 @@ books/bookvolbib add Reis06 Specifying C++ Concepts

books/bookvol5 remove addConsDB

20161225.01.tpd.patch
books/bookvolbib minor typo fix

+20161227.01.tpd.patch
+books/bookvolbib Mahboubi Mathematical Components

--
1.7.5.4