From d1aaa21c9d7133c326384d1e72ff360f826bfbe8 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Mon, 27 Jun 2016 00:05:56 0400
Subject: [PATCH] books/bookvolbib Axiom Citations in the Literature
MIMEVersion: 1.0
ContentType: text/plain; charset=UTF8
ContentTransferEncoding: 8bit
Goal: Axiom Literate Programming
\index{Prevosto, Virgile}
\index{Doligez, Damien}
\begin{chunk}{axiom.bib}
@article{Prev02,
author = "Prevosto, Virgile and Doligez, Damien",
title = "Algorithms and proofs inheritance in the FOC language",
journal = "J. Autom. Reasoning",
volume = "29",
number = "34",
pages = "337363",
keywords = "axiomref",
paper = "Prev02.pdf",
abstract =
"In this paper, we present the FOC language, dedicated to the
development of certified computer algebra libraries (that is sets of
programs). These libraries are based on a hierarchy of implementations
of mathematical structures. After presenting the core set of features
of our language, we describe the static analyses, which reject
inconsistent programs. We then show how we translate FOC definitions
into OCAML and COQ, our target languages for the computational part
and the proof checking, respectively."
}
\end{chunk}
\index{Schwarz, Fritz}
\begin{chunk}{axiom.bib}
@InProceedings{Schw02,
author = "Schwarz, Fritz",
title = "ALLTYPES: An algebraic language and type system",
booktitle = "1st Int. Congress on Mathematical Software",
year = "2002",
isbn = "9812380485",
location = "Beijing China",
pages = "486500",
keywords = "axiomref",
paper = "Schw02.pdf",
url =
"http://www.scai.fraunhofer.de/content/dam/scai/de/documents/MitarbeiterinnenundMitarbeiter/ICMS2002.pdf",
abstract =
"The software system ALLTYPES provides an environment that is
particularly designed for developing software in differential
algebra. Its most important features may be described as follows: A
set of about thirty parametrized algebraic types is defined. Data
objects represented by these types may be manipulated by more than one
hundred polymorphic functions. Reusability of code is achieved by
genericity and multiple inheritance. The user may extend the system by
defining new types and polymorphic functions. A language comprising
seven basic language constructs is defined for implementing
mathematical algorithms. The easy manipulation of types is
particularly supported due to a special portion of the language
dedicated to manipulating typed objects, i.e. for performing
userdefined or automatic type coercions. Type inquiries are also
included in the language."
}
\end{chunk}
\index{Adams, Andrew A.}
\index{Dunstan, Martin}
\index{Gottlieben, Hanne}
\index{Kelsey, Tom}
\index{Martin, Ursula}
\index{Owre, Sam}
\begin{chunk}{axiom.bib}
@InProceedings{Adam01,
author = "Adams, Andrew A. and Dunstan, Martin and Gottlieben, Hanne and
Kelsey, Tom and Martin, Ursula and Owre, Sam",
title = "Computer algebra meets automated theorem proving: Integrating
Maple and PVS",
booktitle = "Theorem proving in higher order logics",
series = "TPHOLs 2001",
year = "2001",
location = "Edinburgh, Scotland",
pages = "2742",
keywords = "axiomref",
paper = "Adam01.pdf",
abstract =
"We describe an interface between version 6 of the Maple computer
algebra system with the PVS automated theorem prover. The interface is
designed to allow Maple users access to the robust and checkable proof
environment of PVS. We also extend this environment by the provision
of a library of proof strategies for use in real analysis. We
demonstrate examples using the interface and the real analysis
library. These examples provide proofs which are both illustrative and
applicable to genuine symbolic computation problems."
}
\end{chunk}
\index{Antoine, Xavier}
\begin{chunk}{axiom.bib}
@article{Anto01,
author = "Antoine, Xavier",
title = "Microlocal diagonalization of strictly hyperbolic pseudodifferential
systems and application to the design of radiation conditions in
electromagnetism",
journal = "SIAM J. Appl. Math",
volume = "61",
number = "6",
pages = "18771905",
year = "2001",
keywords = "axiomref",
abstract =
"In [Commun. Pure Appl. Math. 28, 457478 (1975; Zbl 0332.35058)],
M. E. Taylor described a constructive diagonalization method to
investigate the reflection of singularities of the solution to
firstorder hyperbolic systems. According to further works initiated
by Engquist and Majda, this approach proved to be well adapted to the
construction of artificial boundary conditions. However, in the case
of systems governed by pseudodifferential operators with variable
coefficients, Taylor’s method involves very elaborate calculations of
the symbols of the operators. Hence, a direct approach may be
difficult when dealing with highorder conditions.
This motivates the first part of this paper, where a recursive
explicit formulation of Taylor’s method is stated for microlocally
strictly hyperbolic systems. Consequently, it provides an algorithm
leading to symbolic calculations which can be handled by a computer
algebra system. In the second part, an application of the method is
investigated for the construction of local radiation boundary
conditions on arbitrarily shaped surfaces for the transverse electric
Maxwell system. It is proved that they are of complete order, provided
the introduction of a new symbols class well adapted to the Maxwell
system. Next, a complete secondorder condition is designed, and when
used as an onsurface radiation condition [G. A. Kriegsmann,
A. Taflove, and K. R. Umashankar, IEEE Trans. Antennas Propag. 35,
153161 (1987; Zbl 0947.78571)], it can give rise to an ultrafast
numerical approximate solution of the scattered field."
}
\end{chunk}
\index{Delliere, Stephane}
\begin{chunk}{axiom.bib}
@article{Dell01,
author = "Delliere, Stephane",
title = "On the links between triangular sets and dynamic constructable
closure",
journal = "J. Pure Appl. Algebra",
volume = "163",
number = "1",
pages = "4968",
year = "2001",
keywords = "axiomref",
abstract =
"Two kinds of triangular systems are studied: normalized triangular
polynomial systems (a weaker form of Lazard’s triangular sets
[D. Lazard, Discrete Appl. Math. 33, No. 13, 147160 (1991; Zbl
0753.13013)] and constructible triangular systems (involved in the
dynamic constructible closure programs of T. GomezDíaz [Quelques
applications de l'evaluation dynamique, Ph.D. Thesis, Universite de
Limoges (1994)]. This paper shows that these notions are strongly
related. In particular, combining the two points of view
(constructible and polynomial) on the subject of squarefree
conditions, it allows us to effect dramatic improvements in the
dynamic constructible closure programs."
}
\end{chunk}
\index{Michler, Gerhard O.}
\begin{chunk}{axiom.bib}
@article{Mich01,
author = "Michler, Gerhard O.",
title = "The character values of multiplicityfree irreducible constituents
of a transitive permutation representation",
journal = "Kyushu J. Math.",
volume = "55",
number = "1",
pages = "75106",
year = "2001",
keywords = "axiomref",
url = "https://www.jstage.jst.go.jp/article/kyushujm/55/1/55\_1\_75/\_pdf",
paper = "Mich01.pdf",
abstract =
"Let $G$ be a finite group and $M$ a subgroup of $G$. Let the
permutation character of $G$ on the set of right cosets of $M$ be
denoted by $(1_M)^G$. Any ordinary irreducible constituent of
$(1_M)^G$ with multiplicity one is called a multiplicityfree
constituent of $(1_M)^G$. In the paper under review the author gives
an efficient algorithm to compute the values of any multiplicityfree
constituent of $(1_M)^G$. The character value is in terms of the
double coset decomposition of $M$ and related concepts concerning
intersection matrices. The author uses this algorithm to determine the
values of the multiplicityfree constituents of $(1_C)^{J_1}$, where
$J_1$ is the smallest Janko group of order 175560 and $C$ is the
centralizer of an involution in $J_1$. Using these, he then is able to
compute the character table of $J_1$ which is already known."
}
\end{chunk}
\index{Rudnicki, Piotr}
\index{Schwarzweller, Christoph}
\index{Trybulec, Andrzej}
\begin{chunk}{axiom.bib}
@article{Rudn01,
author = "Rudnicki, Piotr and Schwarzweller, Christoph and
Trybulec, Andrzej",
title = "Commutative algebra in the Mizar system",
journal = "J. Symb. Comput.",
volume = "32",
number = "12",
pages = "143169",
year = "2001",
keywords = "axiomref",
url = "https://inf.ug.edu.pl/~schwarzw/papers/jsc01.pdf",
paper = "Rudn01.pdf",
abstract =
"We report on the development of algebra in the Mizar system. This
includes the construction of formal multivariate power series and
polynomials as well as the definition of ideals up to a proof of the
Hilbert basis theorem. We present how the algebraic structures are
handled and how we inherited the past developments from the Mizar
Mathematical Library (MML). The MML evolves and past contributions are
revised and generalized. Our work on formal power series caused a
number of such revisions. It seems that revising past developments
with an intent to generalize them is a necessity when building a
database of formalized mathematics. This poses a question: how much
generalization is best?"
}
\end{chunk}
\index{Safouhi, Hassan}
\begin{chunk}{axiom.bib}
@article{Safo01,
author = "Safouhi, Hassan",
title = "Numerical evaluation of threecenter twoelectron Coulomb and
hybrid integrals over $B$ functions using the $HD$ and
$H\overline{D}$ methods and convergence properties",
journal = "J. Math. Chem.",
volume = "29",
number = "3",
pages = "213232",
year = "2001",
keywords = "axiomref",
abstract =
"The $B$ function is a product of a spherical $K$ Bessel function and
a spherical harmonic. The integrals to be evaluated contain
complicated expressions of finite hypergeometric functions and
spherical $J$ Bessel functions. Sequence transformation techniques are
used for the numerical evaluation of the integrals. Numerical examples
illustrate the accuracy and the efficiency of the method."
}
\end{chunk}
\index{Thompson, Simon}
\begin{chunk}{ignore}
@InProceedings{Thom01,
author = "Thompson, Simon",
title = "Logic and dependent types in the Aldor Computer Algebra System",
booktitle = "Symbolic computation and automated reasoning",
series = "CALCULEMUS 2000",
year = "2001",
location = "St. Andrews, Scotland",
pages = "205233",
keywords = "axiomref",
paper = "Thom01.pdf",
url = "http://axiomwiki.newsynthesis.org/public/refs/aldorcalc2000.pdf",
abstract = "
We show how the Aldor type system can represent propositions of
firstorder logic, by means of the 'propositions as types'
correspondence. The representation relies on type casts (using
pretend) but can be viewed as a prototype implementation of a modified
type system with {\sl type evaluation} reported elsewhere. The logic
is used to provide an axiomatisation of a number of familiar Aldor
categories as well as a type of vectors."
}
\end{chunk}
\index{Poll, Erik}
\begin{chunk}{axiom.bib}
@misc{Poll99,
author = "Poll, Erik",
title = "The Type System of Axiom",
year = "1999",
url = "http://www.cs.ru.nl/E.Poll/talks/axiom.pdf",
paper = "Poll99.pdf",
keywords = "axiomref",
abstract =
"This is a slide deck from a talk on the correspondence between
Axiom/Aldor types and Logic."
}
\end{chunk}
\index{Poll, Erik}
\index{Thompson, Simon}
\begin{chunk}{axiom.bib}
@misc{Pollxx,
author = "Poll, Erik and Thompson, Simon",
title = "Adding the axioms to Axiom. Toward a system of automated
reasoning in Aldor",
url =
"http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.1457&rep=rep1&type=ps",
paper = "Pollxx.pdf",
keywords = "axiomref",
abstract = "
This paper examines the proposal of using the type system of Axiom to
represent a logic, and thus to use the constructions of Axiom to
handle the logic and represent proofs and propositions, in the same
way as is done in theorem provers based on type theory such as Nuprl
or Coq.
The paper shows an interesting way to decorate Axiom with pre and
postconditions.
The CurryHoward correspondence used is
\begin{verbatim}
PROGRAMMING LOGIC
Type Formula
Program Proof
Product/record type (...,...) Conjunction
Sum/union type \/ Disjunction
Function type > Implication
Dependent function type (x:A) > B(x) Universal quantifier
Dependent product type (x:A,B(x)) Existential quantifier
Empty type Exit Contradictory proposition
One element type Triv True proposition
\end{verbatim}"
}
\end{chunk}
\index{Poll, Erik}
\index{Thompson, Simon}
\begin{chunk}{axiom.bib}
@misc{Poll00,
author = "Poll, Erik and Thompson, Simon",
title = "Integrating Computer Algebra and Reasoning through the Type
System of Aldor",
paper = "P0ll00.pdf",
keywords = "axiomref",
year = "2000",
abstract =
"A number of combinations of reasoning and computer algebra systems
have been proposed; in this paper we describe another, namely a way to
incorporate a logic in the computer algebra system Axiom. We examine
the type system of Aldor  the Axiom Library Compiler  and show
that with some modifications we can use the dependent types of the
system to model a logic, under the CurryHoward isomorphism. We give
a number of example applications of the logic we construct and explain
a prototype implementation of a modified typechecking system written
in Haskell."
}
\end{chunk}
\index{Page, Bill}
\begin{chunk}{axiom.bib}
@misc{Page08,
author = "Page, Bill",
title = "Algebraist Network",
url = "http://lambdatheultimate.org/node/2737",
year = "2008",
keywords = "axiomref"
}
\end{chunk}
\index{Poll, Erik}
\index{Thompson, Simon}
\begin{chunk}{axiom.bib}
@InProceedings{Poll00a,
author = "Poll, Erik and Thompson, Simon",
title = "Integrating Computer Algebra and Reasoning through the Type
System of Aldor",
booktitle = "Frontiers of Combining Systems",
series = "Lecture Notes in Artificial Intelligence",
year = "2000",
isbn = "3540672818",
location = "Nancy, France",
pages = "136150",
keywords = "axiomref"
}
\end{chunk}
\index{Davenport, James H.}
\begin{chunk}{axiom.bib}
@InProceedings{Dave00,
author = "Davenport, James H.",
title = "Abstract data types in computer algebra",
booktitle = "Mathematical foundations of computer science",
series = "MFCS 2000",
year = "2000",
location = "Bratislava, Slovakia",
pages = "2135",
keywords = "axiomref",
abstract =
"The theory of abstract data types was developed in the late 1970s and
the 1980s by several people, including the ``ADJ'' group, whose work
influenced the design of Axiom. One practical manifestation of this
theory was the OBJ3 system. An area of computing that cries out for
this approach is computer algebra, where the objects of discourse are
mathematical, generally satisfying various algebraic rules. There have
been various theoretical studies of this in the literature. The aim of
this paper is to report on the practical applications of this theory
within computer algebra, and also to outline some of the theoretical
issues raised by this practical application. We also give a
substantial bibliography."
}
\end{chunk}
\index{Weber, Andreas}
\begin{chunk}{axiom.bib}
@phdthesis{Webe93b,
author = "Weber, Andreas",
title = "Type Systems for Computer Algebra",
school = "University of Tubingen",
year = "1993",
paper = "Webe93b.pdf",
keywords = "axiomref",
abstract =
"An important feature of modern computer algebra systems is the support
of a rich type system with the possibility of type inference. Basic
features of such a type system are polymorphism and coercion between
types. Recently the use of ordersorted rewrite systems was proposed
as a general framework. We will give a quite simple example of a
family of types arising in computer algebra whose coercion relations
cannot be captured by a finite set of firstorder rewrite rules."
}
\end{chunk}
\index{Fateman, Richard J.}
\begin{chunk}{axiom.bib}
@InProceedings{Fate00,
author = "Fateman, Richard J.",
title = "Problem solving environments and symbolic computing",
booktitle = "Enabling technologies for computational science",
publisher = "Kluwer Academic Publishers",
year = "2000",
pages = "91102",
keywords = "axiomref",
paper = "Fate00.pdf",
url = "http://people.eecs.berkeley.edu/~fateman/papers/psekluwer.pdf",
abstract =
"What role should be played by symbolic mathematical computation
facilities in scientific and engineering ``problem solving
environments''? Drawing upon standard facilities such as numerical and
graphical libraries, symbolic computation should be useful for: The
creation and manipulation of mathematical models; The production of
custom optimized numerical software; The solution of delicate classes
of mathematical problems that require handling beyond that available
in traditional machinesupported floatingpoint computation. Symbolic
representation and manipulation can potentially play a central
organizing role in PSEs since their more general object representation
allows a program to deal with a wider range of computational
issues. In particular numerical, graphical, and other processing can
be viewed as special cases of symbolic manipulation with interactive
symbolic computing providing both an organizing backbone and the
communication ``glue'' among otherwise dissimilar components"
}
\end{chunk}
\index{Hoang, Ngoc Minh}
\index{Petitot, Michel}
\index{Van er Hoeven, Joris}
\begin{chunk}{axiom.bib}
@article{Hoan00,
author = "Hoang, Ngoc Minh and Petitot, Michel and Van er Hoeven, Joris",
title = "Shuffle algebra and polylogarithms",
journal = "Discrete Math.",
volume = "225",
number = "13",
pages = "217230",
year = "2000",
keywords = "axiomref",
paper = "Hoan00.pdf",
abstract =
"Generalized polylogarithms are defined as iterated integrals with
respect to the two differential forms $\omega_0=\frac{dz}{z}$ and
$\omega_1=\frac{dz}{(1z)}$. We give an algorithm which computes the
monodromy of these special functions. This algorithm, implemented in
AXIOM, is based on the computation of the associator $\Phi_{KZ}$ of
Drinfel’d, in factorized form. The monodromy formulae involve special
constants, called multiple zeta values. We prove that the algebra of
polylogarithms is isomorphic to a shuffle algebra."
}
\end{chunk}
\index{Raab, C.G.}
\begin{chunk}{axiom.bib}
@article{Raab13,
author = "Raab, C.G.",
title = "Generalization of Risch's Algorithm to Special Functions",
journal = "CoRR",
volume = "abs/1305.1481",
year = "2013",
url = "http://arxiv.org/pdf/1305.1481v1.pdf",
paper = "Raab13.pdf",
abstract =
"Symbolic integration deals with the evaluation of integrals in closed
form. We present an overview of Risch's algorithm including recent
developments. The algorithms discussed are suited for both indefinite
and definite integration. They can also be used to compute linear
relations among integrals and to find identities for special functions
given by parameter integrals. The aim of this presentation is twofold:
to introduce the reader to some basic ideas of differential algebra in
the context of integration and to raise awareness in the physics
community of computer algebra algorithms for indefinite and definite
integration. "
}
\end{chunk}
\index{Houstis, Elias N.}
\index{Rice, John R.}
\begin{chunk}{axiom.bib}
@article{Hous00,
author = "Houstis, Elias N. and Rice, John R.",
title = "Future problem solving environments for computational science",
journal = "Math. Comput. Simul.",
volume = "54",
number = "45",
pages = "243257",
year = "2000",
keywords = "axiomref",
abstract =
"We review the current state of the Problem Solving Environment (PSE)
field and make projections for the future. First, we describe the
computing context, the definition of a PSE and the goals of a PSE. The
stateoftheart is summarized along with the principal components and
paradigms for building PSEs. The discussion of the future is given in
three parts: future trends, scenarios for 2010/2025, and research
issues to be addressed."
}
\end{chunk}
\index{Gallopoulos, Stratis}
\index{Houstis, Elias}
\index{Rice, John}
\begin{chunk}{axiom.bib}
@techreport{Gall92,
author = "Gallopoulos, Stratis and Houstis, Elias and Rice, John",
title = "Future Research Directions in Problem Solving Environments for
Computational Science",
institution = "Purdue University",
year = "1992",
type = "technical report",
number = "CSDTR92032",
paper = "Gall92.pdf",
url =
"http://docs.lib.purdue.edu/cgi/viewcontent.cgi?article=1953\&context=cstech",
keywords = "axiomref",
abstract =
"During the early 19605 some were visualizing that computers could
provide a powerful problem solving environment (PSE) which would
interact with scientists on their own terms. By the mid 1960s there
were many attempts underway to create these PSEs, but the early
1970s almost all of these attempts had been abandoned, because the
technological infrastructure could not yet support PSEs in
computational science. The dream of the 1960s can be the reality of
the 1990s; high performance computers combined with better
understanding of computing and computational science have put PSEs
well within our reach."
}
\end{chunk}

books/bookvolbib.pamphlet  723 ++++++++++++++++++++++++++++++++
changelog  2 +
patch  618 +++++++++++++++++++++++++++++
src/axiomwebsite/patches.html  2 +
4 files changed, 1124 insertions(+), 221 deletions()
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 77d5e71..f44bc7a 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 3763,15 +3763,21 @@ Martin, U.
\index{Kelsey, Tom}
\index{Martin, Ursula}
\index{Owre, Sam}
\begin{chunk}{ignore}
\bibitem[Adams 01]{Adam01} Adams, Andrew; Dunstan, Martin; Gottliebsen, Hanne;
Kelsey, Tom; Martin, Ursula; Owre, Sam
 title = "Computer Algebra Meets Automated Theorem Proving:
 Integrating Maple and PVS",
 url = "http://www.csl.sri.com/~owre/papers/tphols01/tphols01.pdf",
+\begin{chunk}{axiom.bib}
+@InProceedings{Adam01,
+ author = "Adams, Andrew A. and Dunstan, Martin and Gottlieben, Hanne and
+ Kelsey, Tom and Martin, Ursula and Owre, Sam",
+ title = "Computer algebra meets automated theorem proving: Integrating
+ Maple and PVS",
+ booktitle = "Theorem proving in higher order logics",
+ series = "TPHOLs 2001",
+ year = "2001",
+ location = "Edinburgh, Scotland",
+ pages = "2742",
+ keywords = "axiomref",
paper = "Adam01.pdf",
 abstract = "
 We describe an interface between version 6 of the Maple computer
+ abstract =
+ "We describe an interface between version 6 of the Maple computer
algebra system with the PVS automated theorem prover. The interface is
designed to allow Maple users access to the robust and checkable proof
environment of PVS. We also extend this environment by the provision
@@ 3779,6 +3785,7 @@ Kelsey, Tom; Martin, Ursula; Owre, Sam
demonstrate examples using the interface and the real analysis
library. These examples provide proofs which are both illustrative and
applicable to genuine symbolic computation problems."
+}
\end{chunk}
@@ 4105,6 +4112,111 @@ Kelsey, Tom; Martin, Ursula; Owre, Sam
\end{chunk}
+\index{Poll, Erik}
+\index{Thompson, Simon}
+\begin{chunk}{axiom.bib}
+@misc{Pollxx,
+ author = "Poll, Erik and Thompson, Simon",
+ title = "Adding the axioms to Axiom. Toward a system of automated
+ reasoning in Aldor",
+ url =
+"http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.1457&rep=rep1&type=ps",
+ paper = "Pollxx.pdf",
+ keywords = "axiomref",
+ abstract = "
+ This paper examines the proposal of using the type system of Axiom to
+ represent a logic, and thus to use the constructions of Axiom to
+ handle the logic and represent proofs and propositions, in the same
+ way as is done in theorem provers based on type theory such as Nuprl
+ or Coq.
+
+ The paper shows an interesting way to decorate Axiom with pre and
+ postconditions.
+
+ The CurryHoward correspondence used is
+ \begin{verbatim}
+ PROGRAMMING LOGIC
+ Type Formula
+ Program Proof
+ Product/record type (...,...) Conjunction
+ Sum/union type \/ Disjunction
+ Function type > Implication
+ Dependent function type (x:A) > B(x) Universal quantifier
+ Dependent product type (x:A,B(x)) Existential quantifier
+ Empty type Exit Contradictory proposition
+ One element type Triv True proposition
+ \end{verbatim}"
+}
+
+\end{chunk}
+
+\index{Poll, Erik}
+\index{Thompson, Simon}
+\begin{chunk}{axiom.bib}
+@misc{Poll00,
+ author = "Poll, Erik and Thompson, Simon",
+ title = "Integrating Computer Algebra and Reasoning through the Type
+ System of Aldor",
+ paper = "P0ll00.pdf",
+ keywords = "axiomref",
+ year = "2000",
+ abstract =
+ "A number of combinations of reasoning and computer algebra systems
+ have been proposed; in this paper we describe another, namely a way to
+ incorporate a logic in the computer algebra system Axiom. We examine
+ the type system of Aldor  the Axiom Library Compiler  and show
+ that with some modifications we can use the dependent types of the
+ system to model a logic, under the CurryHoward isomorphism. We give
+ a number of example applications of the logic we construct and explain
+ a prototype implementation of a modified typechecking system written
+ in Haskell."
+}
+
+\end{chunk}
+
+\index{Poll, Erik}
+\index{Thompson, Simon}
+\begin{chunk}{axiom.bib}
+@InProceedings{Poll00a,
+ author = "Poll, Erik and Thompson, Simon",
+ title = "Integrating Computer Algebra and Reasoning through the Type
+ System of Aldor",
+ booktitle = "Frontiers of Combining Systems",
+ series = "Lecture Notes in Artificial Intelligence",
+ year = "2000",
+ isbn = "3540672818",
+ location = "Nancy, France",
+ pages = "136150",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
+\index{Prevosto, Virgile}
+\index{Doligez, Damien}
+\begin{chunk}{axiom.bib}
+@article{Prev02,
+ author = "Prevosto, Virgile and Doligez, Damien",
+ title = "Algorithms and proofs inheritance in the FOC language",
+ journal = "J. Autom. Reasoning",
+ volume = "29",
+ number = "34",
+ pages = "337363",
+ keywords = "axiomref",
+ paper = "Prev02.pdf",
+ abstract =
+ "In this paper, we present the FOC language, dedicated to the
+ development of certified computer algebra libraries (that is sets of
+ programs). These libraries are based on a hierarchy of implementations
+ of mathematical structures. After presenting the core set of features
+ of our language, we describe the static analyses, which reject
+ inconsistent programs. We then show how we translate FOC definitions
+ into OCAML and COQ, our target languages for the computational part
+ and the proof checking, respectively."
+}
+
+\end{chunk}
+
\index{Lamport, Leslie}
\begin{chunk}{axiom.bib}
@misc{TLA16,
@@ 4284,6 +4396,38 @@ Kelsey, Tom; Martin, Ursula; Owre, Sam
\end{chunk}
+\index{Rudnicki, Piotr}
+\index{Schwarzweller, Christoph}
+\index{Trybulec, Andrzej}
+\begin{chunk}{axiom.bib}
+@article{Rudn01,
+ author = "Rudnicki, Piotr and Schwarzweller, Christoph and
+ Trybulec, Andrzej",
+ title = "Commutative algebra in the Mizar system",
+ journal = "J. Symb. Comput.",
+ volume = "32",
+ number = "12",
+ pages = "143169",
+ year = "2001",
+ keywords = "axiomref",
+ url = "https://inf.ug.edu.pl/~schwarzw/papers/jsc01.pdf",
+ paper = "Rudn01.pdf",
+ abstract =
+ "We report on the development of algebra in the Mizar system. This
+ includes the construction of formal multivariate power series and
+ polynomials as well as the definition of ideals up to a proof of the
+ Hilbert basis theorem. We present how the algebraic structures are
+ handled and how we inherited the past developments from the Mizar
+ Mathematical Library (MML). The MML evolves and past contributions are
+ revised and generalized. Our work on formal power series caused a
+ number of such revisions. It seems that revising past developments
+ with an intent to generalize them is a necessity when building a
+ database of formalized mathematics. This poses a question: how much
+ generalization is best?"
+}
+
+\end{chunk}
+
\index{Th\'ery, Laurent}
\begin{chunk}{axiom.bib}
@article{Ther01,
@@ 4842,14 +4986,18 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\end{chunk}
\index{Poll, Erik}
\begin{chunk}{ignore}
\bibitem[Poll 99a]{P99a} Poll, Erik
+\begin{chunk}{axiom.bib}
+@misc{Poll99,
+ author = "Poll, Erik",
title = "The Type System of Axiom",
+ year = "1999",
url = "http://www.cs.ru.nl/E.Poll/talks/axiom.pdf",
 paper = "P99a.pdf",
 abstract = "
 This is a slide deck from a talk on the correspondence between
+ paper = "Poll99.pdf",
+ keywords = "axiomref",
+ abstract =
+ "This is a slide deck from a talk on the correspondence between
Axiom/Aldor types and Logic."
+}
\end{chunk}
@@ 4868,60 +5016,6 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\end{chunk}
\index{Poll, Erik}
\index{Thompson, Simon}
\begin{chunk}{ignore}
\bibitem[Poll (a)]{PTxx} Poll, Erik; Thompson, Simon
 title = "Adding the axioms to Axiom. Toward a system of automated reasoning in Aldor",
 url = "http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.1457&rep=rep1&type=ps",
 paper = "PTxx.pdf",
 keywords = "axiomref",
 abstract = "
 This paper examines the proposal of using the type system of Axiom to
 represent a logic, and thus to use the constructions of Axiom to
 handle the logic and represent proofs and propositions, in the same
 way as is done in theorem provers based on type theory such as Nuprl
 or Coq.

 The paper shows an interesting way to decorate Axiom with pre and
 postconditions.

 The CurryHoward correspondence used is
 \begin{verbatim}
 PROGRAMMING LOGIC
 Type Formula
 Program Proof
 Product/record type (...,...) Conjunction
 Sum/union type \/ Disjunction
 Function type > Implication
 Dependent function type (x:A) > B(x) Universal quantifier
 Dependent product type (x:A,B(x)) Existential quantifier
 Empty type Exit Contradictory proposition
 One element type Triv True proposition
 \end{verbatim}"

\end{chunk}

\index{Poll, Erik}
\index{Thompson, Simon}
\begin{chunk}{ignore}
\bibitem[Poll 00]{PT00} Poll, Erik; Thompson, Simon
 title = "Integrating Computer Algebra and Reasoning through the Type System of Aldor",
 paper = "PT00.pdf",
 keywords = "axiomref",
 abstract = "
 A number of combinations of reasoning and computer algebra systems
 have been proposed; in this paper we describe another, namely a way to
 incorporate a logic in the computer algebra system Axiom. We examine
 the type system of Aldor  the Axiom Library Compiler  and show
 that with some modifications we can use the dependent types of the
 system to model a logic, under the CurryHoweard isomorphism. We give
 a number of example applications of the logi we construct and explain
 a prototype implementation of a modified typechecking system written
 in Haskell."

\end{chunk}

\index{Roberts, Siobhan}
\begin{chunk}{axiom.bib}
@misc{Robe15,
@@ 9933,6 +10027,31 @@ J. Symbolic Computation 5, 237259 (1988)
\end{chunk}
+\index{Raab, C.G.}
+\begin{chunk}{axiom.bib}
+@article{Raab13,
+ author = "Raab, C.G.",
+ title = "Generalization of Risch's Algorithm to Special Functions",
+ journal = "CoRR",
+ volume = "abs/1305.1481",
+ year = "2013",
+ url = "http://arxiv.org/pdf/1305.1481v1.pdf",
+ paper = "Raab13.pdf",
+ abstract =
+ "Symbolic integration deals with the evaluation of integrals in closed
+ form. We present an overview of Risch's algorithm including recent
+ developments. The algorithms discussed are suited for both indefinite
+ and definite integration. They can also be used to compute linear
+ relations among integrals and to find identities for special functions
+ given by parameter integrals. The aim of this presentation is twofold:
+ to introduce the reader to some basic ideas of differential algebra in
+ the context of integration and to raise awareness in the physics
+ community of computer algebra algorithms for indefinite and definite
+ integration. "
+}
+
+\end{chunk}
+
\index{Samadani, M.}
\index{Kaltofen, Erich}
\begin{chunk}{axiom.bib}
@@ 10472,6 +10591,49 @@ J. Symbolic Computation 5, 237259 (1988)
\end{chunk}
+\index{Antoine, Xavier}
+\begin{chunk}{axiom.bib}
+@article{Anto01,
+ author = "Antoine, Xavier",
+ title = "Microlocal diagonalization of strictly hyperbolic pseudodifferential
+ systems and application to the design of radiation conditions in
+ electromagnetism",
+ journal = "SIAM J. Appl. Math",
+ volume = "61",
+ number = "6",
+ pages = "18771905",
+ year = "2001",
+ keywords = "axiomref",
+ abstract =
+ "In [Commun. Pure Appl. Math. 28, 457478 (1975; Zbl 0332.35058)],
+ M. E. Taylor described a constructive diagonalization method to
+ investigate the reflection of singularities of the solution to
+ firstorder hyperbolic systems. According to further works initiated
+ by Engquist and Majda, this approach proved to be well adapted to the
+ construction of artificial boundary conditions. However, in the case
+ of systems governed by pseudodifferential operators with variable
+ coefficients, Taylor’s method involves very elaborate calculations of
+ the symbols of the operators. Hence, a direct approach may be
+ difficult when dealing with highorder conditions.
+
+ This motivates the first part of this paper, where a recursive
+ explicit formulation of Taylor’s method is stated for microlocally
+ strictly hyperbolic systems. Consequently, it provides an algorithm
+ leading to symbolic calculations which can be handled by a computer
+ algebra system. In the second part, an application of the method is
+ investigated for the construction of local radiation boundary
+ conditions on arbitrarily shaped surfaces for the transverse electric
+ Maxwell system. It is proved that they are of complete order, provided
+ the introduction of a new symbols class well adapted to the Maxwell
+ system. Next, a complete secondorder condition is designed, and when
+ used as an onsurface radiation condition [G. A. Kriegsmann,
+ A. Taflove, and K. R. Umashankar, IEEE Trans. Antennas Propag. 35,
+ 153161 (1987; Zbl 0947.78571)], it can give rise to an ultrafast
+ numerical approximate solution of the scattered field."
+}
+
+\end{chunk}
+
\index{Augot, D.}
\index{Charpin, P.}
\index{Sendrier, N.}
@@ 11999,6 +12161,33 @@ Academic Press, New York, NY, USA, 1988, ISBN 0122042329
\index{Davenport, James H.}
\begin{chunk}{axiom.bib}
+@InProceedings{Dave00,
+ author = "Davenport, James H.",
+ title = "Abstract data types in computer algebra",
+ booktitle = "Mathematical foundations of computer science",
+ series = "MFCS 2000",
+ year = "2000",
+ location = "Bratislava, Slovakia",
+ pages = "2135",
+ keywords = "axiomref",
+ abstract =
+ "The theory of abstract data types was developed in the late 1970s and
+ the 1980s by several people, including the ``ADJ'' group, whose work
+ influenced the design of Axiom. One practical manifestation of this
+ theory was the OBJ3 system. An area of computing that cries out for
+ this approach is computer algebra, where the objects of discourse are
+ mathematical, generally satisfying various algebraic rules. There have
+ been various theoretical studies of this in the literature. The aim of
+ this paper is to report on the practical applications of this theory
+ within computer algebra, and also to outline some of the theoretical
+ issues raised by this practical application. We also give a
+ substantial bibliography."
+}
+
+\end{chunk}
+
+\index{Davenport, James H.}
+\begin{chunk}{axiom.bib}
@article{Dave02,
author = "Davenport, James H.",
title = "Equality in computer algebra and beyond",
@@ 12228,6 +12417,34 @@ May 1984
\end{chunk}
+\index{Delliere, Stephane}
+\begin{chunk}{axiom.bib}
+@article{Dell01,
+ author = "Delliere, Stephane",
+ title = "On the links between triangular sets and dynamic constructable
+ closure",
+ journal = "J. Pure Appl. Algebra",
+ volume = "163",
+ number = "1",
+ pages = "4968",
+ year = "2001",
+ keywords = "axiomref",
+ abstract =
+ "Two kinds of triangular systems are studied: normalized triangular
+ polynomial systems (a weaker form of Lazard’s triangular sets
+ [D. Lazard, Discrete Appl. Math. 33, No. 13, 147160 (1991; Zbl
+ 0753.13013)] and constructible triangular systems (involved in the
+ dynamic constructible closure programs of T. GomezDíaz [Quelques
+ applications de l'evaluation dynamique, Ph.D. Thesis, Universite de
+ Limoges (1994)]. This paper shows that these notions are strongly
+ related. In particular, combining the two points of view
+ (constructible and polynomial) on the subject of squarefree
+ conditions, it allows us to effect dramatic improvements in the
+ dynamic constructible closure programs."
+}
+
+\end{chunk}
+
\index{Dewar, Mike C.}
\begin{chunk}{ignore}
\bibitem[Dewar 94]{Dew94} Dewar, M. C.
@@ 12601,6 +12818,38 @@ In Watanabe and Nagata [WN90], pp6067 ISBN 0897914015 LCCN QA76.95.I57 1990
\end{chunk}
\index{Fateman, Richard J.}
+\begin{chunk}{axiom.bib}
+@InProceedings{Fate00,
+ author = "Fateman, Richard J.",
+ title = "Problem solving environments and symbolic computing",
+ booktitle = "Enabling technologies for computational science",
+ publisher = "Kluwer Academic Publishers",
+ year = "2000",
+ pages = "91102",
+ keywords = "axiomref",
+ paper = "Fate00.pdf",
+ url = "http://people.eecs.berkeley.edu/~fateman/papers/psekluwer.pdf",
+ abstract =
+ "What role should be played by symbolic mathematical computation
+ facilities in scientific and engineering ``problem solving
+ environments''? Drawing upon standard facilities such as numerical and
+ graphical libraries, symbolic computation should be useful for: The
+ creation and manipulation of mathematical models; The production of
+ custom optimized numerical software; The solution of delicate classes
+ of mathematical problems that require handling beyond that available
+ in traditional machinesupported floatingpoint computation. Symbolic
+ representation and manipulation can potentially play a central
+ organizing role in PSEs since their more general object representation
+ allows a program to deal with a wider range of computational
+ issues. In particular numerical, graphical, and other processing can
+ be viewed as special cases of symbolic manipulation with interactive
+ symbolic computing providing both an organizing backbone and the
+ communication ``glue'' among otherwise dissimilar components"
+}
+
+\end{chunk}
+
+\index{Fateman, Richard J.}
\begin{chunk}{ignore}
\bibitem[Fateman 05]{Fat05} Fateman, R. J.
title = "An incremental approach to building a mathematical expert out of software",
@@ 12817,6 +13066,37 @@ Strasbourg, France, 1990 31pp
\subsection{G} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Gallopoulos, Stratis}
+\index{Houstis, Elias}
+\index{Rice, John}
+\begin{chunk}{axiom.bib}
+@techreport{Gall92,
+ author = "Gallopoulos, Stratis and Houstis, Elias and Rice, John",
+ title = "Future Research Directions in Problem Solving Environments for
+ Computational Science",
+ institution = "Purdue University",
+ year = "1992",
+ type = "technical report",
+ number = "CSDTR92032",
+ paper = "Gall92.pdf",
+ url =
+"http://docs.lib.purdue.edu/cgi/viewcontent.cgi?article=1953\&context=cstech",
+ keywords = "axiomref",
+ abstract =
+ "During the early 19605 some were visualizing that computers could
+ provide a powerful problem solving environment (PSE) which would
+ interact with scientists on their own terms. By the mid 1960s there
+ were many attempts underway to create these PSEs, but the early
+ 1970s almost all of these attempts had been abandoned, because the
+ technological infrastructure could not yet support PSEs in
+ computational science. The dream of the 1960s can be the reality of
+ the 1990s; high performance computers combined with better
+ understanding of computing and computational science have put PSEs
+ well within our reach."
+}
+
+\end{chunk}
+
\index{Gebauer, R{\"u}diger}
\index{M{\"o}ller, H. Michael}
\begin{chunk}{ignore}
@@ 13360,6 +13640,33 @@ Vol. 8 No. 3 pp195210 (2001)
\end{chunk}
+\index{Hoang, Ngoc Minh}
+\index{Petitot, Michel}
+\index{Van er Hoeven, Joris}
+\begin{chunk}{axiom.bib}
+@article{Hoan00,
+ author = "Hoang, Ngoc Minh and Petitot, Michel and Van er Hoeven, Joris",
+ title = "Shuffle algebra and polylogarithms",
+ journal = "Discrete Math.",
+ volume = "225",
+ number = "13",
+ pages = "217230",
+ year = "2000",
+ keywords = "axiomref",
+ paper = "Hoan00.pdf",
+ abstract =
+ "Generalized polylogarithms are defined as iterated integrals with
+ respect to the two differential forms $\omega_0=\frac{dz}{z}$ and
+ $\omega_1=\frac{dz}{(1z)}$. We give an algorithm which computes the
+ monodromy of these special functions. This algorithm, implemented in
+ AXIOM, is based on the computation of the associator $\Phi_{KZ}$ of
+ Drinfel’d, in factorized form. The monodromy formulae involve special
+ constants, called multiple zeta values. We prove that the algebra of
+ polylogarithms is isomorphic to a shuffle algebra."
+}
+
+\end{chunk}
+
\index{Hoarau, Emma}
\index{David, Claire}
\begin{chunk}{axiom.bib}
@@ 13475,6 +13782,30 @@ SpringerVerlag, Berlin, Germany / Heildelberg, Germany / London, UK / etc.,
\end{chunk}
+\index{Houstis, Elias N.}
+\index{Rice, John R.}
+\begin{chunk}{axiom.bib}
+@article{Hous00,
+ author = "Houstis, Elias N. and Rice, John R.",
+ title = "Future problem solving environments for computational science",
+ journal = "Math. Comput. Simul.",
+ volume = "54",
+ number = "45",
+ pages = "243257",
+ year = "2000",
+ keywords = "axiomref",
+ abstract =
+ "We review the current state of the Problem Solving Environment (PSE)
+ field and make projections for the future. First, we describe the
+ computing context, the definition of a PSE and the goals of a PSE. The
+ stateoftheart is summarized along with the principal components and
+ paradigms for building PSEs. The discussion of the future is given in
+ three parts: future trends, scenarios for 2010/2025, and research
+ issues to be addressed."
+}
+
+\end{chunk}
+
\subsection{J} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Jacob, G.}
@@ 13803,6 +14134,15 @@ In ACM [ACM94], pp3240 ISBN 0897916387 LCCN QA76.95.I59 1994
\end{chunk}
+\index{Joswig, Rainer}
+\begin{chunk}{ignore}
+\bibitem[Rainer 14]{Rain14} Joswig, Rainer
+ title = "2014: 30+ Years Common Lisp the Language",
+ url = "http://lispm.de/30ycltl",
+ keywords = "axiomref",
+
+\end{chunk}
+
\index{Joyner, David}
\begin{chunk}{axiom.bib}
@article{Joyn08,
@@ 14750,6 +15090,18 @@ CODEN AJPIAS ISSN 00029505
\end{chunk}
+\index{Page, Bill}
+\begin{chunk}{axiom.bib}
+@misc{Page08,
+ author = "Page, Bill",
+ title = "Algebraist Network",
+ url = "http://lambdatheultimate.org/node/2737",
+ year = "2008",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
\subsection{M} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Mahboubi, Assia}
@@ 14838,6 +15190,38 @@ CoED, 10(1) pp7176, JanuaryMarch 1990 CODEN CWLJDP ISSN 07368607
\end{chunk}
+\index{Michler, Gerhard O.}
+\begin{chunk}{axiom.bib}
+@article{Mich01,
+ author = "Michler, Gerhard O.",
+ title = "The character values of multiplicityfree irreducible constituents
+ of a transitive permutation representation",
+ journal = "Kyushu J. Math.",
+ volume = "55",
+ number = "1",
+ pages = "75106",
+ year = "2001",
+ keywords = "axiomref",
+ url = "https://www.jstage.jst.go.jp/article/kyushujm/55/1/55\_1\_75/\_pdf",
+ paper = "Mich01.pdf",
+ abstract =
+ "Let $G$ be a finite group and $M$ a subgroup of $G$. Let the
+ permutation character of $G$ on the set of right cosets of $M$ be
+ denoted by $(1_M)^G$. Any ordinary irreducible constituent of
+ $(1_M)^G$ with multiplicity one is called a multiplicityfree
+ constituent of $(1_M)^G$. In the paper under review the author gives
+ an efficient algorithm to compute the values of any multiplicityfree
+ constituent of $(1_M)^G$. The character value is in terms of the
+ double coset decomposition of $M$ and related concepts concerning
+ intersection matrices. The author uses this algorithm to determine the
+ values of the multiplicityfree constituents of $(1_C)^{J_1}$, where
+ $J_1$ is the smallest Janko group of order 175560 and $C$ is the
+ centralizer of an involution in $J_1$. Using these, he then is able to
+ compute the character table of $J_1$ which is already known."
+}
+
+\end{chunk}
+
\index{Miola, A.}
\begin{chunk}{ignore}
\bibitem[Miola 90]{Mio90} Miola, A. (ed)
@@ 15322,6 +15706,19 @@ A281 1986 ACM order number 505860
\subsection{R} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Ralston, Anthony}
+\index{Rabinowitz, Philip}
+\begin{chunk}{axiom.bib}
+@book{Rals78,
+ author = "Ralston, Anthony and Rabinowitz, Philip",
+ title = "A First Course in Numerical Analysis",
+ year = "1978",
+ publisher = "McGrawHill",
+ isbn = "0070511586",
+}
+
+\end{chunk}
+
\index{Rioboo, Renaud}
\begin{chunk}{axiom.bib}
@article{Riob09,
@@ 15350,6 +15747,37 @@ A281 1986 ACM order number 505860
\end{chunk}
+\index{Rioboo, Renaud}
+\begin{chunk}{ignore}
+\bibitem[Rioboo 03a]{Riob03a} Rioboo, Renaud
+ title = "Quelques aspects du calcul exact avec des nombres r\'eels",
+Ph.D. Thesis, Laboratoire d'Informatique Th\'eorique et Programmationg
+ paper = "Riob03a.ps",
+ paper = "Riob03a.pdf",
+ keywords = "axiomref",
+
+\end{chunk}
+
+\index{Rioboo, Renaud}
+\begin{chunk}{ignore}
+\bibitem[Rioboo 03]{Riob03} Rioboo, Renaud
+ title = "Towards Faster Real Algebraic Numbers",
+J. of Symbolic Computation 36 pp 513533 (2003)
+ paper = "Riob03.pdf",
+ keywords = "axiomref",
+ abstract = "
+ This paper presents a new encoding scheme for real algebraic number
+ manipulations which enhances current Axiom's real closure. Algebraic
+ manipulations are performed using different instantiations of
+ subresultantlike algorithms instead of Euclideanlike algorithms.
+ We use these algorithms to compute polynomial gcds and Bezout
+ relations, to compute the roots and the signs of algebraic
+ numbers. This allows us to work in the ring of real algebraic integers
+ instead of the field of read algebraic numbers avoiding many
+ denominators."
+
+\end{chunk}
+
\index{RoanesLozano, Eugenio}
\index{RoanesMacias, Eugenio}
\index{VillarMena, M.}
@@ 15459,59 +15887,6 @@ A281 1986 ACM order number 505860
\end{chunk}
\index{Joswig, Rainer}
\begin{chunk}{ignore}
\bibitem[Rainer 14]{Rain14} Joswig, Rainer
 title = "2014: 30+ Years Common Lisp the Language",
 url = "http://lispm.de/30ycltl",
 keywords = "axiomref",

\end{chunk}

\index{Ralston, Anthony}
\index{Rabinowitz, Philip}
\begin{chunk}{axiom.bib}
@book{Rals78,
 author = "Ralston, Anthony and Rabinowitz, Philip",
 title = "A First Course in Numerical Analysis",
 year = "1978",
 publisher = "McGrawHill",
 isbn = "0070511586",
}

\end{chunk}

\index{Rioboo, Renaud}
\begin{chunk}{ignore}
\bibitem[Rioboo 03a]{Riob03a} Rioboo, Renaud
 title = "Quelques aspects du calcul exact avec des nombres r\'eels",
Ph.D. Thesis, Laboratoire d'Informatique Th\'eorique et Programmationg
 paper = "Riob03a.ps",
 paper = "Riob03a.pdf",
 keywords = "axiomref",

\end{chunk}

\index{Rioboo, Renaud}
\begin{chunk}{ignore}
\bibitem[Rioboo 03]{Riob03} Rioboo, Renaud
 title = "Towards Faster Real Algebraic Numbers",
J. of Symbolic Computation 36 pp 513533 (2003)
 paper = "Riob03.pdf",
 keywords = "axiomref",
 abstract = "
 This paper presents a new encoding scheme for real algebraic number
 manipulations which enhances current Axiom's real closure. Algebraic
 manipulations are performed using different instantiations of
 subresultantlike algorithms instead of Euclideanlike algorithms.
 We use these algorithms to compute polynomial gcds and Bezout
 relations, to compute the roots and the signs of algebraic
 numbers. This allows us to work in the ring of real algebraic integers
 instead of the field of read algebraic numbers avoiding many
 denominators."

\end{chunk}

\index{Robidoux, Nicolas}
\begin{chunk}{ignore}
\bibitem[Robidoux 93]{Rob93} Robidoux, Nicolas
@@ 15547,6 +15922,30 @@ Mathematik und Physik, 75 (suppl. 2):S435S438, 1995 ISSN 00442267
\subsection{S} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Safouhi, Hassan}
+\begin{chunk}{axiom.bib}
+@article{Safo01,
+ author = "Safouhi, Hassan",
+ title = "Numerical evaluation of threecenter twoelectron Coulomb and
+ hybrid integrals over $B$ functions using the $HD$ and
+ $H\overline{D}$ methods and convergence properties",
+ journal = "J. Math. Chem.",
+ volume = "29",
+ number = "3",
+ pages = "213232",
+ year = "2001",
+ keywords = "axiomref",
+ abstract =
+ "The $B$ function is a product of a spherical $K$ Bessel function and
+ a spherical harmonic. The integrals to be evaluated contain
+ complicated expressions of finite hypergeometric functions and
+ spherical $J$ Bessel functions. Sequence transformation techniques are
+ used for the numerical evaluation of the integrals. Numerical examples
+ illustrate the accuracy and the efficiency of the method."
+}
+
+\end{chunk}
+
\begin{chunk}{axiom.bib}
@misc{SALSA,
title = "Solvers for Algebraic Systems and Applications",
@@ 15558,15 +15957,6 @@ Mathematik und Physik, 75 (suppl. 2):S435S438, 1995 ISSN 00442267
\end{chunk}
\index{Stein, William}
\begin{chunk}{ignore}
\bibitem[Sage 14]{Sage14} Stein, William
 title = "Sage",
 url = "http://www.sagemath.org/doc/reference/interfaces/sage/interfaces/axiom.html",
 keywords = "axiomref",

\end{chunk}

\index{Salvy, Bruno}
\begin{chunk}{ignore}
\bibitem[Salvy 89]{Sal89} Salvy, B.
@@ 15623,7 +16013,7 @@ Kognitive Systeme, Universit\"t Karlsruhe 1992
\end{chunk}
\index{Schwarz, F.}
+\index{Schwarz, Fritz}
\begin{chunk}{ignore}
\bibitem[Schwarz 88]{Sch88} Schwarz, F.
title = "Programming with abstract data types: the symmetry package SPDE in Scratchpad'",
@@ 15633,7 +16023,7 @@ In Jan{\ss}en [Jan88], pp167176, ISBN 3540189289,
\end{chunk}
\index{Schwarz, F.}
+\index{Schwarz, Fritz}
\begin{chunk}{ignore}
\bibitem[Schwarz 89]{Sch89} Schwarz, F.
title = "A factorization algorithm for linear ordinary differential equations",
@@ 15642,7 +16032,40 @@ In ACM [ACM89], pp1725 ISBN 0897913256 LCCN QA76.95.I59 1989
\end{chunk}
\index{Schwarz, F.}
+\index{Schwarz, Fritz}
+\begin{chunk}{axiom.bib}
+@InProceedings{Schw02,
+ author = "Schwarz, Fritz",
+ title = "ALLTYPES: An algebraic language and type system",
+ booktitle = "1st Int. Congress on Mathematical Software",
+ year = "2002",
+ isbn = "9812380485",
+ location = "Beijing China",
+ pages = "486500",
+ keywords = "axiomref",
+ paper = "Schw02.pdf",
+ url =
+"http://www.scai.fraunhofer.de/content/dam/scai/de/documents/MitarbeiterinnenundMitarbeiter/ICMS2002.pdf",
+ abstract =
+ "The software system ALLTYPES provides an environment that is
+ particularly designed for developing software in differential
+ algebra. Its most important features may be described as follows: A
+ set of about thirty parametrized algebraic types is defined. Data
+ objects represented by these types may be manipulated by more than one
+ hundred polymorphic functions. Reusability of code is achieved by
+ genericity and multiple inheritance. The user may extend the system by
+ defining new types and polymorphic functions. A language comprising
+ seven basic language constructs is defined for implementing
+ mathematical algorithms. The easy manipulation of types is
+ particularly supported due to a special portion of the language
+ dedicated to manipulating typed objects, i.e. for performing
+ userdefined or automatic type coercions. Type inquiries are also
+ included in the language."
+}
+
+\end{chunk}
+
+\index{Schwarz, Fritz}
\begin{chunk}{ignore}
\bibitem[Schwarz 91]{Sch91} Schwarz, F.
title = "Monomial orderings and Gr{\"o}bner bases",
@@ 15949,6 +16372,15 @@ Physics, pp337344, Acireale (Italy), 1992 Kluwer, Dordrecht 1993
\end{chunk}
+\index{Stein, William}
+\begin{chunk}{ignore}
+\bibitem[Sage 14]{Sage14} Stein, William
+ title = "Sage",
+ url = "http://www.sagemath.org/doc/reference/interfaces/sage/interfaces/axiom.html",
+ keywords = "axiomref",
+
+\end{chunk}
+
\index{Sutor, Robert S.}
\begin{chunk}{ignore}
\bibitem[Sutor 85]{Sut85} Sutor, R.S.
@@ 16039,10 +16471,17 @@ IBM Manual, March 1988
\index{Thompson, Simon}
\begin{chunk}{ignore}
\bibitem[Thompson 00]{Tho00} Thompson, Simon
+@InProceedings{Thom01,
+ author = "Thompson, Simon",
title = "Logic and dependent types in the Aldor Computer Algebra System",
 paper = "Tho00.pdf",
+ booktitle = "Symbolic computation and automated reasoning",
+ series = "CALCULEMUS 2000",
+ year = "2001",
+ location = "St. Andrews, Scotland",
+ pages = "205233",
keywords = "axiomref",
+ paper = "Thom01.pdf",
+ url = "http://axiomwiki.newsynthesis.org/public/refs/aldorcalc2000.pdf",
abstract = "
We show how the Aldor type system can represent propositions of
firstorder logic, by means of the 'propositions as types'
@@ 16051,6 +16490,7 @@ IBM Manual, March 1988
type system with {\sl type evaluation} reported elsewhere. The logic
is used to provide an axiomatisation of a number of familiar Aldor
categories as well as a type of vectors."
+}
\end{chunk}
@@ 16403,20 +16843,23 @@ IBM T. J. Watson Research Center (2001)
\end{chunk}
\index{Weber, Andreas}
\begin{chunk}{ignore}
\bibitem[Weber 92]{Webe92} Weber, Andreas
+\begin{chunk}{axiom.bib}
+@phdthesis{Webe93b,
+ author = "Weber, Andreas",
title = "Type Systems for Computer Algebra",
 url = "http://cg.cs.unibonn.de/personalpages/weber/publications/pdf/WeberA/Weber92a.pdf",
 paper = "Webe92.pdf",
+ school = "University of Tubingen",
+ year = "1993",
+ paper = "Webe93b.pdf",
keywords = "axiomref",
 abstract = "
 An important feature of modern computer algebra systems is the support
+ abstract =
+ "An important feature of modern computer algebra systems is the support
of a rich type system with the possibility of type inference. Basic
features of such a type system are polymorphism and coercion between
types. Recently the use of ordersorted rewrite systems was proposed
as a general framework. We will give a quite simple example of a
family of types arising in computer algebra whose coercion relations
cannot be captured by a finite set of firstorder rewrite rules."
+}
\end{chunk}
diff git a/changelog b/changelog
index 7fc64d4..34c6aab 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20160626 tpd src/axiomwebsite/patches.html 20160626.10.tpd.patch
+20160626 tpd books/bookvolbib Axiom Citations in the Literature
20160626 tpd src/axiomwebsite/patches.html 20160626.09.tpd.patch
20160626 tpd books/bookvolbib Axiom Citations in the Literature
20160626 tpd src/axiomwebsite/patches.html 20160626.08.tpd.patch
diff git a/patch b/patch
index 194ca90..83a346c 100644
 a/patch
+++ b/patch
@@ 2,115 +2,571 @@ books/bookvolbib Axiom Citations in the Literature
Goal: Axiom Literate Programming
\index{Tournier, Evelyne}
+\index{Prevosto, Virgile}
+\index{Doligez, Damien}
\begin{chunk}{axiom.bib}
@misc{Tour95,
 author = "Tournier, Evelyne",
 title = "Summary of organisation, history and possible future",
 paper = "Tour95.pdf",
 year = "1995",
+@article{Prev02,
+ author = "Prevosto, Virgile and Doligez, Damien",
+ title = "Algorithms and proofs inheritance in the FOC language",
+ journal = "J. Autom. Reasoning",
+ volume = "29",
+ number = "34",
+ pages = "337363",
+ keywords = "axiomref",
+ paper = "Prev02.pdf",
+ abstract =
+ "In this paper, we present the FOC language, dedicated to the
+ development of certified computer algebra libraries (that is sets of
+ programs). These libraries are based on a hierarchy of implementations
+ of mathematical structures. After presenting the core set of features
+ of our language, we describe the static analyses, which reject
+ inconsistent programs. We then show how we translate FOC definitions
+ into OCAML and COQ, our target languages for the computational part
+ and the proof checking, respectively."
+}
+
+\end{chunk}
+
+\index{Schwarz, Fritz}
+\begin{chunk}{axiom.bib}
+@InProceedings{Schw02,
+ author = "Schwarz, Fritz",
+ title = "ALLTYPES: An algebraic language and type system",
+ booktitle = "1st Int. Congress on Mathematical Software",
+ year = "2002",
+ isbn = "9812380485",
+ location = "Beijing China",
+ pages = "486500",
+ keywords = "axiomref",
+ paper = "Schw02.pdf",
url =
 "ftp://ftp.inf.ethz.ch/org/cathode/workshops/jan95/abstracts/tournier.ps",
+"http://www.scai.fraunhofer.de/content/dam/scai/de/documents/MitarbeiterinnenundMitarbeiter/ICMS2002.pdf",
+ abstract =
+ "The software system ALLTYPES provides an environment that is
+ particularly designed for developing software in differential
+ algebra. Its most important features may be described as follows: A
+ set of about thirty parametrized algebraic types is defined. Data
+ objects represented by these types may be manipulated by more than one
+ hundred polymorphic functions. Reusability of code is achieved by
+ genericity and multiple inheritance. The user may extend the system by
+ defining new types and polymorphic functions. A language comprising
+ seven basic language constructs is defined for implementing
+ mathematical algorithms. The easy manipulation of types is
+ particularly supported due to a special portion of the language
+ dedicated to manipulating typed objects, i.e. for performing
+ userdefined or automatic type coercions. Type inquiries are also
+ included in the language."
+}
+
+\end{chunk}
+
+\index{Adams, Andrew A.}
+\index{Dunstan, Martin}
+\index{Gottlieben, Hanne}
+\index{Kelsey, Tom}
+\index{Martin, Ursula}
+\index{Owre, Sam}
+\begin{chunk}{axiom.bib}
+@InProceedings{Adam01,
+ author = "Adams, Andrew A. and Dunstan, Martin and Gottlieben, Hanne and
+ Kelsey, Tom and Martin, Ursula and Owre, Sam",
+ title = "Computer algebra meets automated theorem proving: Integrating
+ Maple and PVS",
+ booktitle = "Theorem proving in higher order logics",
+ series = "TPHOLs 2001",
+ year = "2001",
+ location = "Edinburgh, Scotland",
+ pages = "2742",
+ keywords = "axiomref",
+ paper = "Adam01.pdf",
+ abstract =
+ "We describe an interface between version 6 of the Maple computer
+ algebra system with the PVS automated theorem prover. The interface is
+ designed to allow Maple users access to the robust and checkable proof
+ environment of PVS. We also extend this environment by the provision
+ of a library of proof strategies for use in real analysis. We
+ demonstrate examples using the interface and the real analysis
+ library. These examples provide proofs which are both illustrative and
+ applicable to genuine symbolic computation problems."
+}
+
+\end{chunk}
+
+\index{Antoine, Xavier}
+\begin{chunk}{axiom.bib}
+@article{Anto01,
+ author = "Antoine, Xavier",
+ title = "Microlocal diagonalization of strictly hyperbolic pseudodifferential
+ systems and application to the design of radiation conditions in
+ electromagnetism",
+ journal = "SIAM J. Appl. Math",
+ volume = "61",
+ number = "6",
+ pages = "18771905",
+ year = "2001",
+ keywords = "axiomref",
+ abstract =
+ "In [Commun. Pure Appl. Math. 28, 457478 (1975; Zbl 0332.35058)],
+ M. E. Taylor described a constructive diagonalization method to
+ investigate the reflection of singularities of the solution to
+ firstorder hyperbolic systems. According to further works initiated
+ by Engquist and Majda, this approach proved to be well adapted to the
+ construction of artificial boundary conditions. However, in the case
+ of systems governed by pseudodifferential operators with variable
+ coefficients, Taylor’s method involves very elaborate calculations of
+ the symbols of the operators. Hence, a direct approach may be
+ difficult when dealing with highorder conditions.
+
+ This motivates the first part of this paper, where a recursive
+ explicit formulation of Taylor’s method is stated for microlocally
+ strictly hyperbolic systems. Consequently, it provides an algorithm
+ leading to symbolic calculations which can be handled by a computer
+ algebra system. In the second part, an application of the method is
+ investigated for the construction of local radiation boundary
+ conditions on arbitrarily shaped surfaces for the transverse electric
+ Maxwell system. It is proved that they are of complete order, provided
+ the introduction of a new symbols class well adapted to the Maxwell
+ system. Next, a complete secondorder condition is designed, and when
+ used as an onsurface radiation condition [G. A. Kriegsmann,
+ A. Taflove, and K. R. Umashankar, IEEE Trans. Antennas Propag. 35,
+ 153161 (1987; Zbl 0947.78571)], it can give rise to an ultrafast
+ numerical approximate solution of the scattered field."
+}
+
+\end{chunk}
+
+\index{Delliere, Stephane}
+\begin{chunk}{axiom.bib}
+@article{Dell01,
+ author = "Delliere, Stephane",
+ title = "On the links between triangular sets and dynamic constructable
+ closure",
+ journal = "J. Pure Appl. Algebra",
+ volume = "163",
+ number = "1",
+ pages = "4968",
+ year = "2001",
+ keywords = "axiomref",
+ abstract =
+ "Two kinds of triangular systems are studied: normalized triangular
+ polynomial systems (a weaker form of Lazard’s triangular sets
+ [D. Lazard, Discrete Appl. Math. 33, No. 13, 147160 (1991; Zbl
+ 0753.13013)] and constructible triangular systems (involved in the
+ dynamic constructible closure programs of T. GomezDíaz [Quelques
+ applications de l'evaluation dynamique, Ph.D. Thesis, Universite de
+ Limoges (1994)]. This paper shows that these notions are strongly
+ related. In particular, combining the two points of view
+ (constructible and polynomial) on the subject of squarefree
+ conditions, it allows us to effect dramatic improvements in the
+ dynamic constructible closure programs."
+}
+
+\end{chunk}
+
+\index{Michler, Gerhard O.}
+\begin{chunk}{axiom.bib}
+@article{Mich01,
+ author = "Michler, Gerhard O.",
+ title = "The character values of multiplicityfree irreducible constituents
+ of a transitive permutation representation",
+ journal = "Kyushu J. Math.",
+ volume = "55",
+ number = "1",
+ pages = "75106",
+ year = "2001",
+ keywords = "axiomref",
+ url = "https://www.jstage.jst.go.jp/article/kyushujm/55/1/55\_1\_75/\_pdf",
+ paper = "Mich01.pdf",
+ abstract =
+ "Let $G$ be a finite group and $M$ a subgroup of $G$. Let the
+ permutation character of $G$ on the set of right cosets of $M$ be
+ denoted by $(1_M)^G$. Any ordinary irreducible constituent of
+ $(1_M)^G$ with multiplicity one is called a multiplicityfree
+ constituent of $(1_M)^G$. In the paper under review the author gives
+ an efficient algorithm to compute the values of any multiplicityfree
+ constituent of $(1_M)^G$. The character value is in terms of the
+ double coset decomposition of $M$ and related concepts concerning
+ intersection matrices. The author uses this algorithm to determine the
+ values of the multiplicityfree constituents of $(1_C)^{J_1}$, where
+ $J_1$ is the smallest Janko group of order 175560 and $C$ is the
+ centralizer of an involution in $J_1$. Using these, he then is able to
+ compute the character table of $J_1$ which is already known."
+}
+
+\end{chunk}
+
+\index{Rudnicki, Piotr}
+\index{Schwarzweller, Christoph}
+\index{Trybulec, Andrzej}
+\begin{chunk}{axiom.bib}
+@article{Rudn01,
+ author = "Rudnicki, Piotr and Schwarzweller, Christoph and
+ Trybulec, Andrzej",
+ title = "Commutative algebra in the Mizar system",
+ journal = "J. Symb. Comput.",
+ volume = "32",
+ number = "12",
+ pages = "143169",
+ year = "2001",
+ keywords = "axiomref",
+ url = "https://inf.ug.edu.pl/~schwarzw/papers/jsc01.pdf",
+ paper = "Rudn01.pdf",
+ abstract =
+ "We report on the development of algebra in the Mizar system. This
+ includes the construction of formal multivariate power series and
+ polynomials as well as the definition of ideals up to a proof of the
+ Hilbert basis theorem. We present how the algebraic structures are
+ handled and how we inherited the past developments from the Mizar
+ Mathematical Library (MML). The MML evolves and past contributions are
+ revised and generalized. Our work on formal power series caused a
+ number of such revisions. It seems that revising past developments
+ with an intent to generalize them is a necessity when building a
+ database of formalized mathematics. This poses a question: how much
+ generalization is best?"
+}
+
+\end{chunk}
+
+\index{Safouhi, Hassan}
+\begin{chunk}{axiom.bib}
+@article{Safo01,
+ author = "Safouhi, Hassan",
+ title = "Numerical evaluation of threecenter twoelectron Coulomb and
+ hybrid integrals over $B$ functions using the $HD$ and
+ $H\overline{D}$ methods and convergence properties",
+ journal = "J. Math. Chem.",
+ volume = "29",
+ number = "3",
+ pages = "213232",
+ year = "2001",
+ keywords = "axiomref",
+ abstract =
+ "The $B$ function is a product of a spherical $K$ Bessel function and
+ a spherical harmonic. The integrals to be evaluated contain
+ complicated expressions of finite hypergeometric functions and
+ spherical $J$ Bessel functions. Sequence transformation techniques are
+ used for the numerical evaluation of the integrals. Numerical examples
+ illustrate the accuracy and the efficiency of the method."
+}
+
+\end{chunk}
+
+\index{Thompson, Simon}
+\begin{chunk}{ignore}
+@InProceedings{Thom01,
+ author = "Thompson, Simon",
+ title = "Logic and dependent types in the Aldor Computer Algebra System",
+ booktitle = "Symbolic computation and automated reasoning",
+ series = "CALCULEMUS 2000",
+ year = "2001",
+ location = "St. Andrews, Scotland",
+ pages = "205233",
+ keywords = "axiomref",
+ paper = "Thom01.pdf",
+ url = "http://axiomwiki.newsynthesis.org/public/refs/aldorcalc2000.pdf",
+ abstract = "
+ We show how the Aldor type system can represent propositions of
+ firstorder logic, by means of the 'propositions as types'
+ correspondence. The representation relies on type casts (using
+ pretend) but can be viewed as a prototype implementation of a modified
+ type system with {\sl type evaluation} reported elsewhere. The logic
+ is used to provide an axiomatisation of a number of familiar Aldor
+ categories as well as a type of vectors."
+}
+
+\end{chunk}
+
+\index{Poll, Erik}
+\begin{chunk}{axiom.bib}
+@misc{Poll99,
+ author = "Poll, Erik",
+ title = "The Type System of Axiom",
+ year = "1999",
+ url = "http://www.cs.ru.nl/E.Poll/talks/axiom.pdf",
+ paper = "Poll99.pdf",
+ keywords = "axiomref",
+ abstract =
+ "This is a slide deck from a talk on the correspondence between
+ Axiom/Aldor types and Logic."
+}
+
+\end{chunk}
+
+\index{Poll, Erik}
+\index{Thompson, Simon}
+\begin{chunk}{axiom.bib}
+@misc{Pollxx,
+ author = "Poll, Erik and Thompson, Simon",
+ title = "Adding the axioms to Axiom. Toward a system of automated
+ reasoning in Aldor",
+ url =
+"http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.1457&rep=rep1&type=ps",
+ paper = "Pollxx.pdf",
+ keywords = "axiomref",
+ abstract = "
+ This paper examines the proposal of using the type system of Axiom to
+ represent a logic, and thus to use the constructions of Axiom to
+ handle the logic and represent proofs and propositions, in the same
+ way as is done in theorem provers based on type theory such as Nuprl
+ or Coq.
+
+ The paper shows an interesting way to decorate Axiom with pre and
+ postconditions.
+
+ The CurryHoward correspondence used is
+ \begin{verbatim}
+ PROGRAMMING LOGIC
+ Type Formula
+ Program Proof
+ Product/record type (...,...) Conjunction
+ Sum/union type \/ Disjunction
+ Function type > Implication
+ Dependent function type (x:A) > B(x) Universal quantifier
+ Dependent product type (x:A,B(x)) Existential quantifier
+ Empty type Exit Contradictory proposition
+ One element type Triv True proposition
+ \end{verbatim}"
+}
+
+\end{chunk}
+
+\index{Poll, Erik}
+\index{Thompson, Simon}
+\begin{chunk}{axiom.bib}
+@misc{Poll00,
+ author = "Poll, Erik and Thompson, Simon",
+ title = "Integrating Computer Algebra and Reasoning through the Type
+ System of Aldor",
+ paper = "P0ll00.pdf",
+ keywords = "axiomref",
+ year = "2000",
+ abstract =
+ "A number of combinations of reasoning and computer algebra systems
+ have been proposed; in this paper we describe another, namely a way to
+ incorporate a logic in the computer algebra system Axiom. We examine
+ the type system of Aldor  the Axiom Library Compiler  and show
+ that with some modifications we can use the dependent types of the
+ system to model a logic, under the CurryHoward isomorphism. We give
+ a number of example applications of the logic we construct and explain
+ a prototype implementation of a modified typechecking system written
+ in Haskell."
+}
+
+\end{chunk}
+
+\index{Page, Bill}
+\begin{chunk}{axiom.bib}
+@misc{Page08,
+ author = "Page, Bill",
+ title = "Algebraist Network",
+ url = "http://lambdatheultimate.org/node/2737",
+ year = "2008",
keywords = "axiomref"
}
\end{chunk}
\index{Watt, Stephen M.}
+\index{Poll, Erik}
+\index{Thompson, Simon}
\begin{chunk}{axiom.bib}
@misc{Watt95a,
 author = "Watt, Stephen M.",
 title = "The A\# Programming Language and Compiler",
 paper = "Watt95a.pdf",
 year = "1995",
 url = "ftp://ftp.inf.ethz.ch/org/cathode/workshops/march93/Watt.tex",
+@InProceedings{Poll00a,
+ author = "Poll, Erik and Thompson, Simon",
+ title = "Integrating Computer Algebra and Reasoning through the Type
+ System of Aldor",
+ booktitle = "Frontiers of Combining Systems",
+ series = "Lecture Notes in Artificial Intelligence",
+ year = "2000",
+ isbn = "3540672818",
+ location = "Nancy, France",
+ pages = "136150",
keywords = "axiomref"
}
\end{chunk}
\index{Lecerf, Gr{\'e}goire}
+\index{Davenport, James H.}
\begin{chunk}{axiom.bib}
@article{Lece02,
 author = "Lecerf, Gregoire",
 title = "Quadratic Newton iteration for systems with multiplicity",
 journal = "Found. Comput. Math.",
 volume = "2",
 number = "3",
 pages = "247293",
 year = "2002",
+@InProceedings{Dave00,
+ author = "Davenport, James H.",
+ title = "Abstract data types in computer algebra",
+ booktitle = "Mathematical foundations of computer science",
+ series = "MFCS 2000",
+ year = "2000",
+ location = "Bratislava, Slovakia",
+ pages = "2135",
keywords = "axiomref",
 paper = "Lece02.pdf",
abstract =
 "The author proposes an efficient iterator with quadratic convergence
 that generalizes Newton iterator for multiple roots. It is based on an
 $m$adic topology where the ideal $m$ can be chosen generic
 enough. Compared to the Newton iterator the proposed iterator
 introduces a small overhead that grows with the square of the
 multiplicity of the root."
+ "The theory of abstract data types was developed in the late 1970s and
+ the 1980s by several people, including the ``ADJ'' group, whose work
+ influenced the design of Axiom. One practical manifestation of this
+ theory was the OBJ3 system. An area of computing that cries out for
+ this approach is computer algebra, where the objects of discourse are
+ mathematical, generally satisfying various algebraic rules. There have
+ been various theoretical studies of this in the literature. The aim of
+ this paper is to report on the practical applications of this theory
+ within computer algebra, and also to outline some of the theoretical
+ issues raised by this practical application. We also give a
+ substantial bibliography."
}
\end{chunk}
\index{Lecerf, Gr{\'e}goire}
+\index{Weber, Andreas}
\begin{chunk}{axiom.bib}
@article{Lece96,
 author = "Lecerf, Gregoire",
 title = "Dynamic Evaluation and Real Closure Implementation in Axiom",
 year = "1996",
 url = "http://lecerf.perso.math.cnrs.fr/software/drc/drc.ps",
 paper = "Lece96.pdf",
 keywords = "axiomref"
+@phdthesis{Webe93b,
+ author = "Weber, Andreas",
+ title = "Type Systems for Computer Algebra",
+ school = "University of Tubingen",
+ year = "1993",
+ paper = "Webe93b.pdf",
+ keywords = "axiomref",
+ abstract =
+ "An important feature of modern computer algebra systems is the support
+ of a rich type system with the possibility of type inference. Basic
+ features of such a type system are polymorphism and coercion between
+ types. Recently the use of ordersorted rewrite systems was proposed
+ as a general framework. We will give a quite simple example of a
+ family of types arising in computer algebra whose coercion relations
+ cannot be captured by a finite set of firstorder rewrite rules."
}
\end{chunk}
\index{Lomonaco, Samual J.}
\index{Kauffman, Louis H.}
+\index{Fateman, Richard J.}
\begin{chunk}{axiom.bib}
@InProceedings{Lomo02,
 author = "Lomonaco, Samual J. and Kauffman, Louis H.",
 title = "Quantum hidden subgroup algorithms: a mathematical perspective",
 booktitle = "Quantum computation and information",
 series = "AMS special session",
 year = "2002",
 isbn = "0821821407",
 location = "Washington",
 pages = "139202",
+@InProceedings{Fate00,
+ author = "Fateman, Richard J.",
+ title = "Problem solving environments and symbolic computing",
+ booktitle = "Enabling technologies for computational science",
+ publisher = "Kluwer Academic Publishers",
+ year = "2000",
+ pages = "91102",
+ keywords = "axiomref",
+ paper = "Fate00.pdf",
+ url = "http://people.eecs.berkeley.edu/~fateman/papers/psekluwer.pdf",
+ abstract =
+ "What role should be played by symbolic mathematical computation
+ facilities in scientific and engineering ``problem solving
+ environments''? Drawing upon standard facilities such as numerical and
+ graphical libraries, symbolic computation should be useful for: The
+ creation and manipulation of mathematical models; The production of
+ custom optimized numerical software; The solution of delicate classes
+ of mathematical problems that require handling beyond that available
+ in traditional machinesupported floatingpoint computation. Symbolic
+ representation and manipulation can potentially play a central
+ organizing role in PSEs since their more general object representation
+ allows a program to deal with a wider range of computational
+ issues. In particular numerical, graphical, and other processing can
+ be viewed as special cases of symbolic manipulation with interactive
+ symbolic computing providing both an organizing backbone and the
+ communication ``glue'' among otherwise dissimilar components"
+}
+
+\end{chunk}
+
+\index{Hoang, Ngoc Minh}
+\index{Petitot, Michel}
+\index{Van er Hoeven, Joris}
+\begin{chunk}{axiom.bib}
+@article{Hoan00,
+ author = "Hoang, Ngoc Minh and Petitot, Michel and Van er Hoeven, Joris",
+ title = "Shuffle algebra and polylogarithms",
+ journal = "Discrete Math.",
+ volume = "225",
+ number = "13",
+ pages = "217230",
+ year = "2000",
+ keywords = "axiomref",
+ paper = "Hoan00.pdf",
+ abstract =
+ "Generalized polylogarithms are defined as iterated integrals with
+ respect to the two differential forms $\omega_0=\frac{dz}{z}$ and
+ $\omega_1=\frac{dz}{(1z)}$. We give an algorithm which computes the
+ monodromy of these special functions. This algorithm, implemented in
+ AXIOM, is based on the computation of the associator $\Phi_{KZ}$ of
+ Drinfel’d, in factorized form. The monodromy formulae involve special
+ constants, called multiple zeta values. We prove that the algebra of
+ polylogarithms is isomorphic to a shuffle algebra."
+}
+
+\end{chunk}
+
+\index{Raab, C.G.}
+\begin{chunk}{axiom.bib}
+@article{Raab13,
+ author = "Raab, C.G.",
+ title = "Generalization of Risch's Algorithm to Special Functions",
+ journal = "CoRR",
+ volume = "abs/1305.1481",
+ year = "2013",
+ url = "http://arxiv.org/pdf/1305.1481v1.pdf",
+ paper = "Raab13.pdf",
+ abstract =
+ "Symbolic integration deals with the evaluation of integrals in closed
+ form. We present an overview of Risch's algorithm including recent
+ developments. The algorithms discussed are suited for both indefinite
+ and definite integration. They can also be used to compute linear
+ relations among integrals and to find identities for special functions
+ given by parameter integrals. The aim of this presentation is twofold:
+ to introduce the reader to some basic ideas of differential algebra in
+ the context of integration and to raise awareness in the physics
+ community of computer algebra algorithms for indefinite and definite
+ integration. "
+}
+
+\end{chunk}
+
+\index{Houstis, Elias N.}
+\index{Rice, John R.}
+\begin{chunk}{axiom.bib}
+@article{Hous00,
+ author = "Houstis, Elias N. and Rice, John R.",
+ title = "Future problem solving environments for computational science",
+ journal = "Math. Comput. Simul.",
+ volume = "54",
+ number = "45",
+ pages = "243257",
+ year = "2000",
+ keywords = "axiomref",
+ abstract =
+ "We review the current state of the Problem Solving Environment (PSE)
+ field and make projections for the future. First, we describe the
+ computing context, the definition of a PSE and the goals of a PSE. The
+ stateoftheart is summarized along with the principal components and
+ paradigms for building PSEs. The discussion of the future is given in
+ three parts: future trends, scenarios for 2010/2025, and research
+ issues to be addressed."
+}
+
+\end{chunk}
+
+\index{Gallopoulos, Stratis}
+\index{Houstis, Elias}
+\index{Rice, John}
+\begin{chunk}{axiom.bib}
+@techreport{Gall92,
+ author = "Gallopoulos, Stratis and Houstis, Elias and Rice, John",
+ title = "Future Research Directions in Problem Solving Environments for
+ Computational Science",
+ institution = "Purdue University",
+ year = "1992",
+ type = "technical report",
+ number = "CSDTR92032",
+ paper = "Gall92.pdf",
+ url =
+"http://docs.lib.purdue.edu/cgi/viewcontent.cgi?article=1953\&context=cstech",
keywords = "axiomref",
 paper = "Lomo02.pdf",
 url = "https://arxiv.org/pdf/quantph/0201095v3.pdf",
abstract =
 "The ultimate objective of this paper is to create a stepping stone to
 the development of new quantum algorithms. The strategy chosen is to
 begin by focusing on the class of abelian quantum hidden subgroup
 algorithms, i.e., the class of abelian algorithms of the Shor/Simon
 genre. Our strategy is to make this class of algorithms as
 mathematically transparent as possible. By the phrase ``mathematically
 transparent'' we mean to expose, to bring to the surface, and to make
 explicit the concealed mathematical structures that are inherently and
 fundamentally a part of such algorithms. In so doing, we create
 symbolic abelian quantum hidden subgroup algorithms that are analogous
 to the those symbolic algorithms found within such software packages
 as Axiom, Cayley, Maple, Mathematica, and Magma.

 As a spinoff of this effort, we create three different
 generalizations of Shor’s quantum factoring algorithm to free abelian
 groups of finite rank. We refer to these algorithms as wandering (or
 vintage $\mathbb{Z}_Q$) Shor algorithms. They are essentially quantum
 algorithms on free abelian groups of finite rank $n$ which, with each
 iteration, first select a random cyclic direct summand $\mathbb{Z}$ of
 the group and then apply one iteration of the standard Shor algorithm
 to produce a random character of the “approximating” finite group
 $\widetilde{A} = \mathbb{Z}_Q$, called the group probe. These
 characters are then in turn used to find either the order $P$ of a
 maximal cyclic subgroup $\mathbb{Z}_P$ of the hidden quotient group
 $H_{\varphi}$, or the entire hidden quotient group $H_{\varphi}$. An
 integral part of these wandering quantum algorithms is the selection
 of a very special random transversal $t_{\mu}:\widetilde{A}\rightarrow A$,
 which we refer to as a Shor transversal. The algorithmic time
 complexity of the first of these wandering Shor algorithms is found to
 be $O(n^2({rm lg\ } Q)^3 ({\rm lg\ }{\rm lg\ } Q)^{n+1})$."
+ "During the early 19605 some were visualizing that computers could
+ provide a powerful problem solving environment (PSE) which would
+ interact with scientists on their own terms. By the mid 1960s there
+ were many attempts underway to create these PSEs, but the early
+ 1970s almost all of these attempts had been abandoned, because the
+ technological infrastructure could not yet support PSEs in
+ computational science. The dream of the 1960s can be the reality of
+ the 1990s; high performance computers combined with better
+ understanding of computing and computational science have put PSEs
+ well within our reach."
}
\end{chunk}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index af9c646..a922046 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5410,6 +5410,8 @@ books/bookvolbib Axiom Citations in the Literature
books/bookvol* add Mulders to ORE and LODO refs
20160626.09.tpd.patch
books/bookvolbib Axiom Citations in the Literature
+20160626.10.tpd.patch
+books/bookvolbib Axiom Citations in the Literature

1.7.5.4