From 09f6a07f639d165f9c580630a5ebda7b46696a10 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Sat, 18 Jul 2015 16:25:41 -0400
Subject: [PATCH] books/bookvolbib: Add program proof papers
Goal: Prove Axiom correct
Several papers related to proving algorithms (Buchberger's, GCD,
and Cylindrical Algebraic Decomposition) were added.
---
books/bookvol13.pamphlet | 25 ++++++
books/bookvolbib.pamphlet | 165 +++++++++++++++++++++++++++++++++++++++-
changelog | 3 +
patch | 6 +-
src/axiom-website/patches.html | 2 +
5 files changed, 195 insertions(+), 6 deletions(-)
diff --git a/books/bookvol13.pamphlet b/books/bookvol13.pamphlet
index 031ae44..735419c 100644
--- a/books/bookvol13.pamphlet
+++ b/books/bookvol13.pamphlet
@@ -71,6 +71,31 @@ adaptability.}
-- Scherlis and Scott (1983) in \cite{Maso86}
\end{quote}
+
+\begin{quote}
+...constructive mathematics provides a way of viewing the language of
+logical propositions as a {\sl specification} language for
+programs. An ongoing thrust of work in computer science has been to
+develop program specification languages and formalisms for
+systematically deriving programs from specifications. For constructive
+mathematics to provide such a methodology, techniques are needed for
+systematically extracting programs from constructive proofs. Early work
+in this field includes that of Bishop and Constable. What
+distinguished Martin-L\"of's '82 type theory was that the method it
+suggested for program synthesis was exceptionally simple: a direct
+correspondence was set up between the constructs of mathematical
+logic, and the constructs of a functional programming
+language. Specifically, every proposition was considered to be
+isomorphic to a type expression, and the proof of a proposition would
+suggest precisely how to construct an inhabitant of the type, which
+would be a term in a functional programming language. The term that
+inhabits the type corresponding to a proposition is often referred to as
+the {\sl computational content} of the proposition.
+
+-- Paul Bernard Jackson\cite{Jack95}
+
+\end{quote}
+
\chapter{Here is a problem}
The goal is to prove that Axiom's implementation of
the Euclidean GCD algorithm is correct.
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index aae6b60..89e2671 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -2440,6 +2440,35 @@ 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{Bulo10,
+ author = "Medina-Bulo, I. and Palomo-Lozano, F. and Alonso-Jim\'enez, J.A.
+ and Ruiz-Reina, J.L.",
+ title = "A verified Common Lisp implementation of Buchberger's algorithm
+ in ACL2",
+ journal = "Journal of Symbolic Computation",
+ year = "2010",
+ pages = "96-123",
+ paper = "Bulo10.pdf",
+ abstract = "In this article, we present the formal verification of a
+ Common Lisp implementation of Buchberger's algorithm or computing
+ Groebner bases of polynomial ideals. This work is carried out in ACL2,
+ a system which provices an integrated environment where programming
+ (in a pure functional subset of Commmon Lisp) and formal verification
+ of programs, with the assistance of a theorem prover, are possible. Our
+ imlementation is written in a real programming language and it is
+ directly executable within the ACL2 system or any compliant Common Lisp
+ system. We provide here snippets o real verified code, discuss the
+ formalization details in depth, and present quantitative data about
+ the proof effort."
+}
+
+\end{chunk}
+
\index{Chlipala, Adam}
\begin{chunk}{axiom.bib}
@book{Chli15,
@@ -2454,6 +2483,62 @@ Kelsey, Tom; Martin, Ursula; Owre, Sam
\end{chunk}
+\index{Jackson, Paul Bernard}
+\begin{chunk}{axiom.bib}
+@phdthesis{Jack95,
+ author = "Jackson, Paul Bernard",
+ title = "Enhancing the NUPRL Proof Development System and Applying it to Computational Abstract Algebra",
+ school = "Cornell University",
+ year = "1995",
+ month = "1",
+ file = "Jack95.pdf",
+ keyword = "axiomref",
+ note = {
+ This thesis describes substantial enhancements that were made to the
+ software tools in the Nuprl system that are used to interactively
+ guide the production of formal proofs. Over 20,000 lines of code were
+ written for these tools. Also, a corpus of formal mathematics was
+ created that consists of roughly 500 definitions and 1300
+ theorems. Much of this material is of a foundational nature and
+ supports all current work in Nuprl. This thesis concentrates on
+ describing the half of this corpus that is concerned with abstract
+ algebra and that covers topics central to the mathematics of the
+ computations carried out by computer algebra systems.
+
+ The new proof tools include those that solve linear arithmetic
+ problems, those that apply the properties of order relations, those
+ that carry out inductive proof to support recursive definitions, and
+ those that do sophisticated rewriting. The rewrite tools allow
+ rewriting with relations of differing strengths and take care of
+ selecting and applying appropriate congruence lemmas automatically.
+ The rewrite relations can be order relations as well as equivalence
+ relations. If they are order relations, appropriate monotonicity
+ lemmas are selected.
+
+ These proof tools were heavily used throughout the work on
+ computational algebra. Many examples are given that illustrate their
+ operation and demonstrate their effectiveness.
+
+ The foundation for algebra introduced classes of monoids, groups, ring
+ and modules, and included theories of order relations and
+ permutations. Work on finite sets and multisets illustrates how a
+ quotienting operation hides details of datatypes when reasoning about
+ functional programs. Theories of summation operators were developed
+ that drew indices from integer ranges, lists and multisets, and that
+ summed over all the classes mentioned above. Elementary factorization
+ theory was developed that characterized when cancellation monoids are
+ factorial. An abstract data type for the operations of multivariate
+ polynomial arithmetic was defined and the correctness of an
+ implementation of these operations was verified. The implementation is
+ similar to those found in current computer algebra systems.
+
+ This work was all done in Nuprl's constructive type theory. The thesis
+ discusses the appropriateness of this foundation, and the extent to
+ which the work relied on it.}
+}
+
+\end{chunk}
+
\index{Mahboubi, Assia}
\begin{chunk}{axiom.bib}
@article{Mahb06,
@@ -2474,6 +2559,50 @@ Kelsey, Tom; Martin, Ursula; Owre, Sam
\end{chunk}
+\index{Mahboubi, Assia}
+\begin{chunk}{axiom.bib}
+@article{Mahb07,
+ author = "Mahboubi, Assia",
+ title = "Implementing the cylindrical algebraic decomposition within the Coq system",
+ journal = "Math. Struct. in Comp. Science",
+ volume = "17",
+ year = "2007",
+ pages = "99-127",
+ paper = "Mahb07.pdf",
+ abstract = "The Coq system is a Curry-Howard based proof assistant.
+ Therefore, it contains a full functional, strongly typed programming
+ language, which can be used to enhance the system with powerful
+ automation tools through the implementation of reflexive tactics.
+ We present the implementation of a cylindrical algebraic decomposition
+ algorithm within the Coq system, whose certification leads to a proof
+ producing decision procedure for the first-order theory of real numbers."
+}
+
+\end{chunk}
+
+\index{M\"ortberg, Anders}
+\begin{chunk}{axiom.bib}
+@mastersthesis{Mort10,
+ author = {M\"ortbert, Anders},
+ title = "Constructive Algebra in Functional Programming and Type Theory",
+ school = "University of Gothenburg, Department of Computer Science",
+ year = "2010",
+ month = "5",
+ file = "Mort10.pdf",
+ note = {This thesis considers abstract algebra from a constructive point
+ of view. The central concept of study is coherent rings -- algebraic
+ structures in which it is possible to solve homogeneous systems of
+ linear equations. Three different algebraic theories are considered;
+ B\'ezout domains, Pr\"ufer domains and polynomial rings. The first two
+ of these are non-Noetherian analogues of classical notions. The
+ polynomial rings are presented from a constructive point of view with a
+ treatment of Groebner bases. The goal of the thesis is to study the
+ proofs that these theories are coherent and explore how the proofs can
+ be implemented in functional programming and type theory.}
+}
+
+\end{chunk}
+
\index{Pierce, Benjamin C.}
\index{Casinghino, Chris}
\index{Gaboardi, Marco}
@@ -2483,9 +2612,9 @@ Kelsey, Tom; Martin, Ursula; Owre, Sam
\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",
+ author = {Pierce, Benjamin C. and Casinghino, Chris and Gaboardi, Marco and
+ Greenberg, Michael and Hritcu, Catalin and Sj\"oberg, Vilhelm and
+ Yorgey, Brent},
title = "Software Foundations",
year = "2015",
file = "Pier15.tgz",
@@ -2534,6 +2663,36 @@ Kelsey, Tom; Martin, Ursula; Owre, Sam
\end{chunk}
+\index{Troelstra, A.S.}
+\begin{chunk}{axiom.bib}
+@article{Troe97,
+ author = "Troelstra, A.S.",
+ title = "From constructivism to computer science",
+ volume = "211",
+ year = "1999",
+ pages = "232-252",
+ paper = "Troe99.pdf",
+ abstract =
+ {My field is mathematical logic, with a special interest in
+ constructivism, and I would not dare to call myself a computer
+ scientist. But some computer scientists regard my work as a
+ contribution to their field; and in this text I shall try to explain
+ how this is possible, by taking a look at the history of ideas.
+
+ I want to describe how two interrelated ideas, connected with the
+ constructivistic trend in the foundations of mathematics, developed
+ within mathematical logic and ultimatelyh diffused into computer
+ science.
+
+ It will be seen that this development has not been a quite
+ straightforward one. In the history of ideas it often looks as if a
+ certain idea has to be discovered several times, by different people,
+ before it really enters inthe the "consciousness" of science}
+
+}
+
+\end{chunk}
+
\index{Ballarin, Clemens}
\index{Paulson, Lawrence C.}
\begin{chunk}{ignore}
diff --git a/changelog b/changelog
index e806e6f..bb44775 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,6 @@
+20150718 tpd src/axiom-website/patches.html 20150718.01.tpd.patch
+20150718 tpd books/bookvol13 Add program proof papers
+20150718 tpd books/bookvolbib Add program proof papers
20150716 tpd src/axiom-website/patches.html 20150716.01.tpd.patch
20150716 tpd books/Makefile extract and run proof code automatically
20150716 tpd Makefile extract and run proof code automatically
diff --git a/patch b/patch
index 2650206..82321d3 100644
--- a/patch
+++ b/patch
@@ -1,6 +1,6 @@
-Makefile: extract and run proof code automatically
+books/bookvolbib: Add program proof papers
Goal: Prove Axiom correct
-If the command line include "COQ=coq" then the system extracts the
-'coq' chunk from the books and run coq proof code automatically.
+Several papers related to proving algorithms (Buchberger's, GCD,
+and Cylindrical Algebraic Decomposition) were added.
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 4afe204..0701609 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5106,6 +5106,8 @@ books/bookvol5: Use ACL2 to prove isWrapped function

Makefile: extract and run proof code automatically

20150716.01.tpd.patch
Makefile: extract and run proof code automatically

+20150718.01.tpd.patch
+books/bookvolbib Add program proof papers

--
1.7.5.4