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