From 3e6c5c6bb5f34e2dc899f78594f6ca79b92cc20f Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Fri, 29 Sep 2017 19:50:59 0400
Subject: [PATCH] books/bookvolbib add references
MIMEVersion: 1.0
ContentType: text/plain; charset=UTF8
ContentTransferEncoding: 8bit
Goal: Proving Axiom Correct
\index{Meshveliani, Sergei D.}
\begin{chunk}{axiom.bib}
@misc{Mesh13,
author = "Meshveliani, Sergei D.",
title = Dependent Types for an Adequate Programming of Algebra",
link = "\url{http://ceurws.org/Vol1010/paper05.pdf}",
year = "2005",
abstract =
"This research compares the author’s experience in program ming
algebra in Haskell and in Agda (currently the former experience is
large, and the latter is small). There are discussed certain hopes and
doubts related to the dependently typed and verified programming of
symbolic computation. This concerns the 1) author’s experience
history, 2) algebraic class hierarchy design, 3) proof cost overhead
in evaluation and in coding, 4) other subjects. Various examples are
considered.",
paper = "Mesh13.pdf"
}
\end{chunk}
\index{Norell, Ulf}
\index{Chapman, James}
\begin{chunk}{axiom.bib}
@misc{Nore08,
author = "Norell, Ulf and Chapman, James",
title = "Dependently Typed Programming in Agda",
link = "\url{http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf}",
year = "2008",
paper = "Nore08.pdf"
}
\end{chunk}
\index{Bidoit, M.}
\index{Kreowski, H.J.}
\index{Lescanne, P.}
\index{Orejas, F.}
\index{Sannella, D.}
\begin{chunk}{axiom.bib}
@book{Bido91,
author = "Bidoit, M. and Kreowski, H.J. and Lescanne, P. and
Orejas, F. and Sannella, D.",
title = "Algebraic System Specification and Development",
publisher = "SpringerVerlag",
comment = "LNCS 501",
year = "1991",
isbn = "3540540601",
abstract =
"A great deal of work has been devoted to methods of specification
based on the simple idea that a functional program can be modelled as
a {\sl manysorted algebra}, i.e. as a number of sets of data values
(one set of values for each data type) together with a number of total
functions on those sets corresponding to the functions in the
program. This abstracts away from the algorithms used to compute the
functions and how those algorithms are expressed in a given
programming language, focusing instead on the representation of data
and the input/output behavior of functions. The pioneering work in
this area is [Zil 74],[Gut 75], [GTW 76], of which the latter  the
socalled {\sl initial algebra approach}  is the most formal This
idea was soon taken up by other workers, see e.g. [GGM 76], [GHM 76],
[BG 77], [GHM 78]. Today the field of algebraic specification has
grown into one of the major areas of research in theoretical computer
science. More than fifteen years of research have led to an abundance
of competing and complementary theories and approaches. The algebraic
approach provides a conceptual basis, theoretical fundations, and
prototype tools for the stepwise formal development of correct system
components from their specifications, and thus covers the whole
software development process from the specification of requirements to
the finished system. These methos are potentially applicable to the
development of correct hardware systems as well"
}
\end{chunk}

books/axiom.bib  99 ++++++++++
books/bookvolbib.pamphlet  105 +++++++++++
changelog  2 +
patch  379 +++++++
src/axiomwebsite/patches.html  2 +
5 files changed, 256 insertions(+), 331 deletions()
diff git a/books/axiom.bib b/books/axiom.bib
index ff134a1..52ddaf2 100644
 a/books/axiom.bib
+++ b/books/axiom.bib
@@ 7167,6 +7167,40 @@ paper = "Brea89.pdf"
development of zerofault software."
}
+@book{Bido91,
+ author = "Bidoit, M. and Kreowski, H.J. and Lescanne, P. and
+ Orejas, F. and Sannella, D.",
+ title = "Algebraic System Specification and Development",
+ publisher = "SpringerVerlag",
+ comment = "LNCS 501",
+ year = "1991",
+ isbn = "3540540601",
+ abstract =
+ "A great deal of work has been devoted to methods of specification
+ based on the simple idea that a functional program can be modelled as
+ a {\sl manysorted algebra}, i.e. as a number of sets of data values
+ (one set of values for each data type) together with a number of total
+ functions on those sets corresponding to the functions in the
+ program. This abstracts away from the algorithms used to compute the
+ functions and how those algorithms are expressed in a given
+ programming language, focusing instead on the representation of data
+ and the input/output behavior of functions. The pioneering work in
+ this area is [Zil 74],[Gut 75], [GTW 76], of which the latter  the
+ socalled {\sl initial algebra approach}  is the most formal This
+ idea was soon taken up by other workers, see e.g. [GGM 76], [GHM 76],
+ [BG 77], [GHM 78]. Today the field of algebraic specification has
+ grown into one of the major areas of research in theoretical computer
+ science. More than fifteen years of research have led to an abundance
+ of competing and complementary theories and approaches. The algebraic
+ approach provides a conceptual basis, theoretical fundations, and
+ prototype tools for the stepwise formal development of correct system
+ components from their specifications, and thus covers the whole
+ software development process from the specification of requirements to
+ the finished system. These methos are potentially applicable to the
+ development of correct hardware systems as well"
+
+}
+
@misc{Bold07,
author = "Boldo, Sylvie and Filliatre, JeanChristophe",
title = "Formal Verification of FloatingPoint programs",
@@ 8415,7 +8449,7 @@ paper = "Brea89.pdf"
paper = "Heut16.pdf"
}
@article{Jack94,
+@misc{Jack94,
author = "Jackson, Paul",
title = "Exploring Abstract Algebra in Constructive Type Theory",
year = "1994",
@@ 8523,6 +8557,23 @@ paper = "Brea89.pdf"
keywords = "axiomref, CASProof"
}
+@phdthesis{Kali09,
+ author = "Kaliszyk, Cezary",
+ title = "Correctness and Availability: Building Computer Algebra on top
+ of Proof Assistants and making Proof Assistants available over
+ the Web",
+ year = "2009",
+ school = "Radboud University, Nijmegen",
+ link = "\url{http://clinformatik.uibk.ac.at/users/cek/docs/09/kaliszyk\_thesis\_webdoc.pdf}",
+ abstract =
+ "In this thesis we present an approach to extending the usability
+ of proof assistants in mathematics and computer science. We do it
+ in two ways: by combining proof assistants with computer algebra
+ systems and by providing interactive access to such systems on
+ the web.",
+ paper = "Kali09.pdf"
+}
+
@misc{Kauf98,
author = "Kaufmann, Matt and Moore, J Strother",
title = "A Precise Description of the ACL2 Logic",
@@ 8996,6 +9047,23 @@ paper = "Brea89.pdf"
}
+@misc{Mesh13,
+ author = "Meshveliani, Sergei D.",
+ title = "Dependent Types for an Adequate Programming of Algebra",
+ link = "\url{http://ceurws.org/Vol1010/paper05.pdf}",
+ year = "2013",
+ abstract =
+ "This research compares the author’s experience in program ming
+ algebra in Haskell and in Agda (currently the former experience is
+ large, and the latter is small). There are discussed certain hopes and
+ doubts related to the dependently typed and verified programming of
+ symbolic computation. This concerns the 1) author’s experience
+ history, 2) algebraic class hierarchy design, 3) proof cost overhead
+ in evaluation and in coding, 4) other subjects. Various examples are
+ considered.",
+ paper = "Mesh13.pdf"
+}
+
@misc{Mesh10,
author = "Meshveliani, Sergei D.",
title = "Haskell and computer algebra",
@@ 9214,6 +9282,16 @@ paper = "Brea89.pdf"
keywords = "coercion"
}
+@misc{Neup13,
+ author = "Neuper, Walther",
+ title = "Computer Algebra implemented in Isabelle's Function Package
+ under LucasInterpretation  a Case Study",
+ year = "2013",
+ link = "\url{http://ceurws.org/Vol1010/paper09.pdf}",
+ paper = "Neup13.pdf",
+ keywords = "CASProof"
+}
+
@book{Nipk14,
author = "Nipkow, Tobias and Klein, Gerwin",
title = "Concrete Semantics",
@@ 16588,6 +16666,14 @@ paper = "Brea89.pdf"
paper = "Kohl08.pdf"
}
+@misc{Nore08,
+ author = "Norell, Ulf and Chapman, James",
+ title = "Dependently Typed Programming in Agda",
+ link = "\url{http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf}",
+ year = "2008",
+ paper = "Nore08.pdf"
+}
+
@article{Stou79,
author = "Stoutemyer, David R.",
title = "LISP Based Symbolic Math Systems",
@@ 29691,9 +29777,12 @@ paper = "Brea89.pdf"
@misc{Duns01,
author = "Dunstan, M.N. and Gottliebsen, H. and Kelsey, T.W. and
Martin, U.",
 title = "A MaplePVS Interface",
+ title = "Computer Algebra meets Automated Theorem Proving: A
+ MaplePVS Interface",
booktitle = "Proc. Calculemus, 2001",
 year = "2001"
+ year = "2001",
+ paper = "Duns01.pdf",
+ keywords = "axiomref, CASproof"
}
@article{Dute96,
@@ 30399,6 +30488,7 @@ paper = "Brea89.pdf"
author = "Komendantsky, V. and Konovalov, A. and Linton, S.A.",
title = "Interfacing Coq + SSReflect with GAP",
journal = "Electronic Notes in Theoretical Computer Science",
+ year = "2012",
volume = "295",
number = "19",
pages = "1728",
@@ 30753,9 +30843,8 @@ paper = "Brea89.pdf"
@misc{Maye17,
author = "Mayero, Micaela and Delahaye, David",
title = "A Maple Mode for Coq",
+ link = "\url{https://github.com/coqcontribs/maplemode}",
year = "2017",
 link =
 "\url{http://www.lix.polytechnique.fr/coq/V8.2pl1/contribs/MapleMode.html}",
abstract =
"This contribution is an interface between Coq and Maple. In
particular, this exports the functions simplify/factor/expand/normal
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 6f873da..e1da20b 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 9868,6 +9868,48 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp12151231
\end{chunk}
+\index{Bidoit, M.}
+\index{Kreowski, H.J.}
+\index{Lescanne, P.}
+\index{Orejas, F.}
+\index{Sannella, D.}
+\begin{chunk}{axiom.bib}
+@book{Bido91,
+ author = "Bidoit, M. and Kreowski, H.J. and Lescanne, P. and
+ Orejas, F. and Sannella, D.",
+ title = "Algebraic System Specification and Development",
+ publisher = "SpringerVerlag",
+ comment = "LNCS 501",
+ year = "1991",
+ isbn = "3540540601",
+ abstract =
+ "A great deal of work has been devoted to methods of specification
+ based on the simple idea that a functional program can be modelled as
+ a {\sl manysorted algebra}, i.e. as a number of sets of data values
+ (one set of values for each data type) together with a number of total
+ functions on those sets corresponding to the functions in the
+ program. This abstracts away from the algorithms used to compute the
+ functions and how those algorithms are expressed in a given
+ programming language, focusing instead on the representation of data
+ and the input/output behavior of functions. The pioneering work in
+ this area is [Zil 74],[Gut 75], [GTW 76], of which the latter  the
+ socalled {\sl initial algebra approach}  is the most formal This
+ idea was soon taken up by other workers, see e.g. [GGM 76], [GHM 76],
+ [BG 77], [GHM 78]. Today the field of algebraic specification has
+ grown into one of the major areas of research in theoretical computer
+ science. More than fifteen years of research have led to an abundance
+ of competing and complementary theories and approaches. The algebraic
+ approach provides a conceptual basis, theoretical fundations, and
+ prototype tools for the stepwise formal development of correct system
+ components from their specifications, and thus covers the whole
+ software development process from the specification of requirements to
+ the finished system. These methos are potentially applicable to the
+ development of correct hardware systems as well"
+
+}
+
+\end{chunk}
+
\index{Boldo, Sylvie}
\index{Filliatre, JeanChristophe}
\begin{chunk}{axiom.bib}
@@ 11550,7 +11592,7 @@ England, Matthew; Wilson, David
\index{Jackson, Paul}
\begin{chunk}{axiom.bib}
@article{Jack94,
+@misc{Jack94,
author = "Jackson, Paul",
title = "Exploring Abstract Algebra in Constructive Type Theory",
year = "1994",
@@ 11678,7 +11720,7 @@ England, Matthew; Wilson, David
\index{Kaliszyk, Cezary}
\begin{chunk}{axiom.bib}
@phdthesis{Kali09,
 author = "Kaliszyk, Cezary"
+ author = "Kaliszyk, Cezary",
title = "Correctness and Availability: Building Computer Algebra on top
of Proof Assistants and making Proof Assistants available over
the Web",
@@ 12299,6 +12341,27 @@ England, Matthew; Wilson, David
\index{Meshveliani, Sergei D.}
\begin{chunk}{axiom.bib}
+@misc{Mesh13,
+ author = "Meshveliani, Sergei D.",
+ title = "Dependent Types for an Adequate Programming of Algebra",
+ link = "\url{http://ceurws.org/Vol1010/paper05.pdf}",
+ year = "2013",
+ abstract =
+ "This research compares the author’s experience in program ming
+ algebra in Haskell and in Agda (currently the former experience is
+ large, and the latter is small). There are discussed certain hopes and
+ doubts related to the dependently typed and verified programming of
+ symbolic computation. This concerns the 1) author’s experience
+ history, 2) algebraic class hierarchy design, 3) proof cost overhead
+ in evaluation and in coding, 4) other subjects. Various examples are
+ considered.",
+ paper = "Mesh13.pdf"
+}
+
+\end{chunk}
+
+\index{Meshveliani, Sergei D.}
+\begin{chunk}{axiom.bib}
@misc{Mesh10,
author = "Meshveliani, Sergei D.",
title = "Haskell and computer algebra",
@@ 12567,6 +12630,20 @@ England, Matthew; Wilson, David
\subsection{N} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Neuper, Walther}
+\begin{chunk}{axiom.bib}
+@misc{Neup13,
+ author = "Neuper, Walther",
+ title = "Computer Algebra implemented in Isabelle's Function Package
+ under LucasInterpretation  a Case Study",
+ year = "2013",
+ link = "\url{http://ceurws.org/Vol1010/paper09.pdf}",
+ paper = "Neup13.pdf",
+ keywords = "CASProof"
+}
+
+\end{chunk}
+
\index{Newcombe, Chris}
\index{Rath, Tim}
\index{Zhang, Fan}
@@ 23342,6 +23419,19 @@ Proc ISSAC 97 pp172175 (1997)
\end{chunk}
+\index{Norell, Ulf}
+\index{Chapman, James}
+\begin{chunk}{axiom.bib}
+@misc{Nore08,
+ author = "Norell, Ulf and Chapman, James",
+ title = "Dependently Typed Programming in Agda",
+ link = "\url{http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf}",
+ year = "2008",
+ paper = "Nore08.pdf"
+}
+
+\end{chunk}
+
\index{Stoutemyer, David R.}
\begin{chunk}{axiom.bib}
@article{Stou79,
@@ 45059,9 +45149,12 @@ A.E.R.E. Report R.8730. HMSO. (1977)
@misc{Duns01,
author = "Dunstan, M.N. and Gottliebsen, H. and Kelsey, T.W. and
Martin, U.",
 title = "A MaplePVS Interface",
+ title = "Computer Algebra meets Automated Theorem Proving: A
+ MaplePVS Interface",
booktitle = "Proc. Calculemus, 2001",
 year = "2001"
+ year = "2001",
+ paper = "Duns01.pdf",
+ keywords = "axiomref, CASproof"
}
\end{chunk}
@@ 46637,6 +46730,7 @@ J. Symbolic Computations 8, 545552 (1989)
author = "Komendantsky, V. and Konovalov, A. and Linton, S.A.",
title = "Interfacing Coq + SSReflect with GAP",
journal = "Electronic Notes in Theoretical Computer Science",
+ year = "2012",
volume = "295",
number = "19",
pages = "1728",
@@ 47256,9 +47350,8 @@ Mathematical Surveys. 3 Am. Math. Soc., Providence, RI. (1966)
@misc{Maye17,
author = "Mayero, Micaela and Delahaye, David",
title = "A Maple Mode for Coq",
+ link = "\url{https://github.com/coqcontribs/maplemode}",
year = "2017",
 link =
 "\url{http://www.lix.polytechnique.fr/coq/V8.2pl1/contribs/MapleMode.html}",
abstract =
"This contribution is an interface between Coq and Maple. In
particular, this exports the functions simplify/factor/expand/normal
diff git a/changelog b/changelog
index 506aabf..fe5fed2 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20170929 tpd src/axiomwebsite/patches.html 20170929.01.tpd.patch
+20170929 tpd books/bookvolbib add references
20170924 tpd src/axiomwebsite/patches.html 20170924.01.tpd.patch
20170924 tpd books/bookvolbib add references
20170907 tpd src/axiomwebsite/patches.html 20170907.01.tpd.patch
diff git a/patch b/patch
index 7721955..7c92d10 100644
 a/patch
+++ b/patch
@@ 1,341 +1,80 @@
books/bookvolbib add Coercion references
+books/bookvolbib add references
Goal: Proving Axiom Correct
\index{Traytel, Dmitriy}
\index{Berghofer, Stefan}
\index{Nipkow, Tobias}
+\index{Meshveliani, Sergei D.}
\begin{chunk}{axiom.bib}
@article{Tray11,
 author = "Traytel, Dmitriy and Berghofer, Stefan and Nipkow, Tobias",
 title = "Extending HindleyMilner Type Inference with Coercive
 Structural Subtyping",
 journal = "LNCS",
 volume = "7078",
 pages = "89104",
 year = "2011",
 abstract =
 "We investigate how to add coercive structural subtyping to a type
 system for simplytyped lambda calculus with HindleyMilner
 polymorphism. Coercions allow to convert between different types, and
 their automatic insertion can greatly increase readability of
 terms. We present a type inference algorithm that, given a term
 without type information, computes a type assignment and determines at
 which positions in the term coercions have to be inserted to make it
 typecorrect according to the standard HindleyMilner system (without
 any subtypes). The algorithm is sound and, if the subtype relation
 on base types is a disjoint union of lattices, also complete. The
 algorithm has been implemented in the proof assistant Isabelle.",
 paper = "Tray11.pdf",
 keywords = "coercion"
}

\end{chunk}

\index{Ab\'anades, M.}
\index{Botana, F.}
\index{Kov\'acs, Z.}
\index{Recio, T.}
\index{S\'olyomGecse, C.}
\begin{chunk}{axiom.bib}
@article{Aban16,
 author = "Abanades, M. and Botana, F. and Kovacs, Z. and Recio, T. and
 SolyomGecse, C.",
 title = "Development of automatic reasoning tools in GeoGebra",
 journal = "ACM Comm. Computer Algebra",
 volume = "50",
 pages = "8588",
 year = "2016",
+@misc{Mesh13,
+ author = "Meshveliani, Sergei D.",
+ title = Dependent Types for an Adequate Programming of Algebra",
+ link = "\url{http://ceurws.org/Vol1010/paper05.pdf}",
+ year = "2005",
abstract =
 "Much effort has been put into the implementation of automatic proving
 in interactive geometric environments (e.g. Java Geometry Expert,
 GeoGebra). The closely related concept of automatic discovery, remains
 however almost unexplored.

 This software presentation will demonstrate our results towards the
 incorporation of automatic discovery capabilities into GeoGebra, an
 educational software with tens of millions of users worldwide. As main
 result, we report on a new command, currently available in the
 official version, that allows the automatic discovery of loci of
 points in diagrams defined by implicit conditions. This represents an
 extension of a previous command, similar in nature, but restricted to
 loci defined by the standard movertracer construction. Our proposal
 successfully automates the `dummy locus dragging' in dynamic
 geometry. This makes the cycle conjecturingcheckingproving
 accessible for general users in elementary geometry.",
 paper = "Aban16.pdf"
+ "This research compares the author’s experience in program ming
+ algebra in Haskell and in Agda (currently the former experience is
+ large, and the latter is small). There are discussed certain hopes and
+ doubts related to the dependently typed and verified programming of
+ symbolic computation. This concerns the 1) author’s experience
+ history, 2) algebraic class hierarchy design, 3) proof cost overhead
+ in evaluation and in coding, 4) other subjects. Various examples are
+ considered.",
+ paper = "Mesh13.pdf"
}
\end{chunk}
\index{Avigad, Jeremy}
+\index{Norell, Ulf}
+\index{Chapman, James}
\begin{chunk}{axiom.bib}
@article{Avig12a,
 author = "Avigad, Jeremy",
 title = "Type Inference in Mathematics",
 journal = "European Association of Theoretical Computer Science",
 volume = "106",
 pages = "7898",
 year = "2012",
 abstract =
 "In the theory of programming languages, type inference is the process
 of inferring the type of an expression automatically, often making use
 of information from the context in which the expression appears. Such
 mechanisms turn out to be extremely useful in the practice of
 interactive theorem proving, whereby users interact with a
 computational proof assistant to construct formal axiomatic
 derivations of mathematical theorems. This article explains some of
 the mechanisms for type inference used by the Mathematical
 Components project, which is working towards a verification of the
 FeitThompson theorem.",
 paper = "Avig12a.pdf",
 keywords = "coercion"
}

\end{chunk}

\index{Abraham, Erika}
@inproceedings{Abra15,
 author = "Abraham, Erika",
 title = "Building Bridges between Symbolic Computation and Satisfiability
 Checking",
 booktitle = "ISSAC 15",
 year = "2015",
 pages = "16",
 publisher = "ACM",
 isbn = "9781450334358",
 abstract =
 "The satisfiability problem is the problem of deciding whether a
 logical formula is satisfiable. For firstorder arithmetic theories,
 in the early 20th century some novel solutions in form of decision
 procedures were developed in the area of mathematical logic. With the
 advent of powerful computer architectures, a new research line started
 to develop practically feasible implementations of such decision
 procedures. Since then, symbolic computation has grown to an extremely
 successful scientific area, supporting all kinds of scientific
 computing by efficient computer algebra systems.

 Independently, around 1960 a new technology called SAT solving started
 its career. Restricted to propositional logic, SAT solvers showed to
 be very efficient when employed by formal methods for verification. It
 did not take long till the power of SAT solving for Boolean problems
 had been extended to cover also different theories. Nowadays, fast
 SATmodulotheories (SMT) solvers are available also for arithmetic
 problems.

 Due to their different roots, symbolic computation and SMT solving
 tackle the satisfiability problem differently. We discuss differences
 and similarities in their approaches, highlight potentials of
 combining their strengths, and discuss the challenges that come with
 this task.",
 paper = "Abra15.pdf"
+@misc{Nore08,
+ author = "Norell, Ulf and Chapman, James",
+ title = "Dependently Typed Programming in Agda",
+ link = "\url{http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf}",
+ year = "2008",
+ paper = "Nore08.pdf"
}
\end{chunk}
\index{Abraham, Erika}
+\index{Bidoit, M.}
+\index{Kreowski, H.J.}
+\index{Lescanne, P.}
+\index{Orejas, F.}
+\index{Sannella, D.}
\begin{chunk}{axiom.bib}
@inproceedings{Abra16,
 author = "Abraham, Erika",
 title = "Symbolic Computation Techniques in Satisfiability Checking",
 booktitle = "SYNASC 2016",
 publisher = "IEEE Press",
 year = "2016",
 isbn = "9781509057078",
 pages = "310"
}

\end{chunk}

\index{Kauers, Manuel}
\begin{chunk}{axiom.bib}
@article{Kaue11,
 author = "Kauers, Manuel",
 title = "How to use Cylindrical Algebraic Decomposition",
 journal = {S\'emminaire Lotharingien de Combinatoire},
 volume = "65",
 year = "2011",
 comment = "Article B65a",
+@book{Bido91,
+ author = "Bidoit, M. and Kreowski, H.J. and Lescanne, P. and
+ Orejas, F. and Sannella, D.",
+ title = "Algebraic System Specification and Development",
+ publisher = "SpringerVerlag",
+ comment = "LNCS 501",
+ year = "1991",
+ isbn = "3540540601",
abstract =
 "We take some items from a textbook on inequalities and show how to
 prove them with computer algebra using the Cylindrical Algebraic
 Decomposition algorithm. This is an example collection for standard
 applications of this algorithm, intended as a guide for potential users.",
 paper = "Kaue11.pdf"
}
+ "A great deal of work has been devoted to methods of specification
+ based on the simple idea that a functional program can be modelled as
+ a {\sl manysorted algebra}, i.e. as a number of sets of data values
+ (one set of values for each data type) together with a number of total
+ functions on those sets corresponding to the functions in the
+ program. This abstracts away from the algorithms used to compute the
+ functions and how those algorithms are expressed in a given
+ programming language, focusing instead on the representation of data
+ and the input/output behavior of functions. The pioneering work in
+ this area is [Zil 74],[Gut 75], [GTW 76], of which the latter  the
+ socalled {\sl initial algebra approach}  is the most formal This
+ idea was soon taken up by other workers, see e.g. [GGM 76], [GHM 76],
+ [BG 77], [GHM 78]. Today the field of algebraic specification has
+ grown into one of the major areas of research in theoretical computer
+ science. More than fifteen years of research have led to an abundance
+ of competing and complementary theories and approaches. The algebraic
+ approach provides a conceptual basis, theoretical fundations, and
+ prototype tools for the stepwise formal development of correct system
+ components from their specifications, and thus covers the whole
+ software development process from the specification of requirements to
+ the finished system. These methos are potentially applicable to the
+ development of correct hardware systems as well"
\end{chunk}

\index{Abraham, Erika}
\index{Jebelean, Tudor}
\begin{chunk}{axiom.bib}
@inproceedings{Abra17,
 author = "Abraham, Erika and Jebelean, Tudor",
 title = "Adapting Cylindrical Algebraic Decomposition for Proof Specific
 Tasks",
 booktitle = "IJCAI 2017",
 year = "2017",
 comment = "Extended Abstract",
 paper = "Abra17.pdf"
}
\end{chunk}
\index{Abraham, Erika}
\index{Abbott, John}
\index{Becker, Bernd}
\index{Bigatti, Anna M.}
\index{Brain, Martin}
\index{Cimatti, Alessandro}
\index{Davenport, James H.}
\index{England, Matthew}
\index{Fontaine, Pascal}
\index{Forrest, Stephen}
\index{Ganesh, Vijay}
\index{Griggio, Alberto}
\index{Kroenig, Daniel}
\index{Seiler, Werner M.}
\begin{chunk}{axiom.bib}
@misc{Abraxx,
 author = "Abraham, Erika and Abbott, John and Becker, Bernd and
 Bigatti, Anna M. and Brain, Martin and Cimatti, Alessandro and
 Davenport, James H. and England, Matthew and Fontaine, Pascal
 and Forrest, Stephen and Ganesh, Vijay and Griggio, Alberto and
 Kroenig, Daniel and Seiler, Werner M.",
 title = "SC2 challenges: when Satisfiability Checking and Symbolic
 Computation join forces",
 year = "2017",
 abstract =
 "Symbolic Computation and Satisfiability Checking are two research
 areas, both having their individual scientific focus but with common
 interests, e.g., in the development, implementation and application
 of decision procedures for arithmetic theories. Despite their
 commonalities, the two communities are rather weakly connected. The
 aim of the SC 2 initiative is to strengthen the connection between
 these communities by creating common platforms, initiating interaction
 and exchange, identifying common challenges, and developing a common
 roadmap from theory along the way to tools and (industrial) applications.",
 paper = "Abraxx.pdf"
}

\end{chunk}

\index{de Moura, Leonardo}
\index{Avigad, Jeremy}
\index{Kong, Soonho}
\index{Roux, Cody}
\begin{chunk}{axiom.bib}
@misc{Mour15,
 author = "de Moura, Leonardo and Avigad, Jeremy and Kong, Soonho and
 Roux, Cody",
 title = "Elaboration in Dependent Type Theory",
 year = "2015",
 abstract =
 "To be usable in practice, interactive theorem provers need to provide
 convenient and efficient means of writing expressions, definitions,
 and proofs. This involves inferring information that is often left
 implicit in an ordinary mathematical text, and resolving ambiguities
 in mathematical expressions. We refer to the process of passing from a
 quasiformal and partially specified expression to a completely
 precise formal one as {\sl elaboration}. We describe an elaboration
 algorithms for dependent type theory that has been implemented in the
 Lean theorem prover. Lean's elaborator supports higherorder
 unification, type class inference, ad hoc overloading, insertion of
 coercions, the use of tactics, and the computational reduction of
 terms. The interactions between these components are subtle and
 complex, and the elaboration algorithm has been carefully designed to
 balance efficiency and usability. We describe the central design
 goals, and the means by which they are achieved.",
 paper = "Mour15.pdf",
 keywords = "coercion"
}

\end{chunk}

\index{Reynolds, John C.}
\begin{chunk}{axiom.bib}
@article{Reyn05,
 author = "Reynolds, John C.",
 title = "An Overview of Separation Logic",
 journal = "LNCS",
 volume = "4171",
 pages = "460469",
 abstract =
 "After some general remarks about program verification, we introduce
 separation logic, a novel extension of Hoare logic that can strengthen
 the applicability and scalability of program verification for
 imperative programs that use shared mutable data structures or
 sharedmemory concurrency",
 paper = "Reyn05.pdf",
}

\end{chunk}

\index{Reynolds, John C.}
\begin{chunk}{axiom.bib}
@inproceedings{Reyn02,
 author = "Reynolds, John C.",
 title = "Separation Logic: A Logic for Shared Mutable Data Structures",
 booktitle = "Logic in Computer Science '02",
 year = "2002",
 pages = "5574",
 isbn = "0769514839",
 abstract =
 "In joint work with Peter O'Hearn and others, based on early ideas of
 Burstall, we have developed an extension of Hoare logic that permits
 reasoning about lowlevel imperativeprograms that use shared mutable
 data structure.The simple imperative programming language is extended
 with commands (not expressions) for accessing and modifying shared
 structures, and for explicit allocation and deallocation of
 storage. Assertions are extended by introducing a "separating
 conjunction" that asserts that its subformulas hold for disjoint
 parts of the heap, and a closely related "separating
 implication". Coupled with the inductive definition of predicates on
 abstract data structures, this extension permits the concise and
 flexible description of structures with controlled sharing.In this
 paper, we will survey the current development of this program logic,
 including extensions that permit unrestricted address arithmetic,
 dynamically allocated arrays, and recursive procedures. We will also
 discuss promising future directions.",
 paper = "Reyn02.pdf"
}

\end{chunk}

\index{Hearn, Peter W.O.}
\begin{chunk}{axiom.bib}
@misc{Hear12,
 author = "Hearn, Peter W.O.",
 title = "A Primer on Separation Logic (and Automatic Program
 Verification and Analysis",
 year = "2012",
 abstract =
 "These are the notes to accompany a course at the Marktoberdorf PhD
 summer school in 2011. The course consists of an introduction to
 separation logic, with a slant towards its use in automatic program
 verification and analysis.",
 paper = "Hear12.pdf"
}

\end{chunk}

\index{Kaliszyk, Cezary}
\begin{chunk}{axiom.bib}
@phdthesis{Kali09,
 author = "Kaliszyk, Cezary"
 title = "Correctness and Availability: Building Computer Algebra on top
 of Proof Assistants and making Proof Assistants available over
 the Web",
 year = "2009",
 school = "Radboud University, Nijmegen",
 link = "\url{http://clinformatik.uibk.ac.at/users/cek/docs/09/kaliszyk\_thesis\_webdoc.pdf}",
 abstract =
 "In this thesis we present an approach to extending the usability
 of proof assistants in mathematics and computer science. We do it
 in two ways: by combining proof assistants with computer algebra
 systems and by providing interactive access to such systems on
 the web.",
 paper = "Kali09.pdf"
}

\end{chunk}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 4f4fc89..d166d22 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5824,6 +5824,8 @@ books/bookvol3 Additional explanations and references
add Jerry Archibald, Philip Santas, David Saunders
20170924.01.tpd.patch
books/bookvolbib add references
+20170929.01.tpd.patch
+books/bookvolbib add references

1.9.1