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