From 4e6306df4b964f2c48b8b9016eaca709511a34b7 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Thu, 9 Nov 2017 17:09:24 0500
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{Mesh05,
author = "Meshveliani, Sergei D.",
title = {{Term rewriting, Equationional Reasoning, Automatic proofs}},
link = "\url{ftp://ftp.botik.ru/pub/local/Mechveliani/dumatel/1.02/}",
year = "2005",
paper = "Mesh05.pdf"
}
\end{chunk}
\index{Davenport, James H.}
\begin{chunk}{axiom.bib}
@misc{Dave98,
author = "Davenport, James H.",
title = {{Is Computer Algebra the same as Computer Mathematics?}},
year = "1998",
comment = "Talk for British Colloquium for Theoretical Computer Science"
}
\end{chunk}
\index{Th\'ery, Laurent}
\begin{chunk}{axiom.bib}
@article{Ther98,
author = "Thery, Laurent",
title = {{A Certified Version of Buchberger's Algorithm}},
journal = "LNCS",
volume = "1421",
pages = "349364",
year = "1998",
abstract =
"We present a proof of Buchberger's algorithm that has been developed
in the Coq proof assistant. The formulation of the algorithm in Coq
can be efficiently compiled and used to do computation",
paper = "Ther98.pdf"
}
\end{chunk}
\index{Cooley, James W.}
\index{Tukey, John W.}
\begin{chunk}{axiom.bib}
@article{Cool65,
author = "Cooley, James W. and Tukey, John W.",
title = {{An Algorithm for the Machine Calculation of Complex Fourier
Series}},
journal = "Mathematics of Computation",
volume = "19",
number = "04",
year = "1965"
}
\end{chunk}
\index{Rump, Siegfried M.}
\begin{chunk}{axiom.bib}
@article{Rump88,
author = "Rump, Siegfried M.",
title = {{Algebraic Computation, Numerical Computation and Verified
Inclusions}},
journal = "LNCS",
volume = "296",
pages = "177197",
year = "1988",
abstract =
"The three different types of computation  the algebraic
manipulation, the numerical computation and the computation of
verified results  are aiming on different problems and deliver
qualitatively different results, each method having its specific
advantages for specific classes of problems. The following remarks
give some thoughts on possible combinations of all three methods to
obtain algorithms benefitting from the specific strength of either
method.",
paper = "Rump88.pdf"
}
\end{chunk}
\index{Engelman, C.}
\begin{chunk}{axiom.bib}
@inproceedings{Enge65,
author = "Engelman, C.",
title = {{A Program for OnLine Assistance in Symbolic Computation}},
booktitle = "Proc. Fall Joint Comput. Conf. 2",
year = "1965",
publisher = "Spartan Books"
}
\end{chunk}
\index{Church, Alonzo}
\begin{chunk}{axiom.bib}
@article{Chur40,
author = "Church, Alonzo",
title = {{A Formulation of the Simple Theory of Types}},
journal = "J. of Symbolic Logic",
volume = "5",
number = "2",
year = "1940",
pages = "5668",
abstract =
"The purpose of the present paper is to give a formulation of the
simple theory of types which incorporates certain features of the
calculus of $\lambda$conversion. A complete incorporation of the
calculus of $\lambda$conversion into the theory of types is
impossible if we require that $\lambda x$ and juxtaposition shall
retain their respective meanings as an abstraction operator and as
denoting the application of function to argument. But the present
partial incorporation has certain advantages from the point of view of
type theory and is offered as being of interest on this basis
(whatever may be thought of the finally satisfactory character of the
theory of types as a foundation for logic and mathematics).",
paper = "Chur40.pdf"
}
\end{chunk}
\index{Redfern, D.}
\begin{chunk}{axiom.bib}
@book{Redf98,
author = "Redfern, D.",
title = {{The Maple Handbook: Maple V Release 5}},
publisher = "Springer",
year = "1998"
}
\end{chunk}
\index{Sorge, Volker}
\begin{chunk}{axiom.bib}
@misc{Sorg96,
author = "Sorge, Volker",
title = {{Integration eines Computeralgebrasystems in eine logische
Beweisumgebung }},
school = "Univ. des Saarlandes",
year = "1996",
comment = "Master's thesis"
}
\end{chunk}
\index{Farmer, William M.}
\index{Guttman, Joshua D.}
\index{Thayer, Javier}
\begin{chunk}{axiom.bib}
@article{Farm93a,
author = "Farmer, William M. and Guttman, Joshua D. and Thayer, Javier",
title = {{IMPS: An Interactive Mathematical Proof Systems}},
journal = "J. of Automated Reasoning",
volume = "11",
pages = "213248",
year = "1993",
abstract =
"IMPS is an interactive mathematical proof system intended as a
generalpurpose too! formulating and applying mathematics in a
familiar fashion. The logic of IMPS is based on a version of simple
type theory with partial functions and subtypes. Mathematical
specification and inference are performed relative to axiomatic
theories, which can be related to one another via inclusion and theory
interpretation. IMPS provides relatively large primitive inference
steps to facilitate human control of the deductive process and human
comprehension of the resulting proofs. An initial theory library con
taining over a thousand repeatable proofs covers significant portions
of logic, algebra, and analysis and provides some support for modeling
applications in computer science.",
paper = "Farm93a.pdf"
}
\end{chunk}
\index{Bundy, Alan}
\index{Wallen, Lincoln}
\begin{chunk}{axiom.bib}
@inproceedings{Bund75,
author = "Bundy, Alan and Wallen, Lincoln",
title = {{The UT Theorem Prover}},
booktitle = "Catalogue of Artificial Intelligence Tools",
pages = "132133",
year = "1975",
abstract =
"The UT theorem prover is probably the best known natural deduction
<153> theorem prover. It was written in LISP <34> by woody Bledsoe and
his coworkers at the University of Texas, and is best described in
(Bledsoe and Tyson 75]. The theorem prover embodies a Gentzenlike
deduction system for firstorder predicate calculus, and many special
purpose techniques, including: subgoaling, rewrite rules, controlled
lorward chaining, controlled definition instantiation, conditional
procedures, and induction. The prover, though powerful in its own
right, is essentially interactive and thus allows the user of the
prover to control the search for the proof in radical ways. The user
can for example : add hypotheses, instruct the prover to instantiate
certain variables with values, or instruct the prover as to which
deduction rule to use next."
}
\end{chunk}
\index{Bledsoe, W.W.}
\begin{chunk}{axiom.bib}
@techreport{Bled83,
author = "Bledsoe, W.W.",
title = {{The UT Natural Deduction Prover}},
type = "technical report",
institution = "Univ. of Texas at Austin",
year = "1983",
number = "ATP17B"
}
\end{chunk}
\index{Bledsoe, W.W.}
\begin{chunk}{axiom.bib}
@inproceedings{Bled84,
author = "Bledsoe, W.W.",
title = {{Some Automatic Proofs in Analysis}},
booktitle = "Automated Theorem Proving: After 25 Years",
publisher = "American Mathematical Society",
year = "1984"
}
\end{chunk}
\index{Bledsoe, W.W.}
\index{Bruell, P.}
\index{Shostak, R.}
\begin{chunk}{axiom.bib}
@techreport{Bled79,
author = "Bledsoe, W.W. and Bruell, P. and Shostak, R.",
title = {{A Prover for General Inequalities}},
type = "technical report",
institution = "Univ. of Texas at Austin",
year = "1979",
number = "ATP40A"
}
\end{chunk}
\index{Fitting, M.}
\begin{chunk}{axiom.bib}
@book{Fitt90,
author = "Fitting, M.",
title = {{Firstorder Logic and Automated Theorem Proving}},
publisher = "SpringerVerlag",
year = "1990",
isbn = "9781461275152"
}
\end{chunk}
\index{Gallier, Jean H.}
\begin{chunk}{axiom.bib}
@book{Gall86,
author = "Gallier, Jean H.",
title = {{Logic for Computer Science: Foundations of Automatic
Theorem Proving}},
publisher = "Harper and Row",
year = "1986",
isbn = "9780486780825"
}
\end{chunk}
\index{Guessarian, Irene}
\index{Meseguer, Jose}
\begin{chunk}{axiom.bib}
@article{Gues87,
author = "Guessarian, Irene and Meseguer, Jose",
title = {{On the Axiomatization of ``IFTHENELSE''}},
journal = "SIAM J. Comput.",
volume = "16",
numbrrer = "2",
year = "1987",
pages = "332357",
abstract =
"The equationally complete proof system for ``ifthenelse'' of Bloom
and Tindell is extended to a complete proof system for manyosrted
algebras with extra operations, predicates and equations among
those. We give similar completeness results for continuous algebras
and program schemes (infinite trees) by the methods of algebraic
semantics. These extensions provide a purely equational proof system
to prove properties of functional programs over userdefinable data
types.",
paper = "Gues87.pdf"
}
\end{chunk}
\index{Cunningham, R.J.}
\index{Dick, A.J.J}
\begin{chunk}{axiom.bib}
@article{Cunn85,
author = "Cunningham, R.J. and Dick, A.J.J",
title = {{Rewrite Systems on a Lattice of Types}},
journal = "Acta Informatica",
volume = "22",
pages = "149169",
year = "1985",
abstract =
"Rewriting systems for partial algebras are developed by modifying
the KnuthBendix completion algorithm to permit the use of
latticestructured domains. Some problems with the original algorithm,
such as the treatment of division rings, are overcome conveniently by
this means. The use of a type lattice also gives a natural framework
for specifying data types in Computer Science without overspecifying
error situations. The soundness and meaning of the major concepts
involed in rewriting systems are reviewed when applied to such
structures.",
paper = "Cunn85.pdf"
}
\end{chunk}
\index{Paulson, Lawrence C.}
\begin{chunk}{axiom.bib}
@article{Paul90,
author = "Paulson, Lawrence C.",
title = {{A Formulation of the Simple Theory of Types (for
Isabelle}}},
journal = "LNCS",
volume = "417",
pages = "246274",
year = "1990",
abstract =
"Simple type theory is formulated for use with the generic theorem
prover Isabelle. This requires explicit type inference rules. There
are function, product, and subset types, which may be
empty. Descriptions (the etaoperator) introduce the Axiom of
Choice. Higherorder logic is obtained through reflection between
formulae and terms of type bool. Recursive types and functions can be
formally constructed. Isabelle proof procedures are described. The
logic appears suitable for general mathematics as well as
computational problems.",
paper = "Paul90.pdf"
}
\end{chunk}
\index{Kelsey, Tom}
\begin{chunk}{axiom.bib}
@phdthesis{Kels99,
author = "Kelsey, Tom",
title = {{Formal Methods and Computer Algebra: A Larch Specification of
AXIOM Categories and Functors}},
school = "University of St Andrews",
year = "1999",
keywords = "axiomref"
}
\end{chunk}
\index{Lee, Wonyeol}
\index{Sharma, Rahul}
\index{Aiken, Alex}
\begin{chunk}{axiom.bib}
@article{Wony18,
author = "Lee, Wonyeol and Sharma, Rahul and Aiken, Alex",
title = {{On Automatically Proving the Correctness of math.h
Implementation}},
journal = "Proc. ACM Programming Languages",
volume = "2",
number = "42",
year = "2018",
pages = "132",
abstract =
"Industry standard implementations of math.h claim (often without
formal proof) tight bounds on floating point errors. We demonstrate a
novel static analysis that proves these bounds and verifies the
correctness of these implementations. Our key insight is a reduction
of this verification task to a set of mathematical optimization
problems that can be solved by offtheshelf computer algebra
systems. We use this analysis to prove the correctness of
implementations in Intel’s math library automatically. Prior to this
work, these implementations could only be verified with significant
manual effort.",
paper = "Wony18.pdf"
}
\end{chunk}
\index{Daly, Timothy}
\begin{chunk}{axiom.bib}
@misc{Daly10,
author = "Daly, Timothy",
title = {{Intel Instruction Semantics Generator}},
link = "\url{http://daly.axiomdeveloper.org/TimothyDaly_files/publications/sei/intel/intel.pdf}",
abstract =
"Given an Intel x86 binary, extract the semantics of the instruction
stream as Conditional Concurrent Assignments (CCAs). These CCAs
represent the semantics of each individual instruction. They can be
composed to represent higher level semantics.",
paper = "Daly10.pdf"
}
\end{chunk}
\index{Naylor, William A.}
\begin{chunk}{axiom.bib}
@phdthesis{Nayl00,
author = "Naylor, Bill",
title = {{Polynomial GCD Using Straight Line Program Representation}},
school = "University of Bath",
year = "2000",
link = "\url{http://www.sci.csd.uwo.ca/~bill/thesis.ps}",
abstract = "
This thesis is concerned with calculating polynomial greatest common
divisors using straight line program representation.
In the Introduction chapter, we introduce the problem and describe
some of the traditional representations for polynomials, we then talk
about some of the general subjects central to the thesis, terminating
with a synopsis of the category theory which is central to the Axiom
computer algebra system used during this research.
The second chapter is devoted to describing category theory. We follow
with a chapter detailing the important sections of computer code
written in order to investigate the straight line program subject.
The following chapter on evalution strategies and algorithms which are
dependant on these follows, the major algorith which is dependant on
evaluation and which is central to our theis being that of equality
checking. This is indeed central to many mathematical problems.
Interpolation, that is the determination of coefficients of a
polynomial is the subject of the next chapter. This is very important
for many straight line program algorithms, as their noncanonical
structure implies that it is relatively difficult to determine
coefficients, these being the basic objects that many algorithms work
on. We talk about three separate interpolation techniques and compare
their advantages and disadvantages. The final two chapters describe
some of the results we have obtained from this research and finally
conclusions we have drawn as to the viability of the straight line
program approach and possible extensions.
Finally we terminate with a number of appendices discussing side
subjects encountered during the thesis.",
paper = "Nayl00.pdf"
}
\end{chunk}
\index{Shoup, Victor}
\begin{chunk}{axiom.bib}
@inproceedings{Shou93,
author = "Shoup, Victor",
title = {{Factoring Polynomials over Finite Fields:
Asymptotic Complexity vs Reality*}},
booktitle = "Proc. IMACS Symposium, Lille, France",
year = "1993",
link = "\url{http://www.shoup.net/papers/lille.pdf}",
abstract =
"This paper compares the algorithms by Berlekamp, Cantor and
Zassenhaus, and Gathen and Shoup to conclude that (a) if large
polynomials are factored the FFT should be used for polynomial
multiplication and division, (b) Gathen and Shoup should be used if
the number of irreducible factors of $f$ is small. (c) if nothing is
know about the degrees of the factors then Berlekamp's algorithm
should be used.",
paper = "Shou93.pdf"
}
\end{chunk}
\index{Wang, Paul S.}
\begin{chunk}{axiom.bib}
@article{Wang78,
author = "Wang, Paul S.",
title = {{An Improved Multivariate Polynomial Factoring Algorithm}},
journal = "Mathematics of Computation",
volume = "32",
number = "144",
year = "1978",
pages = "12151231",
link = "\url{http://www.ams.org/journals/mcom/197832144/S00255718197805682843/S00255718197805682843.pdf}",
abstract = "
A new algorithm for factoring multivariate polynomials over the
integers based on an algorithm by Wang and Rothschild is described.
The new algorithm has improved strategies for dealing with the known
problems of the original algorithm, namely, the leading coefficient
problem, the badzero problem and the occurence of extraneous factors.
It has an algorithm for correctly predetermining leading coefficients
of the factors. A new and efficient padic algorith named EEZ is
described. Basically it is a linearly convergent variablebyvariable
parallel construction. The improved algorithm is generally faster and
requires less store than the original algorithm. Machine examples with
comparative timing are included.",
paper = "Wang78.pdf"
}
\end{chunk}
\index{Baez, John C.}
\index{Stay, Mike}
\begin{chunk}{axiom.bib}
@misc{Baez09,
author = "Baez, John C.; Stay, Mike",
title = {{Physics, Topology, Logic and Computation: A Rosetta Stone}},
link = "\url{http://arxiv.org/pdf/0903.0340v3.pdf}",
abstract = "
In physics, Feynman diagrams are used to reason about quantum
processes. In the 1980s, it became clear that underlying these
diagrams is a powerful analogy between quantum physics and
topology. Namely, a linear operator behaves very much like a
``cobordism'': a manifold representing spacetime, going between two
manifolds representing space. But this was just the beginning: simiar
diagrams can be used to reason about logic, where they represent
proofs, and computation, where they represent programs. With the rise
of interest in quantum cryptography and quantum computation, it became
clear that there is an extensive network of analogies between physics,
topology, logic and computation. In this expository paper, we make
some of these analogies precise using the concept of ``closed
symmetric monodial category''. We assume no prior knowledge of
category theory, proof theory or computer science.",
paper = "Baez09.pdf"
}
\end{chunk}
\index{Dunstan, Martin}
\begin{chunk}{axiom.bib}
@misc{Duns00,
author = "Dunstan, Martin N.",
title = {{Adding Larch/Aldor Specifications to Aldor}},
abstract =
"We describe a proposal to add Larchstyle annotations to the Aldor
programming language, based on our PhD research. The annotations
are intended to be machinecheckable and may be used for a variety
of purposes ranging from compiler optimizations to verification
condition (VC) generation. In this report we highlight the options
available and describe the changes which would need to be made to
the compiler to make use of this technology.",
paper = "Duns00.pdf",
keywords = "axiomref"
}
\end{chunk}
\index{Thompson, Simon}
\begin{chunk}{axiom.bib}
@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",
link =
"\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.",
paper = "Thom01.pdf",
keywords = "axiomref"
}
\end{chunk}
\index{Newcombe, Chris}
\index{Rath, Tim}
\index{Zhang, Fan}
\index{Munteanu, Bogdan}
\index{Brooker, Marc}
\index{Deardeuff, Michael}
\begin{chunk}{axiom.bib}
@misc{Newc13,
author = "Newcombe, Chris and Rath, Tim and Zhang, Fan and
Munteanu, Bogdan and Brooker, Marc and Deardeuff, Michael",
title = {{Use of Formal Methods at Amazon Web Services}},
link = "\url{http://research.microsoft.com/enus/um/people/lamport/tla/formalmethodsamazon.pdf}",
abstract =
"In order to find subtle bugs in a system design, it is necessary to
have a precise description of that design. There are at least two
major benefits to writing a precise design; the author is forced to
think more clearly, which helps eliminate ``plausible handwaving'',
and tools can be applied to check for errors in the design, even while
it is being written. In contrast, conventional design documents
consist of prose, static diagrams, and perhaps pseudocode in an ad
hoc untestable language. Such descriptions are far from precise; they
are often ambiguous, or omit critical aspects such as partial failure
or the granularity of concurrency (i.e. which constructs are assumed
to be atomic). At the other end of the spectrum, the final executable
code is unambiguous, but contains an overwhelming amount of detail. We
needed to be able to capture the essence of a design in a few hundred
lines of precise description. As our designs are unavoidably complex,
we need a highlyexpressive language, far above the level of code, but
with precise semantics. That expressivity must cover realworld
concurrency and faulttolerance. And, as we wish to build services
quickly, we wanted a language that is simple to learn and apply,
avoiding esoteric concepts. We also very much wanted an existing
ecosystem of tools. We found what we were looking for in TLA+, a
formal specification language."
}
\end{chunk}
\index{O'Connor, Liam}
\begin{chunk}{axiom.bib}
@misc{OCon15,
author = {O'Connor, Liam},
title = {{Write Your Compiler by Proving It Correct}},
year = "2015",
link = "\url{http://liamoc.net/posts/20150823verifiedcompiler.html}",
abstract =
"Recently my research has been centered around the development of a
selfcertifying compiler for a functional language with linear types
called Cogent (see O'Connor et al. [2016]). The compiler works by
emitting, along with generated lowlevel code, a proof in Isabelle/HOL
(see Nipkow et al. [2002]) that the generated code is a refinement of
the original program, expressed via a simple functional semantics in HOL.
As dependent types unify for us the language of code and proof, my
current endeavour has been to explore how such a compiler would look
if it were implemented and verified in a dependently typed programming
language instead. In this post, I implement and verify a toy compiler
for a language of arithmetic expressions and variables to an idealised
assembly language for a virtual stack machine, and explain some of the
useful features that dependent types give us for writing verified
compilers."
}
\end{chunk}
\index{Briggs, Keith}
\begin{chunk}{axiom.bib}
@misc{Brig04,
author = "Briggs, Keith",
title = {{Exact real arithmetic}},
link = "\url{http://keithbriggs.info/documents/xrkenttalkpp.pdf}",
year = "2004",
paper = "Bri04.pdf"
}
\end{chunk}
\index{Fateman, Richard J.}
\index{Yan, Tak W.}
\begin{chunk}{axiom.bib}
@misc{Fate94a,
author = "Fateman, Richard J.; Yan, Tak W.",
title ={{Computation with the Extended Rational Numbers and an
Application to Interval Arithmetic}},
link = "\url{http://www.cs.berkeley.edu/~fateman/papers/extrat.pdf}",
abstract = "
Programming languages such as Common Lisp, and virtually every
computer algebra system (CAS), support exact arbitraryprecision
integer arithmetic as well as exect rational number computation.
Several CAS include interval arithmetic directly, but not in the
extended form indicated here. We explain why changes to the usual
rational number system to include infinity and ``notanumber'' may be
useful, especially to support robust interval computation. We describe
techniques for implementing these changes.",
paper = "Fate94a.pdf"
}
\end{chunk}
\index{Atkinson, Kendall}
\index{Han, Welmin}
\index{Stewear, David}
\begin{chunk}{axiom.bib}
@misc{Atki09,
author = "Atkinson, Kendall and Han, Welmin and Stewear, David",
title = {{Numerical Solution of Ordinary Differential Equations}},
link =
"\url{http://homepage.math.uiowa.edu/~atkinson/papers/NAODE_Book.pdf}",
abstract = "
This book is an expanded version of supplementary notes that we used
for a course on ordinary differential equations for upperdivision
undergraduate students and beginning graduate students in mathematics,
engineering, and sciences. The book introduces the numerical analysis
of differential equations, describing the mathematical background for
understanding numerical methods and giving information on what to
expect when using them. As a reason for studying numerical methods as
a part of a more general course on differential equations, many of the
basic ideas of the numerical analysis of differential equations are
tied closely to theoretical behavior associated with the problem being
solved. For example, the criteria for the stability of a numerical
method is closely connected to the stability of the differential
equation problem being solved.",
paper = "Atki09.pdf"
}
\end{chunk}

books/axiom.bib  636 ++++++++++++++++++++++++++++++++
books/bookvolbib.pamphlet  655 ++++++++++++++++++++++++++++
changelog  2 +
patch  779 ++++++++++++++++++++++++++++++++++
src/axiomwebsite/patches.html  4 +
5 files changed, 1836 insertions(+), 240 deletions()
diff git a/books/axiom.bib b/books/axiom.bib
index 4b710de..b34c93e 100644
 a/books/axiom.bib
+++ b/books/axiom.bib
@@ 3459,6 +3459,16 @@ paper = "Brea89.pdf"
paper = "Coll87.pdf"
}
+@article{Cool65,
+ author = "Cooley, James W. and Tukey, John W.",
+ title = {{An Algorithm for the Machine Calculation of Complex Fourier
+ Series}},
+ journal = "Mathematics of Computation",
+ volume = "19",
+ number = "04",
+ year = "1965"
+}
+
@article{Dave17,
author = "Davenport, James H.",
title = {{A Generalized Successive Resultants Algorithm}},
@@ 6623,6 +6633,63 @@ paper = "Brea89.pdf"
paper = "Ma90.pdf"
}
+@phdthesis{Nayl00,
+ author = "Naylor, Bill",
+ title = {{Polynomial GCD Using Straight Line Program Representation}},
+ school = "University of Bath",
+ year = "2000",
+ link = "\url{http://www.sci.csd.uwo.ca/~bill/thesis.ps}",
+ abstract = "
+ This thesis is concerned with calculating polynomial greatest common
+ divisors using straight line program representation.
+
+ In the Introduction chapter, we introduce the problem and describe
+ some of the traditional representations for polynomials, we then talk
+ about some of the general subjects central to the thesis, terminating
+ with a synopsis of the category theory which is central to the Axiom
+ computer algebra system used during this research.
+
+ The second chapter is devoted to describing category theory. We follow
+ with a chapter detailing the important sections of computer code
+ written in order to investigate the straight line program subject.
+ The following chapter on evalution strategies and algorithms which are
+ dependant on these follows, the major algorith which is dependant on
+ evaluation and which is central to our theis being that of equality
+ checking. This is indeed central to many mathematical problems.
+ Interpolation, that is the determination of coefficients of a
+ polynomial is the subject of the next chapter. This is very important
+ for many straight line program algorithms, as their noncanonical
+ structure implies that it is relatively difficult to determine
+ coefficients, these being the basic objects that many algorithms work
+ on. We talk about three separate interpolation techniques and compare
+ their advantages and disadvantages. The final two chapters describe
+ some of the results we have obtained from this research and finally
+ conclusions we have drawn as to the viability of the straight line
+ program approach and possible extensions.
+
+ Finally we terminate with a number of appendices discussing side
+ subjects encountered during the thesis.",
+ paper = "Nayl00.pdf"
+}
+
+@inproceedings{Shou93,
+ author = "Shoup, Victor",
+ title = {{Factoring Polynomials over Finite Fields:
+ Asymptotic Complexity vs Reality*}},
+ booktitle = "Proc. IMACS Symposium, Lille, France",
+ year = "1993",
+ link = "\url{http://www.shoup.net/papers/lille.pdf}",
+ abstract =
+ "This paper compares the algorithms by Berlekamp, Cantor and
+ Zassenhaus, and Gathen and Shoup to conclude that (a) if large
+ polynomials are factored the FFT should be used for polynomial
+ multiplication and division, (b) Gathen and Shoup should be used if
+ the number of irreducible factors of $f$ is small. (c) if nothing is
+ know about the degrees of the factors then Berlekamp's algorithm
+ should be used.",
+ paper = "Shou93.pdf"
+}
+
@inproceedings{Hoei04,
author = "van Hoeij, Mark and Monagan, Michael",
title = {{Algorithms for Polynomial GCD Computation over Algebraic
@@ 6645,11 +6712,58 @@ paper = "Brea89.pdf"
paper = "Hoei04.pdf"
}
+@article{Wang78,
+ author = "Wang, Paul S.",
+ title = {{An Improved Multivariate Polynomial Factoring Algorithm}},
+ journal = "Mathematics of Computation",
+ volume = "32",
+ number = "144",
+ year = "1978",
+ pages = "12151231",
+ link = "\url{http://www.ams.org/journals/mcom/197832144/S00255718197805682843/S00255718197805682843.pdf}",
+ abstract = "
+ A new algorithm for factoring multivariate polynomials over the
+ integers based on an algorithm by Wang and Rothschild is described.
+ The new algorithm has improved strategies for dealing with the known
+ problems of the original algorithm, namely, the leading coefficient
+ problem, the badzero problem and the occurence of extraneous factors.
+ It has an algorithm for correctly predetermining leading coefficients
+ of the factors. A new and efficient padic algorith named EEZ is
+ described. Basically it is a linearly convergent variablebyvariable
+ parallel construction. The improved algorithm is generally faster and
+ requires less store than the original algorithm. Machine examples with
+ comparative timing are included.",
+ paper = "Wang78.pdf"
+}
+
+@misc{Baez09,
+ author = "Baez, John C.; Stay, Mike",
+ title = {{Physics, Topology, Logic and Computation: A Rosetta Stone}},
+ link = "\url{http://arxiv.org/pdf/0903.0340v3.pdf}",
+ abstract = "
+ In physics, Feynman diagrams are used to reason about quantum
+ processes. In the 1980s, it became clear that underlying these
+ diagrams is a powerful analogy between quantum physics and
+ topology. Namely, a linear operator behaves very much like a
+ ``cobordism'': a manifold representing spacetime, going between two
+ manifolds representing space. But this was just the beginning: simiar
+ diagrams can be used to reason about logic, where they represent
+ proofs, and computation, where they represent programs. With the rise
+ of interest in quantum cryptography and quantum computation, it became
+ clear that there is an extensive network of analogies between physics,
+ topology, logic and computation. In this expository paper, we make
+ some of these analogies precise using the concept of ``closed
+ symmetric monodial category''. We assume no prior knowledge of
+ category theory, proof theory or computer science.",
+ paper = "Baez09.pdf"
+}
+
@misc{Meij91,
author = "Meijer, Erik and Fokkinga, Maarten and Paterson, Ross",
title = {{Functional Programming with Bananas, Lenses, Envelopes and
Barbed Wire}},
 link = "\url{http://eprints.eemcs.utwente.nl/7281/01/dbutwente40501F46.pdf}",
+ link =
+ "\url{http://eprints.eemcs.utwente.nl/7281/01/dbutwente40501F46.pdf}",
abstract = "
We develop a calculus for lazy functional programming based on
recursion operators associated with data type definitions. For these
@@ 7335,6 +7449,32 @@ paper = "Brea89.pdf"
}
+@techreport{Bled79,
+ author = "Bledsoe, W.W. and Bruell, P. and Shostak, R.",
+ title = {{A Prover for General Inequalities}},
+ type = "technical report",
+ institution = "Univ. of Texas at Austin",
+ year = "1979",
+ number = "ATP40A"
+}
+
+@techreport{Bled83,
+ author = "Bledsoe, W.W.",
+ title = {{The UT Natural Deduction Prover}},
+ type = "technical report",
+ institution = "Univ. of Texas at Austin",
+ year = "1983",
+ number = "ATP17B"
+}
+
+@inproceedings{Bled84,
+ author = "Bledsoe, W.W.",
+ title = {{Some Automatic Proofs in Analysis}},
+ booktitle = "Automated Theorem Proving: After 25 Years",
+ publisher = "American Mathematical Society",
+ year = "1984"
+}
+
@misc{Bold07,
author = "Boldo, Sylvie and Filliatre, JeanChristophe",
title = {{Formal Verification of FloatingPoint programs}},
@@ 7675,6 +7815,28 @@ paper = "Brea89.pdf"
paper = "Bulo10.pdf"
}
+@inproceedings{Bund75,
+ author = "Bundy, Alan and Wallen, Lincoln",
+ title = {{The UT Theorem Prover}},
+ booktitle = "Catalogue of Artificial Intelligence Tools",
+ pages = "132133",
+ year = "1975",
+ abstract =
+ "The UT theorem prover is probably the best known natural deduction
+ <153> theorem prover. It was written in LISP <34> by woody Bledsoe and
+ his coworkers at the University of Texas, and is best described in
+ (Bledsoe and Tyson 75]. The theorem prover embodies a Gentzenlike
+ deduction system for firstorder predicate calculus, and many special
+ purpose techniques, including: subgoaling, rewrite rules, controlled
+ lorward chaining, controlled definition instantiation, conditional
+ procedures, and induction. The prover, though powerful in its own
+ right, is essentially interactive and thus allows the user of the
+ prover to control the search for the proof in radical ways. The user
+ can for example : add hypotheses, instruct the prover to instantiate
+ certain variables with values, or instruct the prover as to which
+ deduction rule to use next."
+}
+
@article{Bund88,
author = "Bundy, Alan",
title = {{The Use of Explicit Plans to Guide Inductive Proofs}},
@@ 8130,6 +8292,18 @@ paper = "Brea89.pdf"
isbn = "9780521457019"
}
+@misc{Daly10,
+ author = "Daly, Timothy",
+ title = {{Intel Instruction Semantics Generator}},
+ link = "\url{http://daly.axiomdeveloper.org/TimothyDaly_files/publications/sei/intel/intel.pdf}",
+ abstract =
+ "Given an Intel x86 binary, extract the semantics of the instruction
+ stream as Conditional Concurrent Assignments (CCAs). These CCAs
+ represent the semantics of each individual instruction. They can be
+ composed to represent higher level semantics.",
+ paper = "Daly10.pdf"
+}
+
@InProceedings{Dani06,
author = "Danielsson, Nils Anders and Hughes, John and Jansson, Patrik and
Gibbons, Jeremy",
@@ 8169,6 +8343,13 @@ paper = "Brea89.pdf"
school = "University of Bath"
}
+@misc{Dave98,
+ author = "Davenport, James H.",
+ title = {{Is Computer Algebra the same as Computer Mathematics?}},
+ year = "1998",
+ comment = "Talk for British Colloquium for Theoretical Computer Science"
+}
+
@article{Dave08,
author = "Davenport, James H.",
title = {{Effective Set Membership in Computer Algebra and Beyond}},
@@ 8366,6 +8547,21 @@ paper = "Brea89.pdf"
keywords = "axiomref, CASProof"
}
+@misc{Duns00,
+ author = "Dunstan, Martin N.",
+ title = {{Adding Larch/Aldor Specifications to Aldor}},
+ abstract =
+ "We describe a proposal to add Larchstyle annotations to the Aldor
+ programming language, based on our PhD research. The annotations
+ are intended to be machinecheckable and may be used for a variety
+ of purposes ranging from compiler optimizations to verification
+ condition (VC) generation. In this report we highlight the options
+ available and describe the changes which would need to be made to
+ the compiler to make use of this technology.",
+ paper = "Duns00.pdf",
+ keywords = "axiomref"
+}
+
@InProceedings{Duns98,
author = "Dunstan, Martin and Kelsey, Tom and Linton, Steve and
Martin, Ursula",
@@ 8425,6 +8621,29 @@ paper = "Brea89.pdf"
keywords = "axiomref, CASProof"
}
+@article{Farm93a,
+ author = "Farmer, William M. and Guttman, Joshua D. and Thayer, Javier",
+ title = {{IMPS: An Interactive Mathematical Proof Systems}},
+ journal = "J. of Automated Reasoning",
+ volume = "11",
+ pages = "213248",
+ year = "1993",
+ abstract =
+ "IMPS is an interactive mathematical proof system intended as a
+ generalpurpose too! formulating and applying mathematics in a
+ familiar fashion. The logic of IMPS is based on a version of simple
+ type theory with partial functions and subtypes. Mathematical
+ specification and inference are performed relative to axiomatic
+ theories, which can be related to one another via inclusion and theory
+ interpretation. IMPS provides relatively large primitive inference
+ steps to facilitate human control of the deductive process and human
+ comprehension of the resulting proofs. An initial theory library con
+ taining over a thousand repeatable proofs covers significant portions
+ of logic, algebra, and analysis and provides some support for modeling
+ applications in computer science.",
+ paper = "Farm93a.pdf"
+}
+
@article{Farm93,
author = "Farmer, William M. and Guttman, Joshua D. and Thayer, Javier",
title = {{Reasoning with contexts}},
@@ 8500,6 +8719,14 @@ paper = "Brea89.pdf"
keywords = "CASProof"
}
+@book{Fitt90,
+ author = "Fitting, M.",
+ title = {{Firstorder Logic and Automated Theorem Proving}},
+ publisher = "SpringerVerlag",
+ year = "1990",
+ isbn = "9781461275152"
+}
+
@article{Frad08,
author = "Frade, Maria Joao",
title = {{Calculus of Inductive Construction. Software Formal Verification}},
@@ 8549,6 +8776,15 @@ paper = "Brea89.pdf"
isbn = "9780262062794"
}
+@book{Gall86,
+ author = "Gallier, Jean H.",
+ title = {{Logic for Computer Science: Foundations of Automatic
+ Theorem Proving}},
+ publisher = "Harper and Row",
+ year = "1986",
+ isbn = "9780486780825"
+}
+
@book{Gedd94,
author = "Geddes, D.",
title = {{The DTP Manual}},
@@ 8799,7 +9035,7 @@ paper = "Brea89.pdf"
@book{Gutt93,
author = "Guttag, John V. and Horning, James J.",
 title = {{LARCH: Languages and TOols for Formal Specifications}},
+ title = {{LARCH: Languages and Tools for Formal Specifications}},
publisher = "SpringerVerlag",
year = "1993",
isbn = "3540940065"
@@ 9032,13 +9268,13 @@ paper = "Brea89.pdf"
year = "1994"
}
@phdthesis{Homa96,
+@phdthesis{Homa96a,
author = "Homann, Karsten",
title = {{Symbolisches L\"osen mathematischer Probleme durch
Kooperation algorithmischer und logischer Systeme}},
year = "1996",
school = {Universit\"at Karlsruhe},
 paper = "Homa96.pdf"
+ paper = "Homa96a.pdf"
}
@misc{Howa80,
@@ 9612,6 +9848,29 @@ paper = "Brea89.pdf"
abstract = "Demonstration of Euclid Algorithm Proof in TLA+"
}
+@article{Wony18,
+ author = "Lee, Wonyeol and Sharma, Rahul and Aiken, Alex",
+ title = {{On Automatically Proving the Correctness of math.h
+ Implementation}},
+ journal = "Proc. ACM Programming Languages",
+ volume = "2",
+ number = "42",
+ year = "2018",
+ pages = "132",
+ abstract =
+ "Industry standard implementations of math.h claim (often without
+ formal proof) tight bounds on floating point errors. We demonstrate a
+ novel static analysis that proves these bounds and verifies the
+ correctness of these implementations. Our key insight is a reduction
+ of this verification task to a set of mathematical optimization
+ problems that can be solved by offtheshelf computer algebra
+ systems. We use this analysis to prove the correctness of
+ implementations in Intel’s math library automatically. Prior to this
+ work, these implementations could only be verified with significant
+ manual effort.",
+ paper = "Wony18.pdf"
+}
+
@misc{Lond74,
author = "London, Ralph L. and Musser, David R.",
title = {{The Application of a Symbolic Mathematical System to Program
@@ 9948,6 +10207,14 @@ paper = "Brea89.pdf"
}
+@misc{Mesh05,
+ author = "Meshveliani, Sergei D.",
+ title = {{Term rewriting, Equationional Reasoning, Automatic proofs}},
+ link = "\url{ftp://ftp.botik.ru/pub/local/Mechveliani/dumatel/1.02/}",
+ year = "2005",
+ paper = "Mesh05.pdf"
+}
+
@misc{Mesh13,
author = "Meshveliani, Sergei D.",
title = {{Dependent Types for an Adequate Programming of Algebra}},
@@ 10240,6 +10507,35 @@ paper = "Brea89.pdf"
keywords = "CASProof"
}
+@misc{Newc13,
+ author = "Newcombe, Chris and Rath, Tim and Zhang, Fan and
+ Munteanu, Bogdan and Brooker, Marc and Deardeuff, Michael",
+ title = {{Use of Formal Methods at Amazon Web Services}},
+ link = "\url{http://research.microsoft.com/enus/um/people/lamport/tla/formalmethodsamazon.pdf}",
+ abstract =
+ "In order to find subtle bugs in a system design, it is necessary to
+ have a precise description of that design. There are at least two
+ major benefits to writing a precise design; the author is forced to
+ think more clearly, which helps eliminate ``plausible handwaving'',
+ and tools can be applied to check for errors in the design, even while
+ it is being written. In contrast, conventional design documents
+ consist of prose, static diagrams, and perhaps pseudocode in an ad
+ hoc untestable language. Such descriptions are far from precise; they
+ are often ambiguous, or omit critical aspects such as partial failure
+ or the granularity of concurrency (i.e. which constructs are assumed
+ to be atomic). At the other end of the spectrum, the final executable
+ code is unambiguous, but contains an overwhelming amount of detail. We
+ needed to be able to capture the essence of a design in a few hundred
+ lines of precise description. As our designs are unavoidably complex,
+ we need a highlyexpressive language, far above the level of code, but
+ with precise semantics. That expressivity must cover realworld
+ concurrency and faulttolerance. And, as we wish to build services
+ quickly, we wanted a language that is simple to learn and apply,
+ avoiding esoteric concepts. We also very much wanted an existing
+ ecosystem of tools. We found what we were looking for in TLA+, a
+ formal specification language."
+}
+
@book{Nipk14,
author = "Nipkow, Tobias and Klein, Gerwin",
title = {{Concrete Semantics}},
@@ 10308,6 +10604,29 @@ paper = "Brea89.pdf"
paper = "Nord90.pdf"
}
+@misc{OCon15,
+ author = {O'Connor, Liam},
+ title = {{Write Your Compiler by Proving It Correct}},
+ year = "2015",
+ link = "\url{http://liamoc.net/posts/20150823verifiedcompiler.html}",
+ abstract =
+ "Recently my research has been centered around the development of a
+ selfcertifying compiler for a functional language with linear types
+ called Cogent (see O'Connor et al. [2016]). The compiler works by
+ emitting, along with generated lowlevel code, a proof in Isabelle/HOL
+ (see Nipkow et al. [2002]) that the generated code is a refinement of
+ the original program, expressed via a simple functional semantics in HOL.
+
+ As dependent types unify for us the language of code and proof, my
+ current endeavour has been to explore how such a compiler would look
+ if it were implemented and verified in a dependently typed programming
+ language instead. In this post, I implement and verify a toy compiler
+ for a language of arithmetic expressions and variables to an idealised
+ assembly language for a virtual stack machine, and explain some of the
+ useful features that dependent types give us for writing verified
+ compilers."
+}
+
@article{Pada80,
author = "Padawitz, Peter",
title = {{New results on completeness and consistency of abstract data
@@ 10636,7 +10955,8 @@ paper = "Brea89.pdf"
title = {{Adding the axioms to Axiom. Toward a system of automated
reasoning in Aldor}},
year = "1998",
 link = "\url{http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.1457}",
+ link =
+ "\url{http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.1457}",
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
@@ 10835,6 +11155,34 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@techreport{Sack87,
+ author = "Sacks, Elisha",
+ title = {{Hierarchical Reasoning about Inequalities}},
+ institution = "MIT",
+ year = "1987",
+ abstract =
+ "This paper describes a program called BOUNDER that proves
+ inequalities between functions over finite sets of constraints.
+ Previous inequality algorithms perform well on some subset of the
+ elementary functions, but poorly elsewhere. To overcome this problem,
+ BOUNDER maintains a hierarchy of increasingly complex algorithms.
+ When one fails to resolve an inequality, it tries the next. This
+ strategy resolves more inequalities than any single algorithm. It
+ also performs well on hard problems without wasting time on easy
+ ones. The current hierarchy consists of four algorithms: bounds
+ propagation, substitution, derivative inspection, and iterative
+ approximation. Propagation is an extension of interval arithmetic
+ that takes linear time, but ignores constraints between variables
+ and multiple occurrences of variables. The remaining algorithms
+ consider these factors, but require exponential time. Substitution
+ is a new, provably correct, algorithm for utilizing constraints
+ between variables. The final two algorithms analyze constraints
+ between variables. Inspection examines the signs of partial
+ derivatives. Iteration is based on several earlier algorithms
+ from interval arithmetic.",
+ paper = "Sack87.pdf"
+}
+
@phdthesis{Schw97,
author = "Schwarzweller, Christoph",
title = {{MIZAR verification of generic algebraic algorithms}},
@@ 11009,6 +11357,20 @@ paper = "Brea89.pdf"
paper = "Ther01.pdf"
}
+@article{Ther98,
+ author = "Thery, Laurent",
+ title = {{A Certified Version of Buchberger's Algorithm}},
+ journal = "LNCS",
+ volume = "1421",
+ pages = "349364",
+ year = "1998",
+ abstract =
+ "We present a proof of Buchberger's algorithm that has been developed
+ in the Coq proof assistant. The formulation of the algorithm in Coq
+ can be efficiently compiled and used to do computation",
+ paper = "Ther98.pdf"
+}
+
@article{Tray11,
author = "Traytel, Dmitriy and Berghofer, Stefan and Nipkow, Tobias",
title = {{Extending HindleyMilner Type Inference with Coercive
@@ 11275,6 +11637,31 @@ paper = "Brea89.pdf"
paper = "Boeh86.pdf"
}
+@misc{Brig04,
+ author = "Briggs, Keith",
+ title = {{Exact real arithmetic}},
+ link = "\url{http://keithbriggs.info/documents/xrkenttalkpp.pdf}",
+ year = "2004",
+ paper = "Bri04.pdf"
+}
+
+@misc{Fate94a,
+ author = "Fateman, Richard J.; Yan, Tak W.",
+ title ={{Computation with the Extended Rational Numbers and an
+ Application to Interval Arithmetic}},
+ link = "\url{http://www.cs.berkeley.edu/~fateman/papers/extrat.pdf}",
+ abstract = "
+ Programming languages such as Common Lisp, and virtually every
+ computer algebra system (CAS), support exact arbitraryprecision
+ integer arithmetic as well as exect rational number computation.
+ Several CAS include interval arithmetic directly, but not in the
+ extended form indicated here. We explain why changes to the usual
+ rational number system to include infinity and ``notanumber'' may be
+ useful, especially to support robust interval computation. We describe
+ techniques for implementing these changes.",
+ paper = "Fate94a.pdf"
+}
+
@misc{Gust16,
author = "Gustafson, John",
title ={{A Radical Approach to Computation with Real Numbers}},
@@ 11328,6 +11715,28 @@ paper = "Brea89.pdf"
pages = "102113"
}
+@misc{Atki09,
+ author = "Atkinson, Kendall and Han, Welmin and Stewear, David",
+ title = {{Numerical Solution of Ordinary Differential Equations}},
+ link =
+ "\url{http://homepage.math.uiowa.edu/~atkinson/papers/NAODE_Book.pdf}",
+ abstract = "
+ This book is an expanded version of supplementary notes that we used
+ for a course on ordinary differential equations for upperdivision
+ undergraduate students and beginning graduate students in mathematics,
+ engineering, and sciences. The book introduces the numerical analysis
+ of differential equations, describing the mathematical background for
+ understanding numerical methods and giving information on what to
+ expect when using them. As a reason for studying numerical methods as
+ a part of a more general course on differential equations, many of the
+ basic ideas of the numerical analysis of differential equations are
+ tied closely to theoretical behavior associated with the problem being
+ solved. For example, the criteria for the stability of a numerical
+ method is closely connected to the stability of the differential
+ equation problem being solved.",
+ paper = "Atki09.pdf"
+}
+
@book{Hamm62,
author = "Hamming, R W.",
title = {{Numerical Methods for Scientists and Engineers}},
@@ 11550,6 +11959,13 @@ paper = "Brea89.pdf"
paper = "Bron02.pdf"
}
+@misc{Bron02a,
+ author = "Bronstein, Manuel",
+ title = {{$\Sigma^{it}$ User Guide and Reference Manual}},
+ year = "2002",
+ paper = "Bron02a.pdf"
+}
+
\bibitem[Davenport 86]{Dav86} Davenport, J.H.
@article{Dave86,
author = "Davenport, James H.",
@@ 13763,6 +14179,7 @@ paper = "Brea89.pdf"
with branch cuts etc}},
journal = "14th Int. Symp. on Symbolic and Numeric Algorithms for
Scientific Computing",
+ link = "\url{http://arxiv.org/pdf/1212.5417.pdf}",
year = "2012",
series = "SYNASC'12",
pages = "8388",
@@ 22929,6 +23346,7 @@ paper = "Brea89.pdf"
The problem of implicitization is an active topic where research is
still taking place. Examples of further research points are included
in the conclusion",
+ paper = "ElAl01.pdf",
keywords = "axiomref"
}
@@ 24261,6 +24679,15 @@ paper = "Brea89.pdf"
number = "3",
pages = "2528",
year = "1979",
+ abstract =
+ "When I was first asked to give this banquet talk, I was somewhat
+ hesitant to accept. I have not been very heavily involved in the field
+ of symbolic and algebraic manipulation for the past three years. I
+ have contented myself with such behindthescenes activities as
+ serving as an associate editor for the ACM Transactions on
+ Mathematical Software and as a member of the SIGSAM Nominating
+ Committees two years ago and again this year.",
+ paper = "Grie79.pdf",
keywwords = "axiomref"
}
@@ 25809,6 +26236,15 @@ paper = "Brea89.pdf"
beebe = "Keady:1994:PAS"
}
+@phdthesis{Kels99,
+ author = "Kelsey, Tom",
+ title = {{Formal Methods and Computer Algebra: A Larch Specification of
+ AXIOM Categories and Functors}},
+ school = "University of St Andrews",
+ year = "1999",
+ keywords = "axiomref"
+}
+
@misc{Kels00a,
author = "Kelsey, Tom",
title = {{Formal specification of computer algebra}},
@@ 25874,6 +26310,20 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@misc{Kenn01,
+ author = "Kennedy, A.D.",
+ title = {{Semantics of Categories in Aldor}},
+ year = "2001",
+ abstract =
+ "We consider some questions about the semantics of Aldor regarding the
+ way that types can be considered on an equal footing with any other
+ objects in the language. After a digression into the relationship
+ between Aldor categories and mathematical categories, we shall discuss
+ the more practical issue of the limitations of the {\tt define}
+ keyword and what the compiler should do about them.",
+ paper = "Kenn01.pdf"
+}
+
@article{Kerb98,
author = "Kerber, Manfred and Kohlhase, Michael and Volker, Sorge",
title = {{Integrating computer algebra into proof planning}},
@@ 28558,7 +29008,7 @@ paper = "Brea89.pdf"
@article{Seil94b,
author = "Seiler, Werner Markus",
 title = {{Pseudo differential operators and integrable systems in AXIOM}},
+ title = {{Pseudo Differential Operators and Integrable Systems in AXIOM}},
journal = "Computer Physics Communications",
volume = "79",
number = "2",
@@ 29378,6 +29828,28 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@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",
+ link =
+ "\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.",
+ paper = "Thom01.pdf",
+ keywords = "axiomref"
+}
+
@misc{Thomxx,
author = "Thompson, Simon and Timochouk, Leonid",
title = {{The Aldor\\ language}},
@@ 29403,7 +29875,8 @@ paper = "Brea89.pdf"
title = {{Etude du typage dans le syst\`eme de calcul scientifique Aldor}},
comment = "Study of types in the Aldor scientific computation system",
year = "1998",
 link = "\url{http://axiomwiki.newsynthesis.org/public/refs/AldorT1998_04.pdf}",
+ link =
+ "\url{http://axiomwiki.newsynthesis.org/public/refs/AldorT1998_04.pdf}",
paper = "Tour98.pdf",
keywords = "axiomref"
}
@@ 29883,6 +30356,14 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@misc{Watt01,
+ author = "Watt, Stephen M. and Broadbery, Peter A. and Iglio, Pietro and
+ Morrison, Scott C. and Steinbach, Jonathan M",
+ title = {{FOAM: A First Order Abstract Machine Version 0.35}},
+ year = "2001",
+ paper = "Watt01.pdf"
+}
+
@misc{Watt00,
author = "Watt, Stephen M.",
title = {{Aldor: The language and recent directions}},
@@ 30050,7 +30531,7 @@ paper = "Brea89.pdf"
keywords = "axiomref, coercion"
}
@InProceedings{Webe94,
+@Inproceedings{Webe94,
author = "Weber, Andreas",
title = {{Algorithms for Type Inference with Coercions}},
booktitle = "Proc ISSAC 94",
@@ 31276,6 +31757,29 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@article{Chur40,
+ author = "Church, Alonzo",
+ title = {{A Formulation of the Simple Theory of Types}},
+ journal = "J. of Symbolic Logic",
+ volume = "5",
+ number = "2",
+ year = "1940",
+ pages = "5668",
+ abstract =
+ "The purpose of the present paper is to give a formulation of the
+ simple theory of types which incorporates certain features of the
+ calculus of $\lambda$conversion. A complete incorporation of the
+ calculus of $\lambda$conversion into the theory of types is
+ impossible if we require that $\lambda x$ and juxtaposition shall
+ retain their respective meanings as an abstraction operator and as
+ denoting the application of function to argument. But the present
+ partial incorporation has certain advantages from the point of view of
+ type theory and is offered as being of interest on this basis
+ (whatever may be thought of the finally satisfactory character of the
+ theory of types as a foundation for logic and mathematics).",
+ paper = "Chur40.pdf"
+}
+
@techreport{Clar92,
author = "Clarke, Edmund and Zhao, Xudong",
title = {{Analytica  An Experiment in Combining Theorem Proving and
@@ 31383,6 +31887,26 @@ paper = "Brea89.pdf"
paper = "Corl92.pdf"
}
+@article{Cunn85,
+ author = "Cunningham, R.J. and Dick, A.J.J",
+ title = {{Rewrite Systems on a Lattice of Types}},
+ journal = "Acta Informatica",
+ volume = "22",
+ pages = "149169",
+ year = "1985",
+ abstract =
+ "Rewriting systems for partial algebras are developed by modifying
+ the KnuthBendix completion algorithm to permit the use of
+ latticestructured domains. Some problems with the original algorithm,
+ such as the treatment of division rings, are overcome conveniently by
+ this means. The use of a type lattice also gives a natural framework
+ for specifying data types in Computer Science without overspecifying
+ error situations. The soundness and meaning of the major concepts
+ involed in rewriting systems are reviewed when applied to such
+ structures.",
+ paper = "Cunn85.pdf"
+}
+
@misc{Dave80b,
author = "Davenport, J.H. and Jenks, R.D.",
title = {{SCRATCHPAD/370: Modes and Domains}},
@@ 31624,6 +32148,14 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@inproceedings{Enge65,
+ author = "Engelman, C.",
+ title = {{A Program for OnLine Assistance in Symbolic Computation}},
+ booktitle = "Proc. Fall Joint Comput. Conf. 2",
+ year = "1965",
+ publisher = "Spartan Books"
+}
+
@misc{Fate08,
author = "Fateman, Richard J.",
title = {{Revisiting numeric/symbolic indefinite integration of rational
@@ 31778,6 +32310,26 @@ paper = "Brea89.pdf"
more efficient and reliable programs."
}
+@article{Gues87,
+ author = "Guessarian, Irene and Meseguer, Jose",
+ title = {{On the Axiomatization of ``IFTHENELSE''}},
+ journal = "SIAM J. Comput.",
+ volume = "16",
+ numbrrer = "2",
+ year = "1987",
+ pages = "332357",
+ abstract =
+ "The equationally complete proof system for ``ifthenelse'' of Bloom
+ and Tindell is extended to a complete proof system for manyosrted
+ algebras with extra operations, predicates and equations among
+ those. We give similar completeness results for continuous algebras
+ and program schemes (infinite trees) by the methods of algebraic
+ semantics. These extensions provide a purely equational proof system
+ to prove properties of functional programs over userdefinable data
+ types.",
+ paper = "Gues87.pdf"
+}
+
@article{Hach95,
author = "Hach\'e, G. and Le Brigand, D.",
title = {{Effective construction of algebraic geometry codes}},
@@ 31912,7 +32464,7 @@ paper = "Brea89.pdf"
keywords = "axiomref, CASProof"
}
@article{Hom965,
+@article{Homa96,
author = "Homann, Karsten and Calmet, Jacques",
title = {{Structures for Symbolic Mathematical Reasoning and Computation}},
journal = "LNCS",
@@ 32821,6 +33373,27 @@ paper = "Brea89.pdf"
isbn = "026216082X"
}
+@article{Paul90,
+ author = "Paulson, Lawrence C.",
+ title = {{A Formulation of the Simple Theory of Types (for
+ Isabelle}}},
+ journal = "LNCS",
+ volume = "417",
+ pages = "246274",
+ year = "1990",
+ abstract =
+ "Simple type theory is formulated for use with the generic theorem
+ prover Isabelle. This requires explicit type inference rules. There
+ are function, product, and subset types, which may be
+ empty. Descriptions (the etaoperator) introduce the Axiom of
+ Choice. Higherorder logic is obtained through reflection between
+ formulae and terms of type bool. Recursive types and functions can be
+ formally constructed. Isabelle proof procedures are described. The
+ logic appears suitable for general mathematics as well as
+ computational problems.",
+ paper = "Paul90.pdf"
+}
+
@book{Pear56,
author = "Pearcey, T.",
title = {{Table of the Fresnel Integral}},
@@ 32965,6 +33538,13 @@ paper = "Brea89.pdf"
}
+@book{Redf98,
+ author = "Redfern, D.",
+ title = {{The Maple Handbook: Maple V Release 5}},
+ publisher = "Springer",
+ year = "1998"
+}
+
@article{Redf27,
author = "Redfield, J. Howard",
title = {{The Theory of GroupReduced Distributions}},
@@ 33034,6 +33614,26 @@ paper = "Brea89.pdf"
paper = "Rube06.pdf"
}
+@article{Rump88,
+ author = "Rump, Siegfried M.",
+ title = {{Algebraic Computation, Numerical Computation and Verified
+ Inclusions}},
+ journal = "LNCS",
+ volume = "296",
+ pages = "177197",
+ year = "1988",
+ abstract =
+ "The three different types of computation  the algebraic
+ manipulation, the numerical computation and the computation of
+ verified results  are aiming on different problems and deliver
+ qualitatively different results, each method having its specific
+ advantages for specific classes of problems. The following remarks
+ give some thoughts on possible combinations of all three methods to
+ obtain algorithms benefitting from the specific strength of either
+ method.",
+ paper = "Rump88.pdf"
+}
+
@book{Saun79,
author = "MacLane, Saunders and Birkhoff, Garrett",
title = {{Algebra, Second Edition}},
@@ 33149,6 +33749,15 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@misc{Sorg96,
+ author = "Sorge, Volker",
+ title = {{Integration eines Computeralgebrasystems in eine logische
+ Beweisumgebung }},
+ school = "Univ. des Saarlandes",
+ year = "1996",
+ comment = "Master's thesis"
+}
+
@article{Sorg00,
author = "Sorge, Volker",
title = {{Nontrivial Symbolic Computations in Proof Planning}},
@@ 33201,15 +33810,16 @@ paper = "Brea89.pdf"
}
@article{Supp89,
 author = "Suppes, Patrick and Takahashi, Shuzo",
 title = {{An Interactive Calculus TheoremProver for Continuity Properties}},
+ author = "Suppes, P. and Takahashi, S.",
+ title = {{An Interactive Calculus Theoremprover for Continuity
+ Properites}},
journal = "J. Symbolic Computation",
volume = "7",
number = "6",
 pages = "573590",
year = "1989",
+ pages = "573590",
abstract =
 "The work reported concerns the development of an interactive
+ "he work reported concerns the development of an interactive
theoremprover for the foundationsof the differential and integral
calculus. The main tools are a resolution theoremprover VERIFY,
previously developed for interactive proofs in set theory, and the
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 85eb8cc..1c89504 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 4884,6 +4884,21 @@ when shown in factored form.
\end{chunk}
+\index{Cooley, James W.}
+\index{Tukey, John W.}
+\begin{chunk}{axiom.bib}
+@article{Cool65,
+ author = "Cooley, James W. and Tukey, John W.",
+ title = {{An Algorithm for the Machine Calculation of Complex Fourier
+ Series}},
+ journal = "Mathematics of Computation",
+ volume = "19",
+ number = "04",
+ year = "1965"
+}
+
+\end{chunk}
+
\index{Davenport, James H.}
\begin{chunk}{axiom.bib}
@article{Dave17,
@@ 9072,10 +9087,12 @@ when shown in factored form.
\end{chunk}
\index{Naylor, William A.}
\begin{chunk}{ignore}
\bibitem[Naylor 00a]{N00} Naylor, Bill
+\begin{chunk}{axiom.bib}
+@phdthesis{Nayl00,
+ author = "Naylor, Bill",
title = {{Polynomial GCD Using Straight Line Program Representation}},
PhD. Thesis, University of Bath, 2000
+ school = "University of Bath",
+ year = "2000",
link = "\url{http://www.sci.csd.uwo.ca/~bill/thesis.ps}",
abstract = "
This thesis is concerned with calculating polynomial greatest common
@@ 9107,25 +9124,30 @@ PhD. Thesis, University of Bath, 2000
Finally we terminate with a number of appendices discussing side
subjects encountered during the thesis.",
 paper = "N00.pdf"
+ paper = "Nayl00.pdf"
+}
\end{chunk}
\index{Shoup, Victor}
\begin{chunk}{ignore}
\bibitem[Shoup 93]{STPGCDSh93} Shoup, Victor
 title = {{Factoring Polynomials over Finite Fields: Asymptotic Complexity vs Reality*}},
Proc. IMACS Symposium, Lille, France, (1993)
+\begin{chunk}{axiom.bib}
+@inproceedings{Shou93,
+ author = "Shoup, Victor",
+ title = {{Factoring Polynomials over Finite Fields:
+ Asymptotic Complexity vs Reality*}},
+ booktitle = "Proc. IMACS Symposium, Lille, France",
+ year = "1993",
link = "\url{http://www.shoup.net/papers/lille.pdf}",
 abstract = "
 This paper compares the algorithms by Berlekamp, Cantor and
+ abstract =
+ "This paper compares the algorithms by Berlekamp, Cantor and
Zassenhaus, and Gathen and Shoup to conclude that (a) if large
polynomials are factored the FFT should be used for polynomial
multiplication and division, (b) Gathen and Shoup should be used if
the number of irreducible factors of $f$ is small. (c) if nothing is
know about the degrees of the factors then Berlekamp's algorithm
should be used.",
 paper = "STPGCDSh93.pdf"
+ paper = "Shou93.pdf"
+}
\end{chunk}
@@ 9157,10 +9179,15 @@ Proc. IMACS Symposium, Lille, France, (1993)
\end{chunk}
\index{Wang, Paul S.}
\begin{chunk}{ignore}
\bibitem[Wang 78]{Wang78} Wang, Paul S.
+\begin{chunk}{axiom.bib}
+@article{Wang78,
+ author = "Wang, Paul S.",
title = {{An Improved Multivariate Polynomial Factoring Algorithm}},
Mathematics of Computation, Vol 32, No 144 Oct 1978, pp12151231
+ journal = "Mathematics of Computation",
+ volume = "32",
+ number = "144",
+ year = "1978",
+ pages = "12151231",
link = "\url{http://www.ams.org/journals/mcom/197832144/S00255718197805682843/S00255718197805682843.pdf}",
abstract = "
A new algorithm for factoring multivariate polynomials over the
@@ 9175,13 +9202,7 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp12151231
requires less store than the original algorithm. Machine examples with
comparative timing are included.",
paper = "Wang78.pdf"

\end{chunk}

\begin{chunk}{ignore}
\bibitem[Wiki 4]{Wiki4}.
 title = {{Polynomial greatest common divisor}},
 link = "\url{http://en.wikipedia.org/wiki/Polynomial_greatest_common_divisor}",
+}
\end{chunk}
@@ 9189,8 +9210,9 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp12151231
\index{Baez, John C.}
\index{Stay, Mike}
\begin{chunk}{ignore}
\bibitem[Baez 09]{Baez09} Baez, John C.; Stay, Mike
+\begin{chunk}{axiom.bib}
+@misc{Baez09,
+ author = "Baez, John C.; Stay, Mike",
title = {{Physics, Topology, Logic and Computation: A Rosetta Stone}},
link = "\url{http://arxiv.org/pdf/0903.0340v3.pdf}",
abstract = "
@@ 9209,6 +9231,7 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp12151231
symmetric monodial category''. We assume no prior knowledge of
category theory, proof theory or computer science.",
paper = "Baez09.pdf"
+}
\end{chunk}
@@ 9220,7 +9243,8 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp12151231
author = "Meijer, Erik and Fokkinga, Maarten and Paterson, Ross",
title = {{Functional Programming with Bananas, Lenses, Envelopes and
Barbed Wire}},
 link = "\url{http://eprints.eemcs.utwente.nl/7281/01/dbutwente40501F46.pdf}",
+ link =
+ "\url{http://eprints.eemcs.utwente.nl/7281/01/dbutwente40501F46.pdf}",
abstract = "
We develop a calculus for lazy functional programming based on
recursion operators associated with data type definitions. For these
@@ 10085,6 +10109,46 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp12151231
\end{chunk}
+\index{Bledsoe, W.W.}
+\index{Bruell, P.}
+\index{Shostak, R.}
+\begin{chunk}{axiom.bib}
+@techreport{Bled79,
+ author = "Bledsoe, W.W. and Bruell, P. and Shostak, R.",
+ title = {{A Prover for General Inequalities}},
+ type = "technical report",
+ institution = "Univ. of Texas at Austin",
+ year = "1979",
+ number = "ATP40A"
+}
+
+\end{chunk}
+
+\index{Bledsoe, W.W.}
+\begin{chunk}{axiom.bib}
+@techreport{Bled83,
+ author = "Bledsoe, W.W.",
+ title = {{The UT Natural Deduction Prover}},
+ type = "technical report",
+ institution = "Univ. of Texas at Austin",
+ year = "1983",
+ number = "ATP17B"
+}
+
+\end{chunk}
+
+\index{Bledsoe, W.W.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Bled84,
+ author = "Bledsoe, W.W.",
+ title = {{Some Automatic Proofs in Analysis}},
+ booktitle = "Automated Theorem Proving: After 25 Years",
+ publisher = "American Mathematical Society",
+ year = "1984"
+}
+
+\end{chunk}
+
\index{Boldo, Sylvie}
\index{Filliatre, JeanChristophe}
\begin{chunk}{axiom.bib}
@@ 10525,6 +10589,34 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp12151231
\end{chunk}
\index{Bundy, Alan}
+\index{Wallen, Lincoln}
+\begin{chunk}{axiom.bib}
+@inproceedings{Bund75,
+ author = "Bundy, Alan and Wallen, Lincoln",
+ title = {{The UT Theorem Prover}},
+ booktitle = "Catalogue of Artificial Intelligence Tools",
+ pages = "132133",
+ year = "1975",
+ abstract =
+ "The UT theorem prover is probably the best known natural deduction
+ <153> theorem prover. It was written in LISP <34> by woody Bledsoe and
+ his coworkers at the University of Texas, and is best described in
+ (Bledsoe and Tyson 75]. The theorem prover embodies a Gentzenlike
+ deduction system for firstorder predicate calculus, and many special
+ purpose techniques, including: subgoaling, rewrite rules, controlled
+ lorward chaining, controlled definition instantiation, conditional
+ procedures, and induction. The prover, though powerful in its own
+ right, is essentially interactive and thus allows the user of the
+ prover to control the search for the proof in radical ways. The user
+ can for example : add hypotheses, instruct the prover to instantiate
+ certain variables with values, or instruct the prover as to which
+ deduction rule to use next."
+}
+
+\end{chunk}
+
+
+\index{Bundy, Alan}
\begin{chunk}{axiom.bib}
@article{Bund88,
author = "Bundy, Alan",
@@ 11147,16 +11239,18 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp12151231
\subsection{D} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Daly, Timothy}
\begin{chunk}{ignore}
\bibitem[Daly 10]{Daly10} Daly, Timothy
+\begin{chunk}{axiom.bib}
+@misc{Daly10,
+ author = "Daly, Timothy",
title = {{Intel Instruction Semantics Generator}},
link = "\url{http://daly.axiomdeveloper.org/TimothyDaly_files/publications/sei/intel/intel.pdf}",
 abstract = "
 Given an Intel x86 binary, extract the semantics of the instruction
+ abstract =
+ "Given an Intel x86 binary, extract the semantics of the instruction
stream as Conditional Concurrent Assignments (CCAs). These CCAs
represent the semantics of each individual instruction. They can be
composed to represent higher level semantics.",
paper = "Daly10.pdf"
+}
\end{chunk}
@@ 11212,6 +11306,17 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp12151231
\index{Davenport, James H.}
\begin{chunk}{axiom.bib}
+@misc{Dave98,
+ author = "Davenport, James H.",
+ title = {{Is Computer Algebra the same as Computer Mathematics?}},
+ year = "1998",
+ comment = "Talk for British Colloquium for Theoretical Computer Science"
+}
+
+\end{chunk}
+
+\index{Davenport, James H.}
+\begin{chunk}{axiom.bib}
@article{Dave08,
author = "Davenport, James H.",
title = {{Effective Set Membership in Computer Algebra and Beyond}},
@@ 11234,38 +11339,6 @@ Mathematics of Computation, Vol 32, No 144 Oct 1978, pp12151231
\end{chunk}
\index{Davenport, James H.}
\index{Bradford, Russell}
\index{England, Matthew}
\index{Wilson, David}
\begin{chunk}{ignore}
\bibitem[Davenport 12]{Davenp12} Davenport, James H.; Bradford, Russell;
England, Matthew; Wilson, David
 title = {{Program Verification in the presence of complex numbers,
 functions with branch cuts etc.}},
 link = "\url{http://arxiv.org/pdf/1212.5417.pdf}",
 abstract = "
 In considering the reliability of numerical programs, it is normal to
 ``limit our study to the semantics dealing with numerical precision''.
 On the other hand, there is a great deal of work on the reliability of
 programs that essentially ignores the numerics. The thesis of this
 paper is that there is a class of problems that fall between these
 two, which could be described as ``does the lowlevel arithmetic
 implement the highlevel mathematics''. Many of these problems arise
 because mathematics, particularly the mathematics of the complex
 numbers, is more difficult than expected: for example the complex
 function log is not continuous, writing down a program to compute an
 inverse function is more complicated than just solving an equation,
 and many algebraic simplification rules are not universally valid.

 The good news is that these problems are {\sl theoretically} capable
 of being solved, and are {\sl practically} close to being solved, but
 not yet solved, in several realworld examples. However, there is
 still a long way to go before implementations match the theoretical
 possibilities.",
 paper = "Davenp12.pdf"

\end{chunk}
\index{Davenport, James}
\begin{chunk}{axiom.bib}
@@ 11494,18 +11567,21 @@ England, Matthew; Wilson, David
\end{chunk}
\index{Dunstan, Martin}
\begin{chunk}{ignore}
\bibitem[Dunstan 00a]{Dun00a} Dunstan, Martin N.
+\begin{chunk}{axiom.bib}
+@misc{Duns00,
+ author = "Dunstan, Martin N.",
title = {{Adding Larch/Aldor Specifications to Aldor}},
 abstract = "
 We describe a proposal to add Larchstyle annotations to the Aldor
+ abstract =
+ "We describe a proposal to add Larchstyle annotations to the Aldor
programming language, based on our PhD research. The annotations
are intended to be machinecheckable and may be used for a variety
of purposes ranging from compiler optimizations to verification
condition (VC) generation. In this report we highlight the options
available and describe the changes which would need to be made to
the compiler to make use of this technology.",
 paper = "Dunxx.pdf"
+ paper = "Duns00.pdf",
+ keywords = "axiomref"
+}
\end{chunk}
@@ 11592,6 +11668,35 @@ England, Matthew; Wilson, David
\index{Guttman, Joshua D.}
\index{Thayer, Javier}
\begin{chunk}{axiom.bib}
+@article{Farm93a,
+ author = "Farmer, William M. and Guttman, Joshua D. and Thayer, Javier",
+ title = {{IMPS: An Interactive Mathematical Proof Systems}},
+ journal = "J. of Automated Reasoning",
+ volume = "11",
+ pages = "213248",
+ year = "1993",
+ abstract =
+ "IMPS is an interactive mathematical proof system intended as a
+ generalpurpose too! formulating and applying mathematics in a
+ familiar fashion. The logic of IMPS is based on a version of simple
+ type theory with partial functions and subtypes. Mathematical
+ specification and inference are performed relative to axiomatic
+ theories, which can be related to one another via inclusion and theory
+ interpretation. IMPS provides relatively large primitive inference
+ steps to facilitate human control of the deductive process and human
+ comprehension of the resulting proofs. An initial theory library con
+ taining over a thousand repeatable proofs covers significant portions
+ of logic, algebra, and analysis and provides some support for modeling
+ applications in computer science.",
+ paper = "Farm93a.pdf"
+}
+
+\end{chunk}
+
+\index{Farmer, William M.}
+\index{Guttman, Joshua D.}
+\index{Thayer, Javier}
+\begin{chunk}{axiom.bib}
@article{Farm93,
author = "Farmer, William M. and Guttman, Joshua D. and Thayer, Javier",
title = {{Reasoning with contexts}},
@@ 11677,6 +11782,18 @@ England, Matthew; Wilson, David
\end{chunk}
+\index{Fitting, M.}
+\begin{chunk}{axiom.bib}
+@book{Fitt90,
+ author = "Fitting, M.",
+ title = {{Firstorder Logic and Automated Theorem Proving}},
+ publisher = "SpringerVerlag",
+ year = "1990",
+ isbn = "9781461275152"
+}
+
+\end{chunk}
+
\index{Frade, Maria Joao}
\begin{chunk}{axiom.bib}
@article{Frad08,
@@ 11746,6 +11863,19 @@ England, Matthew; Wilson, David
\subsection{G} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Gallier, Jean H.}
+\begin{chunk}{axiom.bib}
+@book{Gall86,
+ author = "Gallier, Jean H.",
+ title = {{Logic for Computer Science: Foundations of Automatic
+ Theorem Proving}},
+ publisher = "Harper and Row",
+ year = "1986",
+ isbn = "9780486780825"
+}
+
+\end{chunk}
+
\index{Geddes, D.}
\begin{chunk}{axiom.bib}
@book{Gedd94,
@@ 12079,7 +12209,7 @@ England, Matthew; Wilson, David
\begin{chunk}{axiom.bib}
@book{Gutt93,
author = "Guttag, John V. and Horning, James J.",
 title = {{LARCH: Languages and TOols for Formal Specifications}},
+ title = {{LARCH: Languages and Tools for Formal Specifications}},
publisher = "SpringerVerlag",
year = "1993",
isbn = "3540940065"
@@ 12367,17 +12497,16 @@ England, Matthew; Wilson, David
}
\end{chunk}

\index{Homann, Karsten}
\begin{chunk}{axiom.bib}
@phdthesis{Homa96,
+@phdthesis{Homa96a,
author = "Homann, Karsten",
title = {{Symbolisches L\"osen mathematischer Probleme durch
Kooperation algorithmischer und logischer Systeme}},
year = "1996",
school = {Universit\"at Karlsruhe},
 paper = "Homa96.pdf"
+ paper = "Homa96a.pdf"
}
\end{chunk}
@@ 13097,6 +13226,35 @@ England, Matthew; Wilson, David
\end{chunk}
+\index{Lee, Wonyeol}
+\index{Sharma, Rahul}
+\index{Aiken, Alex}
+\begin{chunk}{axiom.bib}
+@article{Wony18,
+ author = "Lee, Wonyeol and Sharma, Rahul and Aiken, Alex",
+ title = {{On Automatically Proving the Correctness of math.h
+ Implementation}},
+ journal = "Proc. ACM Programming Languages",
+ volume = "2",
+ number = "42",
+ year = "2018",
+ pages = "132",
+ abstract =
+ "Industry standard implementations of math.h claim (often without
+ formal proof) tight bounds on floating point errors. We demonstrate a
+ novel static analysis that proves these bounds and verifies the
+ correctness of these implementations. Our key insight is a reduction
+ of this verification task to a set of mathematical optimization
+ problems that can be solved by offtheshelf computer algebra
+ systems. We use this analysis to prove the correctness of
+ implementations in Intel’s math library automatically. Prior to this
+ work, these implementations could only be verified with significant
+ manual effort.",
+ paper = "Wony18.pdf"
+}
+
+\end{chunk}
+
\index{London, Ralph L.}
\index{Musser, David R.}
\begin{chunk}{axiom.bib}
@@ 13516,6 +13674,19 @@ England, Matthew; Wilson, David
\index{Meshveliani, Sergei D.}
\begin{chunk}{axiom.bib}
+@misc{Mesh05,
+ author = "Meshveliani, Sergei D.",
+ title = {{Term rewriting, Equationional Reasoning, Automatic proofs}},
+ link = "\url{ftp://ftp.botik.ru/pub/local/Mechveliani/dumatel/1.02/}",
+ year = "2005",
+ paper = "Mesh05.pdf"
+}
+
+\end{chunk}
+
+
+\index{Meshveliani, Sergei D.}
+\begin{chunk}{axiom.bib}
@misc{Mesh13,
author = "Meshveliani, Sergei D.",
title = {{Dependent Types for an Adequate Programming of Algebra}},
@@ 13881,13 +14052,14 @@ England, Matthew; Wilson, David
\index{Munteanu, Bogdan}
\index{Brooker, Marc}
\index{Deardeuff, Michael}
\begin{chunk}{ignore}
\bibitem[Newcombe 13]{Newc13} Newcombe, Chris; Rath, Tim; Zhang, Fan;
Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
+\begin{chunk}{axiom.bib}
+@misc{Newc13,
+ author = "Newcombe, Chris and Rath, Tim and Zhang, Fan and
+ Munteanu, Bogdan and Brooker, Marc and Deardeuff, Michael",
title = {{Use of Formal Methods at Amazon Web Services}},
link = "\url{http://research.microsoft.com/enus/um/people/lamport/tla/formalmethodsamazon.pdf}",
 abstract = "
 In order to find subtle bugs in a system design, it is necessary to
+ abstract =
+ "In order to find subtle bugs in a system design, it is necessary to
have a precise description of that design. There are at least two
major benefits to writing a precise design; the author is forced to
think more clearly, which helps eliminate ``plausible handwaving'',
@@ 13908,6 +14080,7 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
avoiding esoteric concepts. We also very much wanted an existing
ecosystem of tools. We found what we were looking for in TLA+, a
formal specification language."
+}
\end{chunk}
@@ 13999,7 +14172,7 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\subsection{O} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{O'Connor, Liam}
\begin{chunk}{ignore}
+\begin{chunk}{axiom.bib}
@misc{OCon15,
author = {O'Connor, Liam},
title = {{Write Your Compiler by Proving It Correct}},
@@ 14020,7 +14193,8 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
for a language of arithmetic expressions and variables to an idealised
assembly language for a virtual stack machine, and explain some of the
useful features that dependent types give us for writing verified
 compilers."}
+ compilers."
+}
\end{chunk}
@@ 14429,7 +14603,8 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
title = {{Adding the axioms to Axiom. Toward a system of automated
reasoning in Aldor}},
year = "1998",
 link = "\url{http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.1457}",
+ link =
+ "\url{http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.1457}",
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
@@ 14684,6 +14859,38 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\subsection{S} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Sacks, Elisha}
+\begin{chunk}{axiom.bib}
+@techreport{Sack87,
+ author = "Sacks, Elisha",
+ title = {{Hierarchical Reasoning about Inequalities}},
+ institution = "MIT",
+ year = "1987",
+ abstract =
+ "This paper describes a program called BOUNDER that proves
+ inequalities between functions over finite sets of constraints.
+ Previous inequality algorithms perform well on some subset of the
+ elementary functions, but poorly elsewhere. To overcome this problem,
+ BOUNDER maintains a hierarchy of increasingly complex algorithms.
+ When one fails to resolve an inequality, it tries the next. This
+ strategy resolves more inequalities than any single algorithm. It
+ also performs well on hard problems without wasting time on easy
+ ones. The current hierarchy consists of four algorithms: bounds
+ propagation, substitution, derivative inspection, and iterative
+ approximation. Propagation is an extension of interval arithmetic
+ that takes linear time, but ignores constraints between variables
+ and multiple occurrences of variables. The remaining algorithms
+ consider these factors, but require exponential time. Substitution
+ is a new, provably correct, algorithm for utilizing constraints
+ between variables. The final two algorithms analyze constraints
+ between variables. Inspection examines the signs of partial
+ derivatives. Iteration is based on several earlier algorithms
+ from interval arithmetic.",
+ paper = "Sack87.pdf"
+}
+
+\end{chunk}
+
\index{Schwarzweller, Christoph}
\begin{chunk}{axiom.bib}
@phdthesis{Schw97,
@@ 14906,6 +15113,24 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\end{chunk}
+\index{Th\'ery, Laurent}
+\begin{chunk}{axiom.bib}
+@article{Ther98,
+ author = "Thery, Laurent",
+ title = {{A Certified Version of Buchberger's Algorithm}},
+ journal = "LNCS",
+ volume = "1421",
+ pages = "349364",
+ year = "1998",
+ abstract =
+ "We present a proof of Buchberger's algorithm that has been developed
+ in the Coq proof assistant. The formulation of the algorithm in Coq
+ can be efficiently compiled and used to do computation",
+ paper = "Ther98.pdf"
+}
+
+\end{chunk}
+
\index{Traytel, Dmitriy}
\index{Berghofer, Stefan}
\index{Nipkow, Tobias}
@@ 15260,18 +15485,22 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\end{chunk}
\index{Briggs, Keith}
\begin{chunk}{ignore}
\bibitem[Briggs 04]{Bri04} Briggs, Keith
+\begin{chunk}{axiom.bib}
+@misc{Brig04,
+ author = "Briggs, Keith",
title = {{Exact real arithmetic}},
link = "\url{http://keithbriggs.info/documents/xrkenttalkpp.pdf}",
+ year = "2004",
paper = "Bri04.pdf"
+}
\end{chunk}
\index{Fateman, Richard J.}
\index{Yan, Tak W.}
\begin{chunk}{ignore}
\bibitem[Fateman 94]{Fat94} Fateman, Richard J.; Yan, Tak W.
+\begin{chunk}{axiom.bib}
+@misc{Fate94a,
+ author = "Fateman, Richard J.; Yan, Tak W.",
title ={{Computation with the Extended Rational Numbers and an
Application to Interval Arithmetic}},
link = "\url{http://www.cs.berkeley.edu/~fateman/papers/extrat.pdf}",
@@ 15284,7 +15513,8 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
rational number system to include infinity and ``notanumber'' may be
useful, especially to support robust interval computation. We describe
techniques for implementing these changes.",
 paper = "Fat94.pdf"
+ paper = "Fate94a.pdf"
+}
\end{chunk}
@@ 15362,10 +15592,12 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\index{Atkinson, Kendall}
\index{Han, Welmin}
\index{Stewear, David}
\begin{chunk}{ignore}
\bibitem[Atkinson 09]{Atk09} Atkinson, Kendall; Han, Welmin; Stewear, David
+\begin{chunk}{axiom.bib}
+@misc{Atki09,
+ author = "Atkinson, Kendall and Han, Welmin and Stewear, David",
title = {{Numerical Solution of Ordinary Differential Equations}},
 link = "\url{http://homepage.math.uiowa.edu/~atkinson/papers/NAODE_Book.pdf}",
+ link =
+ "\url{http://homepage.math.uiowa.edu/~atkinson/papers/NAODE_Book.pdf}",
abstract = "
This book is an expanded version of supplementary notes that we used
for a course on ordinary differential equations for upperdivision
@@ 15380,7 +15612,8 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
solved. For example, the criteria for the stability of a numerical
method is closely connected to the stability of the differential
equation problem being solved.",
 paper = "Atk09.pdf"
+ paper = "Atki09.pdf"
+}
\end{chunk}
@@ 15897,6 +16130,17 @@ Petkovsek, Marko
\end{chunk}
\index{Bronstein, Manuel}
+\begin{chunk}{axiom.bib}
+@misc{Bron02a,
+ author = "Bronstein, Manuel",
+ title = {{$\Sigma^{it}$ User Guide and Reference Manual}},
+ year = "2002",
+ paper = "Bron02a.pdf"
+}
+
+\end{chunk}
+
+\index{Bronstein, Manuel}
\index{Li, Ziming}
\index{Wu, Min}
\begin{chunk}{ignore}
@@ 19846,6 +20090,7 @@ Proc ISSAC 97 pp172175 (1997)
with branch cuts etc}},
journal = "14th Int. Symp. on Symbolic and Numeric Algorithms for
Scientific Computing",
+ link = "\url{http://arxiv.org/pdf/1212.5417.pdf}",
year = "2012",
series = "SYNASC'12",
pages = "8388",
@@ 32777,6 +33022,7 @@ Grant citation GR/L48256 Nov 1, 1997Feb 28, 2001
The problem of implicitization is an active topic where research is
still taking place. Examples of further research points are included
in the conclusion",
+ paper = "ElAl01.pdf",
keywords = "axiomref"
}
@@ 34997,6 +35243,15 @@ April 1976 (private copy)
number = "3",
pages = "2528",
year = "1979",
+ abstract =
+ "When I was first asked to give this banquet talk, I was somewhat
+ hesitant to accept. I have not been very heavily involved in the field
+ of symbolic and algebraic manipulation for the past three years. I
+ have contented myself with such behindthescenes activities as
+ serving as an associate editor for the ACM Transactions on
+ Mathematical Software and as a member of the SIGSAM Nominating
+ Committees two years ago and again this year.",
+ paper = "Grie79.pdf",
keywwords = "axiomref"
}
@@ 37370,12 +37625,15 @@ SIGSAM Communications in Computer Algebra, 157 2006
\end{chunk}
\index{Kelsey, Tom}
\begin{chunk}{ignore}
\bibitem[Kelsey 99]{Kel99} Kelsey, Tom
+\begin{chunk}{axiom.bib}
+@phdthesis{Kels99,
+ author = "Kelsey, Tom",
title = {{Formal Methods and Computer Algebra: A Larch Specification of
AXIOM Categories and Functors}},
Ph.D. Thesis, University of St Andrews, 1999
+ school = "University of St Andrews",
+ year = "1999",
keywords = "axiomref"
+}
\end{chunk}
@@ 37502,6 +37760,24 @@ Ph.D. Thesis, University of St Andrews, 1999
\end{chunk}
+\index{Kennedy, A.D.}
+\begin{chunk}{axiom.bib}
+@misc{Kenn01,
+ author = "Kennedy, A.D.",
+ title = {{Semantics of Categories in Aldor}},
+ year = "2001",
+ abstract =
+ "We consider some questions about the semantics of Aldor regarding the
+ way that types can be considered on an equal footing with any other
+ objects in the language. After a digression into the relationship
+ between Aldor categories and mathematical categories, we shall discuss
+ the more practical issue of the limitations of the {\tt define}
+ keyword and what the compiler should do about them.",
+ paper = "Kenn01.pdf"
+}
+
+\end{chunk}
+
\index{Kerber, Manfred}
\index{Kohlhase, Michael}
\index{Volker, Sorge}
@@ 42043,7 +42319,7 @@ Kognitive Systeme, Universit\"t Karlsruhe 1992
\begin{chunk}{axiom.bib}
@article{Seil94b,
author = "Seiler, Werner Markus",
 title = {{Pseudo differential operators and integrable systems in AXIOM}},
+ title = {{Pseudo Differential Operators and Integrable Systems in AXIOM}},
journal = "Computer Physics Communications",
volume = "79",
number = "2",
@@ 43381,7 +43657,7 @@ IBM Manual, March 1988
\subsection{T} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Thompson, Simon}
\begin{chunk}{ignore}
+\begin{chunk}{axiom.bib}
@InProceedings{Thom01,
author = "Thompson, Simon",
title = {{Logic and dependent types in the Aldor Computer Algebra System}},
@@ 43390,7 +43666,8 @@ IBM Manual, March 1988
year = "2001",
location = "St. Andrews, Scotland",
pages = "205233",
 link = "\url{http://axiomwiki.newsynthesis.org/public/refs/aldorcalc2000.pdf}",
+ link =
+ "\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'
@@ 43437,7 +43714,8 @@ IBM Manual, March 1988
title = {{Etude du typage dans le syst\`eme de calcul scientifique Aldor}},
comment = "Study of types in the Aldor scientific computation system",
year = "1998",
 link = "\url{http://axiomwiki.newsynthesis.org/public/refs/AldorT1998_04.pdf}",
+ link =
+ "\url{http://axiomwiki.newsynthesis.org/public/refs/AldorT1998_04.pdf}",
paper = "Tour98.pdf",
keywords = "axiomref"
}
@@ 44339,12 +44617,14 @@ IBM Research Division Technical Report RC19530 May 1994
\index{Iglio, Pietro}
\index{Morrison, Scott C.}
\index{Steinbach, Jonathan M.}
\begin{chunk}{ignore}
\bibitem[Watt 01]{Wat01} Watt, Stephen M.; Broadbery, Peter A.; Iglio, Pietro;
Morrison, Scott C.; Steinbach, Jonathan M.
+\begin{chunk}{axiom.bib}
+@misc{Watt01,
+ author = "Watt, Stephen M. and Broadbery, Peter A. and Iglio, Pietro and
+ Morrison, Scott C. and Steinbach, Jonathan M",
title = {{FOAM: A First Order Abstract Machine Version 0.35}},
IBM T. J. Watson Research Center (2001)
 paper = "Wat01.pdf"
+ year = "2001",
+ paper = "Watt01.pdf"
+}
\end{chunk}
@@ 44587,7 +44867,7 @@ IBM T. J. Watson Research Center (2001)
\index{Weber, Andreas}
\begin{chunk}{axiom.bib}
@InProceedings{Webe94,
+@Inproceedings{Webe94,
author = "Weber, Andreas",
title = {{Algorithms for Type Inference with Coercions}},
booktitle = "Proc ISSAC 94",
@@ 46671,6 +46951,33 @@ Lecture Notes in Computer Science. 76 (1979) SpringerVerlag
\end{chunk}
+\index{Church, Alonzo}
+\begin{chunk}{axiom.bib}
+@article{Chur40,
+ author = "Church, Alonzo",
+ title = {{A Formulation of the Simple Theory of Types}},
+ journal = "J. of Symbolic Logic",
+ volume = "5",
+ number = "2",
+ year = "1940",
+ pages = "5668",
+ abstract =
+ "The purpose of the present paper is to give a formulation of the
+ simple theory of types which incorporates certain features of the
+ calculus of $\lambda$conversion. A complete incorporation of the
+ calculus of $\lambda$conversion into the theory of types is
+ impossible if we require that $\lambda x$ and juxtaposition shall
+ retain their respective meanings as an abstraction operator and as
+ denoting the application of function to argument. But the present
+ partial incorporation has certain advantages from the point of view of
+ type theory and is offered as being of interest on this basis
+ (whatever may be thought of the finally satisfactory character of the
+ theory of types as a foundation for logic and mathematics).",
+ paper = "Chur40.pdf"
+}
+
+\end{chunk}
+
\index{Clarke, Edmund}
\index{Zhao, Xudong}
\begin{chunk}{axiom.bib}
@@ 46937,6 +47244,31 @@ J. Inst. Math. Appl. 21 135143. (1978)
\end{chunk}
+\index{Cunningham, R.J.}
+\index{Dick, A.J.J}
+\begin{chunk}{axiom.bib}
+@article{Cunn85,
+ author = "Cunningham, R.J. and Dick, A.J.J",
+ title = {{Rewrite Systems on a Lattice of Types}},
+ journal = "Acta Informatica",
+ volume = "22",
+ pages = "149169",
+ year = "1985",
+ abstract =
+ "Rewriting systems for partial algebras are developed by modifying
+ the KnuthBendix completion algorithm to permit the use of
+ latticestructured domains. Some problems with the original algorithm,
+ such as the treatment of division rings, are overcome conveniently by
+ this means. The use of a type lattice also gives a natural framework
+ for specifying data types in Computer Science without overspecifying
+ error situations. The soundness and meaning of the major concepts
+ involed in rewriting systems are reviewed when applied to such
+ structures.",
+ paper = "Cunn85.pdf"
+}
+
+\end{chunk}
+
\index{Curtis, A. R.}
\index{Powell, M. J. D.}
\index{Reid, J. K.}
@@ 47508,6 +47840,18 @@ A.E.R.E. Report R.8730. HMSO. (1977)
\subsection{E} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Engelman, C.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Enge65,
+ author = "Engelman, C.",
+ title = {{A Program for OnLine Assistance in Symbolic Computation}},
+ booktitle = "Proc. Fall Joint Comput. Conf. 2",
+ year = "1965",
+ publisher = "Spartan Books"
+}
+
+\end{chunk}
+
\subsection{F} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Fateman, Richard J.}
@@ 48151,6 +48495,31 @@ Grove, IL, USA and Oxford, UK, 1992
\end{chunk}
+\index{Guessarian, Irene}
+\index{Meseguer, Jose}
+\begin{chunk}{axiom.bib}
+@article{Gues87,
+ author = "Guessarian, Irene and Meseguer, Jose",
+ title = {{On the Axiomatization of ``IFTHENELSE''}},
+ journal = "SIAM J. Comput.",
+ volume = "16",
+ numbrrer = "2",
+ year = "1987",
+ pages = "332357",
+ abstract =
+ "The equationally complete proof system for ``ifthenelse'' of Bloom
+ and Tindell is extended to a complete proof system for manyosrted
+ algebras with extra operations, predicates and equations among
+ those. We give similar completeness results for continuous algebras
+ and program schemes (infinite trees) by the methods of algebraic
+ semantics. These extensions provide a purely equational proof system
+ to prove properties of functional programs over userdefinable data
+ types.",
+ paper = "Gues87.pdf"
+}
+
+\end{chunk}
+
\subsection{H} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{GeneralPackageForAlgebraicFunctionField}
@@ 48417,7 +48786,7 @@ Lecture Notes in Economics and Mathematical Systems. 187 SpringerVerlag. 1981
\index{Homann, Karsten}
\index{Calmet, Jacques}
\begin{chunk}{axiom.bib}
@article{Hom965,
+@article{Homa96,
author = "Homann, Karsten and Calmet, Jacques",
title = {{Structures for Symbolic Mathematical Reasoning and Computation}},
journal = "LNCS",
@@ 50134,6 +50503,31 @@ Science of Computer Programming V25 No.1 Oct 1995 pp4161 Elesevier
\end{chunk}
+\index{Paulson, Lawrence C.}
+\begin{chunk}{axiom.bib}
+@article{Paul90,
+ author = "Paulson, Lawrence C.",
+ title = {{A Formulation of the Simple Theory of Types (for
+ Isabelle}}},
+ journal = "LNCS",
+ volume = "417",
+ pages = "246274",
+ year = "1990",
+ abstract =
+ "Simple type theory is formulated for use with the generic theorem
+ prover Isabelle. This requires explicit type inference rules. There
+ are function, product, and subset types, which may be
+ empty. Descriptions (the etaoperator) introduce the Axiom of
+ Choice. Higherorder logic is obtained through reflection between
+ formulae and terms of type bool. Recursive types and functions can be
+ formally constructed. Isabelle proof procedures are described. The
+ logic appears suitable for general mathematics as well as
+ computational problems.",
+ paper = "Paul90.pdf"
+}
+
+\end{chunk}
+
\index{DoubleFloatSpecialFunctions}
\index{Pearcey, T.}
\begin{chunk}{axiom.bib}
@@ 50529,6 +50923,17 @@ ORSUM August 2003
\end{chunk}
+\index{Redfern, D.}
+\begin{chunk}{axiom.bib}
+@book{Redf98,
+ author = "Redfern, D.",
+ title = {{The Maple Handbook: Maple V Release 5}},
+ publisher = "Springer",
+ year = "1998"
+}
+
+\end{chunk}
+
\index{Redfield, J. Howard}
\begin{chunk}{axiom.bib}
@article{Redf27,
@@ 50741,6 +51146,30 @@ April 2007
\end{chunk}
+\index{Rump, Siegfried M.}
+\begin{chunk}{axiom.bib}
+@article{Rump88,
+ author = "Rump, Siegfried M.",
+ title = {{Algebraic Computation, Numerical Computation and Verified
+ Inclusions}},
+ journal = "LNCS",
+ volume = "296",
+ pages = "177197",
+ year = "1988",
+ abstract =
+ "The three different types of computation  the algebraic
+ manipulation, the numerical computation and the computation of
+ verified results  are aiming on different problems and deliver
+ qualitatively different results, each method having its specific
+ advantages for specific classes of problems. The following remarks
+ give some thoughts on possible combinations of all three methods to
+ obtain algorithms benefitting from the specific strength of either
+ method.",
+ paper = "Rump88.pdf"
+}
+
+\end{chunk}
+
\index{Rutishauser, H.}
\begin{chunk}{ignore}
\bibitem[Rutishauser 69]{Rut69} Rutishauser H.
@@ 51046,6 +51475,19 @@ The University of Chicago Press. 1974
\index{Sorge, Volker}
\begin{chunk}{axiom.bib}
+@misc{Sorg96,
+ author = "Sorge, Volker",
+ title = {{Integration eines Computeralgebrasystems in eine logische
+ Beweisumgebung }},
+ school = "Univ. des Saarlandes",
+ year = "1996",
+ comment = "Master's thesis"
+}
+
+\end{chunk}
+
+\index{Sorge, Volker}
+\begin{chunk}{axiom.bib}
@article{Sorg00,
author = "Sorge, Volker",
title = {{Nontrivial Symbolic Computations in Proof Planning}},
@@ 51129,19 +51571,20 @@ PrenticeHall 1971
\end{chunk}
\index{Suppes, Patrick}
\index{Takahashi, Shuzo}
+\index{Suppes, P.}
+\index{Takahashi, S.}
\begin{chunk}{axiom.bib}
@article{Supp89,
 author = "Suppes, Patrick and Takahashi, Shuzo",
 title = {{An Interactive Calculus TheoremProver for Continuity Properties}},
+ author = "Suppes, P. and Takahashi, S.",
+ title = {{An Interactive Calculus Theoremprover for Continuity
+ Properites}},
journal = "J. Symbolic Computation",
volume = "7",
number = "6",
 pages = "573590",
year = "1989",
+ pages = "573590",
abstract =
 "The work reported concerns the development of an interactive
+ "he work reported concerns the development of an interactive
theoremprover for the foundationsof the differential and integral
calculus. The main tools are a resolution theoremprover VERIFY,
previously developed for interactive proofs in set theory, and the
diff git a/changelog b/changelog
index 1d9bfe7..382520f 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20171109 tpd src/axiomwebsite/patches.html 20171109.01.tpd.patch
+20171109 tpd books/bookvolbib add references
20171031 tpd src/axiomwebsite/patches.html 20171031.03.tpd.patch
20171031 tpd books/bookvolbib add references
20171031 tpd src/axiomwebsite/patches.html 20171031.02.tpd.patch
diff git a/patch b/patch
index be340d0..b3912fb 100644
 a/patch
+++ b/patch
@@ 1,153 +1,692 @@
books/bookvolbib add references
Goal: Axiom Literate Programming
+Goal: Proving Axiom Correct
\index{Jenks, Richard D.}
+\index{Meshveliani, Sergei D.}
\begin{chunk}{axiom.bib}
@article{Jenk87a,
 author = "Jenks, Richard D.",
 title = {{19621992: The First 30 Years of Symbolic Mathematical
 Programming Systems}},
 journal = "Lecture Notes in Computer Science",
+@misc{Mesh05,
+ author = "Meshveliani, Sergei D.",
+ title = {{Term rewriting, Equationional Reasoning, Automatic proofs}},
+ link = "\url{ftp://ftp.botik.ru/pub/local/Mechveliani/dumatel/1.02/}",
+ year = "2005",
+ paper = "Mesh05.pdf"
+}
+
+\end{chunk}
+
+\index{Davenport, James H.}
+\begin{chunk}{axiom.bib}
+@misc{Dave98,
+ author = "Davenport, James H.",
+ title = {{Is Computer Algebra the same as Computer Mathematics?}},
+ year = "1998",
+ comment = "Talk for British Colloquium for Theoretical Computer Science"
+}
+
+\end{chunk}
+
+\index{Th\'ery, Laurent}
+\begin{chunk}{axiom.bib}
+@article{Ther98,
+ author = "Thery, Laurent",
+ title = {{A Certified Version of Buchberger's Algorithm}},
+ journal = "LNCS",
+ volume = "1421",
+ pages = "349364",
+ year = "1998",
+ abstract =
+ "We present a proof of Buchberger's algorithm that has been developed
+ in the Coq proof assistant. The formulation of the algorithm in Coq
+ can be efficiently compiled and used to do computation",
+ paper = "Ther98.pdf"
+}
+
+\end{chunk}
+
+\index{Cooley, James W.}
+\index{Tukey, John W.}
+\begin{chunk}{axiom.bib}
+@article{Cool65,
+ author = "Cooley, James W. and Tukey, John W.",
+ title = {{An Algorithm for the Machine Calculation of Complex Fourier
+ Series}},
+ journal = "Mathematics of Computation",
+ volume = "19",
+ number = "04",
+ year = "1965"
+}
+
+\end{chunk}
+
+\index{Rump, Siegfried M.}
+\begin{chunk}{axiom.bib}
+@article{Rump88,
+ author = "Rump, Siegfried M.",
+ title = {{Algebraic Computation, Numerical Computation and Verified
+ Inclusions}},
+ journal = "LNCS",
volume = "296",
 year = "1987",
 pages = "11",
+ pages = "177197",
+ year = "1988",
abstract =
 "This talk examines the history and future of symbolic mathematical
 computer systems. This talk will trace the development of three
 generations of computer algebra systems as typified by an early system
 of 60's: FORMAC, the standalone systems of the 70's: REDUCE and
 MACSYMA, and those developed in the 80's: muMATH, MAPLE, SMP, with
 particular emphasis on Scratchpad II, a system of revolutionary design
 currently under development by IBM Research.

 This talk will trace the progress of algebraic algorithm research in
 the past 25 years, advances in hardware and software technology over
 the same period, and the impact of such progress on the design issues
 of such systems. The talk will conclude with a description of the
 workstation of the future and its anticipated impact on the research
 and educational communities.",
 paper = "Jenk87a.pdf",
 keywords = "axiomref"
+ "The three different types of computation  the algebraic
+ manipulation, the numerical computation and the computation of
+ verified results  are aiming on different problems and deliver
+ qualitatively different results, each method having its specific
+ advantages for specific classes of problems. The following remarks
+ give some thoughts on possible combinations of all three methods to
+ obtain algorithms benefitting from the specific strength of either
+ method.",
+ paper = "Rump88.pdf"
}
\end{chunk}
\index{Calmet, Jacques}
+\index{Engelman, C.}
\begin{chunk}{axiom.bib}
@article{Calm87,
 author = "Calmet, Jacques",
 title = {{Intelligent Computer Algebra System: Myth, Fancy or
 Reality?}},
 journal = "Lecture Notes in Computer Science",
 volume = "296",
 year = "1987",
 pages = "211",
 paper = "Calm87.pdf",
 keywords = "axiomref"
+@inproceedings{Enge65,
+ author = "Engelman, C.",
+ title = {{A Program for OnLine Assistance in Symbolic Computation}},
+ booktitle = "Proc. Fall Joint Comput. Conf. 2",
+ year = "1965",
+ publisher = "Spartan Books"
+}
+
+\end{chunk}
+
+\index{Church, Alonzo}
+\begin{chunk}{axiom.bib}
+@article{Chur40,
+ author = "Church, Alonzo",
+ title = {{A Formulation of the Simple Theory of Types}},
+ journal = "J. of Symbolic Logic",
+ volume = "5",
+ number = "2",
+ year = "1940",
+ pages = "5668",
+ abstract =
+ "The purpose of the present paper is to give a formulation of the
+ simple theory of types which incorporates certain features of the
+ calculus of $\lambda$conversion. A complete incorporation of the
+ calculus of $\lambda$conversion into the theory of types is
+ impossible if we require that $\lambda x$ and juxtaposition shall
+ retain their respective meanings as an abstraction operator and as
+ denoting the application of function to argument. But the present
+ partial incorporation has certain advantages from the point of view of
+ type theory and is offered as being of interest on this basis
+ (whatever may be thought of the finally satisfactory character of the
+ theory of types as a foundation for logic and mathematics).",
+ paper = "Chur40.pdf"
}
\end{chunk}
\index{Lescanne, Pierre}
+\index{Redfern, D.}
\begin{chunk}{axiom.bib}
@article{Lesc87,
 author = "Lescanne, Pierre",
 title = {{Current trends in rewriting techniques and related problems}},
 journal = "Lecture Notes in Computer Science",
 volume = "296",
 year = "1987",
 pages = "3851",
 paper = "Lesc97.pdf"
+@book{Redf98,
+ author = "Redfern, D.",
+ title = {{The Maple Handbook: Maple V Release 5}},
+ publisher = "Springer",
+ year = "1998"
}
\end{chunk}
\index{Abbott, J.A.}
\index{Bradford, R.J.}
\index{Davenport, J.H.}
+\index{Sorge, Volker}
\begin{chunk}{axiom.bib}
@article{Abbo87,
 author = "Abbott, J.A. and Bradford, R.J. and Davenport, J.H.",
 title = {{factorisation of Polynomials: Old Ideas and Recent
 Results}},
 journal = "Lecture Notes in Computer Science",
 volume = "296",
 year = "1987",
 pages = "8191",
+@misc{Sorg96,
+ author = "Sorge, Volker",
+ title = {{Integration eines Computeralgebrasystems in eine logische
+ Beweisumgebung }},
+ school = "Univ. des Saarlandes",
+ year = "1996",
+ comment = "Master's thesis"
+}
+
+\end{chunk}
+
+\index{Farmer, William M.}
+\index{Guttman, Joshua D.}
+\index{Thayer, Javier}
+\begin{chunk}{axiom.bib}
+@article{Farm93a,
+ author = "Farmer, William M. and Guttman, Joshua D. and Thayer, Javier",
+ title = {{IMPS: An Interactive Mathematical Proof Systems}},
+ journal = "J. of Automated Reasoning",
+ volume = "11",
+ pages = "213248",
+ year = "1993",
abstract =
 "The problem of factorising polynomials: that is to say, given a
 polynomial with integer coefficients, to find the irreducible
 polynomials that divide it, is one with a long history. While the last
 word has not been said on the subject, we can say that the past 15
 years have seen major breakthroughs, and many computer algebra
 systems now include {\sl efficient} algorithms for this problem. When
 it comes to polynomials with algebraic number coefficients, the
 problem is far harder, and several major questions remain to be
 answered. Nevertheless, the last few years have seen substantial
 improvements, and such factorisations are now possible",
 paper = "Abbo87.pdf"
+ "IMPS is an interactive mathematical proof system intended as a
+ generalpurpose too! formulating and applying mathematics in a
+ familiar fashion. The logic of IMPS is based on a version of simple
+ type theory with partial functions and subtypes. Mathematical
+ specification and inference are performed relative to axiomatic
+ theories, which can be related to one another via inclusion and theory
+ interpretation. IMPS provides relatively large primitive inference
+ steps to facilitate human control of the deductive process and human
+ comprehension of the resulting proofs. An initial theory library con
+ taining over a thousand repeatable proofs covers significant portions
+ of logic, algebra, and analysis and provides some support for modeling
+ applications in computer science.",
+ paper = "Farm93a.pdf"
}
\end{chunk}
\index{Buchberger, Bruno}
+\index{Bundy, Alan}
+\index{Wallen, Lincoln}
\begin{chunk}{axiom.bib}
@article{Buch87,
 author = "Buchberger, Bruno",
 title = {{AApplications of Gr\"obner Bases in NonLinear
 Computational Geometry}},
 journal = "Lecture Notes in Computer Science",
 volume = "296",
 year = "1987",
 paper = "5280",
+@inproceedings{Bund75,
+ author = "Bundy, Alan and Wallen, Lincoln",
+ title = {{The UT Theorem Prover}},
+ booktitle = "Catalogue of Artificial Intelligence Tools",
+ pages = "132133",
+ year = "1975",
abstract =
 "Groebner bases are certain finite sets of multivariate
 polynomials. Many problems in polynomial ideal theory (algebra
 geometry, nonlinear computational geometry) can be solved by easy
 algorithms after transforming the polynomial sets involved in the
 specification of the problems into Groebner basis form. In this paper
 we give gome examples of applying the Groebner bases method to
 problems in nonlinear computational geometry (inverse kinematics in
 robot programming, collision detection for superellipsoids,
 implicitization of parametric representations of curves and surfaces,
 inversion problem for parametric representations, automated
 geometrical theorem proving, primary decompsotion of implicitly
 defined geometrical objects). The paper starts with a brief summary of
 the Groebner bases method.",
 paper = "Buch87.pdf"
}

\end{chunk}

\index{Andrews, George}
\begin{chunk}{axiom.bib}
@article{Andr87,
 author = "Andrews, George",
 title = {{Applications of Scratchpad to Problems in Special
 Functions and Combinatorics}},
 journal = "Lecture Notes in Computer Science",
 volume = "296",
+ "The UT theorem prover is probably the best known natural deduction
+ <153> theorem prover. It was written in LISP <34> by woody Bledsoe and
+ his coworkers at the University of Texas, and is best described in
+ (Bledsoe and Tyson 75]. The theorem prover embodies a Gentzenlike
+ deduction system for firstorder predicate calculus, and many special
+ purpose techniques, including: subgoaling, rewrite rules, controlled
+ lorward chaining, controlled definition instantiation, conditional
+ procedures, and induction. The prover, though powerful in its own
+ right, is essentially interactive and thus allows the user of the
+ prover to control the search for the proof in radical ways. The user
+ can for example : add hypotheses, instruct the prover to instantiate
+ certain variables with values, or instruct the prover as to which
+ deduction rule to use next."
+}
+
+\end{chunk}
+
+\index{Bledsoe, W.W.}
+\begin{chunk}{axiom.bib}
+@techreport{Bled83,
+ author = "Bledsoe, W.W.",
+ title = {{The UT Natural Deduction Prover}},
+ type = "technical report",
+ institution = "Univ. of Texas at Austin",
+ year = "1983",
+ number = "ATP17B"
+}
+
+\end{chunk}
+
+\index{Bledsoe, W.W.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Bled84,
+ author = "Bledsoe, W.W.",
+ title = {{Some Automatic Proofs in Analysis}},
+ booktitle = "Automated Theorem Proving: After 25 Years",
+ publisher = "American Mathematical Society",
+ year = "1984"
+}
+
+\end{chunk}
+
+\index{Bledsoe, W.W.}
+\index{Bruell, P.}
+\index{Shostak, R.}
+\begin{chunk}{axiom.bib}
+@techreport{Bled79,
+ author = "Bledsoe, W.W. and Bruell, P. and Shostak, R.",
+ title = {{A Prover for General Inequalities}},
+ type = "technical report",
+ institution = "Univ. of Texas at Austin",
+ year = "1979",
+ number = "ATP40A"
+}
+
+\end{chunk}
+
+\index{Fitting, M.}
+\begin{chunk}{axiom.bib}
+@book{Fitt90,
+ author = "Fitting, M.",
+ title = {{Firstorder Logic and Automated Theorem Proving}},
+ publisher = "SpringerVerlag",
+ year = "1990",
+ isbn = "9781461275152"
+}
+
+\end{chunk}
+
+\index{Gallier, Jean H.}
+\begin{chunk}{axiom.bib}
+@book{Gall86,
+ author = "Gallier, Jean H.",
+ title = {{Logic for Computer Science: Foundations of Automatic
+ Theorem Proving}},
+ publisher = "Harper and Row",
+ year = "1986",
+ isbn = "9780486780825"
+}
+
+\end{chunk}
+
+\index{Guessarian, Irene}
+\index{Meseguer, Jose}
+\begin{chunk}{axiom.bib}
+@article{Gues87,
+ author = "Guessarian, Irene and Meseguer, Jose",
+ title = {{On the Axiomatization of ``IFTHENELSE''}},
+ journal = "SIAM J. Comput.",
+ volume = "16",
+ numbrrer = "2",
year = "1987",
 pages = "158166",
+ pages = "332357",
+ abstract =
+ "The equationally complete proof system for ``ifthenelse'' of Bloom
+ and Tindell is extended to a complete proof system for manyosrted
+ algebras with extra operations, predicates and equations among
+ those. We give similar completeness results for continuous algebras
+ and program schemes (infinite trees) by the methods of algebraic
+ semantics. These extensions provide a purely equational proof system
+ to prove properties of functional programs over userdefinable data
+ types.",
+ paper = "Gues87.pdf"
+}
+
+\end{chunk}
+
+\index{Cunningham, R.J.}
+\index{Dick, A.J.J}
+\begin{chunk}{axiom.bib}
+@article{Cunn85,
+ author = "Cunningham, R.J. and Dick, A.J.J",
+ title = {{Rewrite Systems on a Lattice of Types}},
+ journal = "Acta Informatica",
+ volume = "22",
+ pages = "149169",
+ year = "1985",
+ abstract =
+ "Rewriting systems for partial algebras are developed by modifying
+ the KnuthBendix completion algorithm to permit the use of
+ latticestructured domains. Some problems with the original algorithm,
+ such as the treatment of division rings, are overcome conveniently by
+ this means. The use of a type lattice also gives a natural framework
+ for specifying data types in Computer Science without overspecifying
+ error situations. The soundness and meaning of the major concepts
+ involed in rewriting systems are reviewed when applied to such
+ structures.",
+ paper = "Cunn85.pdf"
+}
+
+\end{chunk}
+
+\index{Paulson, Lawrence C.}
+\begin{chunk}{axiom.bib}
+@article{Paul90,
+ author = "Paulson, Lawrence C.",
+ title = {{A Formulation of the Simple Theory of Types (for
+ Isabelle}}},
+ journal = "LNCS",
+ volume = "417",
+ pages = "246274",
+ year = "1990",
+ abstract =
+ "Simple type theory is formulated for use with the generic theorem
+ prover Isabelle. This requires explicit type inference rules. There
+ are function, product, and subset types, which may be
+ empty. Descriptions (the etaoperator) introduce the Axiom of
+ Choice. Higherorder logic is obtained through reflection between
+ formulae and terms of type bool. Recursive types and functions can be
+ formally constructed. Isabelle proof procedures are described. The
+ logic appears suitable for general mathematics as well as
+ computational problems.",
+ paper = "Paul90.pdf"
+}
+
+\end{chunk}
+
+\index{Kelsey, Tom}
+\begin{chunk}{axiom.bib}
+@phdthesis{Kels99,
+ author = "Kelsey, Tom",
+ title = {{Formal Methods and Computer Algebra: A Larch Specification of
+ AXIOM Categories and Functors}},
+ school = "University of St Andrews",
+ year = "1999",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
+\index{Lee, Wonyeol}
+\index{Sharma, Rahul}
+\index{Aiken, Alex}
+\begin{chunk}{axiom.bib}
+@article{Wony18,
+ author = "Lee, Wonyeol and Sharma, Rahul and Aiken, Alex",
+ title = {{On Automatically Proving the Correctness of math.h
+ Implementation}},
+ journal = "Proc. ACM Programming Languages",
+ volume = "2",
+ number = "42",
+ year = "2018",
+ pages = "132",
+ abstract =
+ "Industry standard implementations of math.h claim (often without
+ formal proof) tight bounds on floating point errors. We demonstrate a
+ novel static analysis that proves these bounds and verifies the
+ correctness of these implementations. Our key insight is a reduction
+ of this verification task to a set of mathematical optimization
+ problems that can be solved by offtheshelf computer algebra
+ systems. We use this analysis to prove the correctness of
+ implementations in Intel’s math library automatically. Prior to this
+ work, these implementations could only be verified with significant
+ manual effort.",
+ paper = "Wony18.pdf"
+}
+
+\end{chunk}
+
+\index{Daly, Timothy}
+\begin{chunk}{axiom.bib}
+@misc{Daly10,
+ author = "Daly, Timothy",
+ title = {{Intel Instruction Semantics Generator}},
+ link = "\url{http://daly.axiomdeveloper.org/TimothyDaly_files/publications/sei/intel/intel.pdf}",
+ abstract =
+ "Given an Intel x86 binary, extract the semantics of the instruction
+ stream as Conditional Concurrent Assignments (CCAs). These CCAs
+ represent the semantics of each individual instruction. They can be
+ composed to represent higher level semantics.",
+ paper = "Daly10.pdf"
+}
+
+\end{chunk}
+
+\index{Naylor, William A.}
+\begin{chunk}{axiom.bib}
+@phdthesis{Nayl00,
+ author = "Naylor, Bill",
+ title = {{Polynomial GCD Using Straight Line Program Representation}},
+ school = "University of Bath",
+ year = "2000",
+ link = "\url{http://www.sci.csd.uwo.ca/~bill/thesis.ps}",
+ abstract = "
+ This thesis is concerned with calculating polynomial greatest common
+ divisors using straight line program representation.
+
+ In the Introduction chapter, we introduce the problem and describe
+ some of the traditional representations for polynomials, we then talk
+ about some of the general subjects central to the thesis, terminating
+ with a synopsis of the category theory which is central to the Axiom
+ computer algebra system used during this research.
+
+ The second chapter is devoted to describing category theory. We follow
+ with a chapter detailing the important sections of computer code
+ written in order to investigate the straight line program subject.
+ The following chapter on evalution strategies and algorithms which are
+ dependant on these follows, the major algorith which is dependant on
+ evaluation and which is central to our theis being that of equality
+ checking. This is indeed central to many mathematical problems.
+ Interpolation, that is the determination of coefficients of a
+ polynomial is the subject of the next chapter. This is very important
+ for many straight line program algorithms, as their noncanonical
+ structure implies that it is relatively difficult to determine
+ coefficients, these being the basic objects that many algorithms work
+ on. We talk about three separate interpolation techniques and compare
+ their advantages and disadvantages. The final two chapters describe
+ some of the results we have obtained from this research and finally
+ conclusions we have drawn as to the viability of the straight line
+ program approach and possible extensions.
+
+ Finally we terminate with a number of appendices discussing side
+ subjects encountered during the thesis.",
+ paper = "Nayl00.pdf"
+}
+
+\end{chunk}
+
+\index{Shoup, Victor}
+\begin{chunk}{axiom.bib}
+@inproceedings{Shou93,
+ author = "Shoup, Victor",
+ title = {{Factoring Polynomials over Finite Fields:
+ Asymptotic Complexity vs Reality*}},
+ booktitle = "Proc. IMACS Symposium, Lille, France",
+ year = "1993",
+ link = "\url{http://www.shoup.net/papers/lille.pdf}",
+ abstract =
+ "This paper compares the algorithms by Berlekamp, Cantor and
+ Zassenhaus, and Gathen and Shoup to conclude that (a) if large
+ polynomials are factored the FFT should be used for polynomial
+ multiplication and division, (b) Gathen and Shoup should be used if
+ the number of irreducible factors of $f$ is small. (c) if nothing is
+ know about the degrees of the factors then Berlekamp's algorithm
+ should be used.",
+ paper = "Shou93.pdf"
+}
+
+\end{chunk}
+
+\index{Wang, Paul S.}
+\begin{chunk}{axiom.bib}
+@article{Wang78,
+ author = "Wang, Paul S.",
+ title = {{An Improved Multivariate Polynomial Factoring Algorithm}},
+ journal = "Mathematics of Computation",
+ volume = "32",
+ number = "144",
+ year = "1978",
+ pages = "12151231",
+ link = "\url{http://www.ams.org/journals/mcom/197832144/S00255718197805682843/S00255718197805682843.pdf}",
+ abstract = "
+ A new algorithm for factoring multivariate polynomials over the
+ integers based on an algorithm by Wang and Rothschild is described.
+ The new algorithm has improved strategies for dealing with the known
+ problems of the original algorithm, namely, the leading coefficient
+ problem, the badzero problem and the occurence of extraneous factors.
+ It has an algorithm for correctly predetermining leading coefficients
+ of the factors. A new and efficient padic algorith named EEZ is
+ described. Basically it is a linearly convergent variablebyvariable
+ parallel construction. The improved algorithm is generally faster and
+ requires less store than the original algorithm. Machine examples with
+ comparative timing are included.",
+ paper = "Wang78.pdf"
+}
+
+\end{chunk}
+
+\index{Baez, John C.}
+\index{Stay, Mike}
+\begin{chunk}{axiom.bib}
+@misc{Baez09,
+ author = "Baez, John C.; Stay, Mike",
+ title = {{Physics, Topology, Logic and Computation: A Rosetta Stone}},
+ link = "\url{http://arxiv.org/pdf/0903.0340v3.pdf}",
+ abstract = "
+ In physics, Feynman diagrams are used to reason about quantum
+ processes. In the 1980s, it became clear that underlying these
+ diagrams is a powerful analogy between quantum physics and
+ topology. Namely, a linear operator behaves very much like a
+ ``cobordism'': a manifold representing spacetime, going between two
+ manifolds representing space. But this was just the beginning: simiar
+ diagrams can be used to reason about logic, where they represent
+ proofs, and computation, where they represent programs. With the rise
+ of interest in quantum cryptography and quantum computation, it became
+ clear that there is an extensive network of analogies between physics,
+ topology, logic and computation. In this expository paper, we make
+ some of these analogies precise using the concept of ``closed
+ symmetric monodial category''. We assume no prior knowledge of
+ category theory, proof theory or computer science.",
+ paper = "Baez09.pdf"
+}
+
+\end{chunk}
+
+\index{Dunstan, Martin}
+\begin{chunk}{axiom.bib}
+@misc{Duns00,
+ author = "Dunstan, Martin N.",
+ title = {{Adding Larch/Aldor Specifications to Aldor}},
abstract =
 "Within the last few years, there have been numerous applications of
 computer algebra to special functions. G. Gasper (Norwestern
 University) has studied classical hypergeometric functions, and
 W. Gosper (Symbolics Inc.) has developed a large variety of
 spectacular transformation and summation techniques for MACSYMA. The
 purpose of this note is to explore some of the interface between
 computer algebra and special functions. In Section 2 we examine an
 application of MACSYMA which inadequately relied, in my opinion, on
 what was readily available in the literature on hypergeometric
 series. In Section 3 we consider classical observations on sums of
 powers of binomial coefficients. In Section 4 we consider a problem of
 D.M. Jackson wherein SCRATCHPAD and classical hypergeometric series
 interact nicely. We close with a problem inspired by work in
 statistical mechanics which leads us to questions about algorithms
 that would be useful in computer algebra applications.",
 paper = "Andr87.pdf",
 keywrods = "axiomref"
+ "We describe a proposal to add Larchstyle annotations to the Aldor
+ programming language, based on our PhD research. The annotations
+ are intended to be machinecheckable and may be used for a variety
+ of purposes ranging from compiler optimizations to verification
+ condition (VC) generation. In this report we highlight the options
+ available and describe the changes which would need to be made to
+ the compiler to make use of this technology.",
+ paper = "Duns00.pdf",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
+\index{Thompson, Simon}
+\begin{chunk}{axiom.bib}
+@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",
+ link =
+ "\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.",
+ paper = "Thom01.pdf",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
+\index{Newcombe, Chris}
+\index{Rath, Tim}
+\index{Zhang, Fan}
+\index{Munteanu, Bogdan}
+\index{Brooker, Marc}
+\index{Deardeuff, Michael}
+\begin{chunk}{axiom.bib}
+@misc{Newc13,
+ author = "Newcombe, Chris and Rath, Tim and Zhang, Fan and
+ Munteanu, Bogdan and Brooker, Marc and Deardeuff, Michael",
+ title = {{Use of Formal Methods at Amazon Web Services}},
+ link = "\url{http://research.microsoft.com/enus/um/people/lamport/tla/formalmethodsamazon.pdf}",
+ abstract =
+ "In order to find subtle bugs in a system design, it is necessary to
+ have a precise description of that design. There are at least two
+ major benefits to writing a precise design; the author is forced to
+ think more clearly, which helps eliminate ``plausible handwaving'',
+ and tools can be applied to check for errors in the design, even while
+ it is being written. In contrast, conventional design documents
+ consist of prose, static diagrams, and perhaps pseudocode in an ad
+ hoc untestable language. Such descriptions are far from precise; they
+ are often ambiguous, or omit critical aspects such as partial failure
+ or the granularity of concurrency (i.e. which constructs are assumed
+ to be atomic). At the other end of the spectrum, the final executable
+ code is unambiguous, but contains an overwhelming amount of detail. We
+ needed to be able to capture the essence of a design in a few hundred
+ lines of precise description. As our designs are unavoidably complex,
+ we need a highlyexpressive language, far above the level of code, but
+ with precise semantics. That expressivity must cover realworld
+ concurrency and faulttolerance. And, as we wish to build services
+ quickly, we wanted a language that is simple to learn and apply,
+ avoiding esoteric concepts. We also very much wanted an existing
+ ecosystem of tools. We found what we were looking for in TLA+, a
+ formal specification language."
+}
+
+\end{chunk}
+
+\index{O'Connor, Liam}
+\begin{chunk}{axiom.bib}
+@misc{OCon15,
+ author = {O'Connor, Liam},
+ title = {{Write Your Compiler by Proving It Correct}},
+ year = "2015",
+ link = "\url{http://liamoc.net/posts/20150823verifiedcompiler.html}",
+ abstract =
+ "Recently my research has been centered around the development of a
+ selfcertifying compiler for a functional language with linear types
+ called Cogent (see O'Connor et al. [2016]). The compiler works by
+ emitting, along with generated lowlevel code, a proof in Isabelle/HOL
+ (see Nipkow et al. [2002]) that the generated code is a refinement of
+ the original program, expressed via a simple functional semantics in HOL.
+
+ As dependent types unify for us the language of code and proof, my
+ current endeavour has been to explore how such a compiler would look
+ if it were implemented and verified in a dependently typed programming
+ language instead. In this post, I implement and verify a toy compiler
+ for a language of arithmetic expressions and variables to an idealised
+ assembly language for a virtual stack machine, and explain some of the
+ useful features that dependent types give us for writing verified
+ compilers."
+}
+
+\end{chunk}
+
+\index{Briggs, Keith}
+\begin{chunk}{axiom.bib}
+@misc{Brig04,
+ author = "Briggs, Keith",
+ title = {{Exact real arithmetic}},
+ link = "\url{http://keithbriggs.info/documents/xrkenttalkpp.pdf}",
+ year = "2004",
+ paper = "Bri04.pdf"
+}
+
+\end{chunk}
+
+\index{Fateman, Richard J.}
+\index{Yan, Tak W.}
+\begin{chunk}{axiom.bib}
+@misc{Fate94a,
+ author = "Fateman, Richard J.; Yan, Tak W.",
+ title ={{Computation with the Extended Rational Numbers and an
+ Application to Interval Arithmetic}},
+ link = "\url{http://www.cs.berkeley.edu/~fateman/papers/extrat.pdf}",
+ abstract = "
+ Programming languages such as Common Lisp, and virtually every
+ computer algebra system (CAS), support exact arbitraryprecision
+ integer arithmetic as well as exect rational number computation.
+ Several CAS include interval arithmetic directly, but not in the
+ extended form indicated here. We explain why changes to the usual
+ rational number system to include infinity and ``notanumber'' may be
+ useful, especially to support robust interval computation. We describe
+ techniques for implementing these changes.",
+ paper = "Fate94a.pdf"
+}
+
+\end{chunk}
+
+\index{Atkinson, Kendall}
+\index{Han, Welmin}
+\index{Stewear, David}
+\begin{chunk}{axiom.bib}
+@misc{Atki09,
+ author = "Atkinson, Kendall and Han, Welmin and Stewear, David",
+ title = {{Numerical Solution of Ordinary Differential Equations}},
+ link =
+ "\url{http://homepage.math.uiowa.edu/~atkinson/papers/NAODE_Book.pdf}",
+ abstract = "
+ This book is an expanded version of supplementary notes that we used
+ for a course on ordinary differential equations for upperdivision
+ undergraduate students and beginning graduate students in mathematics,
+ engineering, and sciences. The book introduces the numerical analysis
+ of differential equations, describing the mathematical background for
+ understanding numerical methods and giving information on what to
+ expect when using them. As a reason for studying numerical methods as
+ a part of a more general course on differential equations, many of the
+ basic ideas of the numerical analysis of differential equations are
+ tied closely to theoretical behavior associated with the problem being
+ solved. For example, the criteria for the stability of a numerical
+ method is closely connected to the stability of the differential
+ equation problem being solved.",
+ paper = "Atki09.pdf"
}
\end{chunk}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 0e5d62b..b24a432 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5851,7 +5851,9 @@ books/bookvol10.3 fix typo
20171031.02.tpd.patch
books/bookvolbib respect case in paper titles
20171031.03.tpd.patch
books/bookvolbib add references
p
+books/bookvolbib add references
+20171109.01.tpd.patch
+books/bookvolbib add references

1.9.1