From a4f4a8441c6588d4fdc70970ab3f87c581163254 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Sat, 11 Jul 2015 16:17:30 -0400
Subject: [PATCH] books/bookvol13 more work on proving Axiom
Goal: Axiom proven correct
Add references for proofs in COQ using OCaml and Common Lisp.
Obtained permission to use Theiry work.
---
books/bookvol13.pamphlet | 11 ++++
books/bookvolbib.pamphlet | 131 ++++++++++++++++++++++++++++++++++++++++
changelog | 3 +
patch | 9 ++-
src/axiom-website/patches.html | 2 +
5 files changed, 152 insertions(+), 4 deletions(-)
diff --git a/books/bookvol13.pamphlet b/books/bookvol13.pamphlet
index 4a6c499..031ae44 100644
--- a/books/bookvol13.pamphlet
+++ b/books/bookvol13.pamphlet
@@ -269,6 +269,17 @@ Temporal Logic of Actions (TLA)
Computerising Mathematical Text\cite{Kama15} explores various ways of
capturing mathematical reasoning.
+Chlipala\cite{Chli15} gives a pragmatic approach to COQ.
+
+Medina-Bulo et al.\cite{Bulo04} gives a formal verification of
+Buchberger's algorithm using ACL2 and Common Lisp.
+
+Th\'ery\cite{Ther01} used COQ to check an implementation of Buchberger's
+algorithm.
+
+Pierce\cite{Pier15} has a Software Foundations course in COQ with
+downloaded files in Pier15.tgz.
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter{Bibliography}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index ab269e5..aae6b60 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -2418,6 +2418,42 @@ Kelsey, Tom; Martin, Ursula; Owre, Sam
\end{chunk}
+\index{Medina-Bulo, I.}
+\index{Palomo-Lozano, F.}
+\index{Alonso-Jim\'enez, J.A.}
+\index{Ruiz-Reina, J.L.}
+\begin{chunk}{axiom.bib}
+@article{Bulo04,
+ author = "Medina-Bulo, I. and Palomo-Lozano, F. and Alonso-Jim\'enez, J.A.
+ and Ruiz-Reina, J.L.",
+ title = "Verified Computer Algebra in ACL2",
+ journal = "ASIC 2004, LNAI 3249",
+ year = "2004",
+ pages = "171-184",
+ paper = "Bulo04.pdf",
+ abstract = "In this paper, we present the formal verification of a
+ Common Lisp implementation of Buchberger's algorithm for computing
+ Groebner bases of polynomial ideals. This work is carried out in the
+ ACL2 system and shows how verified Computer Algebra can be achieved
+ in an executable logic."
+}
+
+\end{chunk}
+
+\index{Chlipala, Adam}
+\begin{chunk}{axiom.bib}
+@book{Chli15,
+ author = "Chlipala, Adam",
+ title = "Certified Programming with Dependent Types",
+ year = "2015",
+ url = "http://adam.chlipala.net/cpdt/cpdt.pdf",
+ publisher = "MIT Press",
+ isbn = "9780262026659",
+ paper = "Chli15.pdf"
+}
+
+\end{chunk}
+
\index{Mahboubi, Assia}
\begin{chunk}{axiom.bib}
@article{Mahb06,
@@ -2438,6 +2474,66 @@ Kelsey, Tom; Martin, Ursula; Owre, Sam
\end{chunk}
+\index{Pierce, Benjamin C.}
+\index{Casinghino, Chris}
+\index{Gaboardi, Marco}
+\index{Greenberg, Michael}
+\index{Hritcu, Catalin}
+\index{Sj\"oberg, Vilhelm}
+\index{Yorgey, Brent}
+\begin{chunk}{axiom.bib}
+@misc{Pier15,
+ author = "Pierce, Benjamin C. and Casinghino, Chris and Gaboardi, Marco and
+ Greenberg, Michael and Hritcu, Catalin and Sjoberg, Vilhelm and
+ Yorgey, Brent",
+ title = "Software Foundations",
+ year = "2015",
+ file = "Pier15.tgz",
+ abstract =
+ "This electronic book is a course on Software Foundations, the
+ mathematical underpinnings of reliable software. Topics include basic
+ concepts of logic, computer-assisted theorem proving, the Coq proof
+ assistant, functional programming, operational semantics, Hoare logic,
+ and static type systems. 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 will be helpful.
+
+ The principal novelty of the course is that it is one hundred per cent
+ formalized and machine-checked: the entire text is literally a script
+ for Coq. It is intended to be read alongside an interactive session
+ with Coq. All the details in the text are fully formalized in Coq, and
+ the exercises are designed to be worked using Coq.
+
+ The files are organized into a sequence of core chapters, covering
+ about one semester's worth of material and organized into a coherent
+ linear narrative, plus a number of appendices covering additional
+ topics. All the core chapters are suitable for both upper-level
+ undergraduate and graduate students."
+
+}
+
+\end{chunk}
+
+
+\index{Th\'ery, Laurent}
+\begin{chunk}{axiom.bib}
+@article{Ther01,
+ author = "Th\'ery, Laurent",
+ title = "A Machine-Checked Implementation of Buchberger's Algorithm",
+ journal = "Journal of Automated Reasoning",
+ volume = "26",
+ year = "2001",
+ pages = "107-137",
+ paper = "Ther01.pdf",
+ abstract = "We present an implementation of Buchberger's algorithm that
+ has been proved correct within the proof assistant Coq. The
+ implementation contains the basic algorithm plus two standard
+ optimizations."
+}
+
+\end{chunk}
+
\index{Ballarin, Clemens}
\index{Paulson, Lawrence C.}
\begin{chunk}{ignore}
@@ -3186,6 +3282,41 @@ in Lecture Notes in Computer Science, Springer ISBN 978-3-540-85520-0
\end{chunk}
+\index{Kamareddine, Fairouz}
+\index{Wells, Joe}
+\index{Zengler, Christoph}
+\index{Barendregt, Henk}
+\begin{chunk}{axiom.bib}
+@misc{Kama15,
+ author = "Kamareddine, Fairouz and Wells, Joe and Zengler, Christoph and
+ Barendregt, Henk",
+ title = "Computerising Mathematical Text",
+ year = "2015",
+ abstract =
+ "Mathematical texts can be computerised in many ways that capture
+ differing amounts of the mathematical meaning. At one end, there is
+ document imaging, which captures the arrangement of black marks on
+ paper, while at the other end there are proof assistants (e.g. Mizar,
+ Isabelle, Coq, etc.), which capture the full mathematical meaning and
+ have proofs expressed in a formal foundation of mathematics. In
+ between, there are computer typesetting systems (e.g. Latex and
+ Presentation MathML) and semantically oriented systems (e.g. Content
+ MathML, OpenMath, OMDoc, etc.). In this paper we advocate a style of
+ computerisation of mathematical texts which is flexible enough to
+ connect the diferent approaches to computerisation, which allows
+ various degrees of formalsation, and which is compatible with
+ different logical frameworks (e.g. set theory, category theory, type
+ theory, etc.) and proof systems. The basic idea is to allow a
+ man-machine collaboration which weaves human input with machine
+ computation at every step in the way. We propose that the huge step from
+ informal mathematics to fully formalised mathematics be divided into
+ smaller steps, each of which is a fully developed method in which
+ human input is minimal."
+
+}
+
+\end{chunk}
+
\index{van Leeuwen, Andr\'e M.A.}
\begin{chunk}{ignore}
\bibitem[Leeuwen]{Leexx} {van Leeuwen}, Andr\'e M.A.
diff --git a/changelog b/changelog
index 841ff32..bb3d757 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,6 @@
+20150711 tpd src/axiom-website/patches.html 20150711.01.tpd.patch
+20150711 tpd books/bookvolbib add references to CQQ proofs
+21050711 tpd books/bookvol13 add references to CQQ proofs
20150701 tpd src/axiom-website/patches.html 20150701.01.tpd.patch
20150701 tpd src/input/tuplebug.inputminor fixes to test suite
20150701 tpd src/input/polycoer.inputminor fixes to test suite
diff --git a/patch b/patch
index ee8ca2b..c853db1 100644
--- a/patch
+++ b/patch
@@ -1,9 +1,10 @@
-src/input/*.input.pamphlet
+books/bookvol13 more work on proving Axiom
-Goal: clean test suite
+Goal: Axiom proven correct
+
+Add references for proofs in COQ using OCaml and Common Lisp.
+Obtained permission to use Theiry work.
-Minor fixes were made to bookvol10.4, cachedf, clements, polycoer, and
-tuplebug to clean up test cases.
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 4cb6ea6..98ac3e9 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5090,6 +5090,8 @@ src/interp/i-code.lisp common lisp cleanup

src/interp/interop.lisp merge and purge code

20150701.01.tpd.patch
src/input/*.input

+20150711.01.tpd.patch
+books/bookvol13 add references to CQQ proofs

--
1.7.5.4