From 5054cfd4facc585040967f77448221ab355fee7c Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Sun, 12 Aug 2018 03:35:48 0400
Subject: [PATCH] books/bookvolbib add references
MIMEVersion: 1.0
ContentType: text/plain; charset=UTF8
ContentTransferEncoding: 8bit
Goal: Proving Axiom Sane
\index{Scott, Dana S.}
\begin{chunk}{axiom.bib}
@article{Scot93,
author = "Scott, Dana S.",
title = {{A TypeTheoretical Alternative to ISWIM, CUCH, OWHY}},
journal = "Theoretical Computer Science",
volume = 121,
number = "12",
year = "1993",
pages = "411440",
abstract =
"The paper (first written in 1969 and circulated privately) concerns
the definition, axiomatization, and applications of the hereditarily
monotone and continuous functionals generated from the integers and
the Booleans (plus “undefined” elements). The system is formulated as
a typed system of combinators (or as a typed λcalculus) with a
recursion operator (the least fixedpoint operator), and its proof
rules are contrasted to a certain extent with those of the untyped
λcalculus. For publication (1993), a new preface has been added, and
many bibliographical references and comments in footnotes have been
appended.",
paper = "Scot93.pdf",
keywords = "printed"
}
\end{chunk}
\index{Winkler, Franz}
\begin{chunk}{axiom.bib}
@inproceedings{Wink85,
author = "Winkler, Franz",
title = {{Reducing the Complexity of the KnuthBendix Completion
Algorithm: A ``Unification'' of Different Approaches}},
booktitle = "European Conference on Computer Algebra (EUROCAL 85)",
pages = "378389",
publisher = "Springer",
year = "1985",
isbn = "9783540159834",
abstract =
"The KnuthBendix completion procedure for rewrite rule systems is
of wide applicability in symbolic and algebraic computation.
Attempts to reduce the complexity of this completion algorithm are
reported in the literature. Already in their seminal 1967 paper
D.E. Knuth and P.B. Bendix have suggested to keep all the rules
iterreduced during the execution of the algorithm. G. Huet has
presented a version of the completion algorithm in which every
rewrite rule is kept in reduced form with respect to all the other
rules in the system. Borrowing an idea of Buchberger's for the
completion of bases of polynomial ideals the author has proposed
in 1983 a criterion for detecting ``unnecessary'' critical
pairs. If a critical pair is recognized as unnecessary then one
need not apply the costly process of computing normal forms to
it. It has been unclear whether these approaches can be
combined. We demonstrate that it is possible to keep all the
rewrite rules interreduced and still use a criterion for
eliminating unnecessary critical pairs.",
paper = "Wink85.pdf",
keywords = "printed"
}
\end{chunk}
\index{KandriRody, Abdelilah}
\index{Kapur, Deepak}
\index{Winkler, Franz}
\begin{chunk}{axiom.bib}
@inproceedings{Kand89,
author = "KandriRody, Abdelilah and Kapur, Deepak and Winkler, Franz",
title = {{KnuthBendix Procedure and Buchberger Algorithm  A Synthesis}},
booktitle = "ISSAC'89",
publisher = "ACM Press",
pages = 5567",
year = "1989",
isbn = "0897913256",
abstract =
"The KnuthBendix procedure for the completion of a rewrite rule
system and the Buchberger algorithm for computing a Groebner basis
of a polynomial ideal are very similar in two respects: they both
start wtih an arbitrary specification of an algebraic structure
(axioms for an equational theory and a basis for a polynomial
ideal, respectively) which is transformed to a very special
specification of this algebraic structure (a complete rewrite rule
system and a Groebner basis of the polynomial ideal, respectively).
This special specification allows to decide many problems concerning
the given algebraic structure. Moreover, both algorithms achieve
their goals by employing the same basic concepts: formation of
critical pairs and completion.
Although the two methods are obviously related, the exact nature
of this relation remains to be clarified. Based on previous work
we show how the KnuthBendix procedure and the Buchberger algorithm
can be seen as special cases of a more general completion procedure.",
paper = "Kand89.pdf",
keywords = "printed"
}
\end{chunk}
\index{Winkler, Franz}
\begin{chunk}{axiom.bib}
@misc{Wink92,
author = "Winkler, Franz",
title = {{Computer Algebra}},
booktitle = "Encyclopedia of Physical Science and Technology",
volume = "4",
year = "1992",
publisher = "Academic Press",
paper = "Wink92.pdf",
keywords = "printed"
}
\end{chunk}
\index{Winkler, Franz}
begin{chunk}{axiom.bib}
@inproceedings{Wink95,
author = "Winkler, Franz",
title = {{Computer Algebra  Problems and Developments}},
booktitle = "Computers in Industry 2 (SCAFI'92)",
pages = "117",
year = "1995",
isbn = "9780471955290",
paper = "Wink95.pdf"
}
\end{chunk}
\index{Winkler, Franz}
\begin{chunk}{axiom.bib}
@techreport{Wink99,
author = "Winkler, Franz",
title = {{Advances and Problems in Algebraic Computation}},
type = "technical report",
number = "9949",
year = "1999",
institution = "RISC, Linz",
abstract =
"In the last years there has been dramatic progress in all areas
of algebraic computation. Many working mathematiians have access
to and actually use algebraic software systems for their research
No end of this development is in sight. We report on some active
topics in algebraic computation, namely the theory of integration
and symbolic solution of systems of differential equations, the
solution of systems of algebraic equations, the factorization of
polynomials, and the design and analysis of algebraic curves and
surfaces.",
paper = "Wink99.pdf",
keywords = "printed"
}
\end{chunk}
\index{Winkler, Franz}
\begin{chunk}{axiom.bib}
@inproceedings{Wink06,
author = "Winkler, Franz",
title = {{Computer Algebra and Geometry  Some Interactions}},
booktitle = "Proc. of Coll. on Constructive Algebra and System
Theory (CAST)",
year = "2006",
publisher = "unknown",
isbn = "906984477x",
pages = "127138",
abstract =
"Algebraic curves and surfaces have been studied intensively in
algebraic geometry for centuries. Thus, there exists a huge amount
of theoretical knowledge about these geometric objects. Recently,
algebraic curves and surfaces play an important and ever
increasing role in computer aided geometric design, computer
vision, computer aided manufacturing, coding theory, and
cryptography, just to name a few application areas. Consequently,
theoretical results need to be adapted to practical needs. We need
efficient algorithms for generating, representing, manipulating,
analyzing, rendering algebraic curves and surfaces. Exact computer
algebraic methods can be employed effectively for dealing with
these geometric problems.",
paper = "Wink06.pdf"
}
\end{chunk}
\index{Davies, Rowan}
\index{Pfenning, Frank}
\begin{chunk}{axiom.bib}
@article{Davi01,
author = "Davies, Rowan and Pfenning, Frank",
title = {{A Modal Analysis of Staged Computation}},
journal = "J. ACM",
volume = "48",
number = "3",
pages = "555604",
year = "2001",
abstract =
"We show that a type system based on the intuitionistic modal logic S4
provides an expressive framework for specifying and analyzing
computation stages in the context of typed $\lambda$calculi and
functional languages. We directly demonstrate the sense in which our
$\lambda_e^{\rightarrow\box}$calculus captures staging, and also give
a conservative embedding of Nielson and Nielson's twolevel functional
language in our functional language MiniML${}^\box$, thus proving that
bindingtime correctness is equivalent to modal correctness on this
fragment. In addition, MiniML${}^\box$ can also express immediate
evaluation and sharing of code across multiple stages, thus supporting
runtime code generation as well as partial evaluation.",
paper = "Davi01.pdf",
keywords = "printed"
}
\end{chunk}
\index{Pfenning, Frank}
\index{Davies, Rowan}
\begin{chunk}{axiom.bib}
@article{Pfen01,
author = "Pfenning, Frank and Davies, Rowan",
title = {{A Judgemental Reconstruction of Modal Logic}},
journal = "Mathematical Structures in Computer Science",
volume = "11",
pages = "511540",
year = "2001",
abstract =
"We reconsider the foundations of modal logic, following MartinLof's
methodology of distinguishing judgments from propositions. We give
constructive meaning explanations for necessity and possibility which
yields a simple and uniform system of natural deduction for
intuitionistic modal logic which does not exhibit anomalies found in
other proposals. We also give a new presentation of lax logic and nd
that the lax modality is already expressible using possibility and
necessity. Through a computational interpretation of proofs in modal
logic we further obtain a new formulation of Moggi's monadic
metalanguage.",
paper = "Pfen01.pdf",
keywords = "printed"
}
\end{chunk}
\index{Lamport, Leslie}
\begin{chunk}{axiom.bib}
@misc{Lamp03,
author = "Lamport, Leslie",
title = {{The Future of Computing: Logic or Biology}},
link =
"\url{https://lamport.azurewebsites.net/pubs/futureofcomputing.pdf}",
year = "2003",
paper = "Lamp03.pdf",
keywords = "printed"
}
\end{chunk}
\index{Glymour, Clark}
\index{Serafin, Luke}
\begin{chunk}{axiom.bib}
@misc{Glym15,
author = "Glymour, Clark and Serafin, Luke",
title = {{Mathematical Metaphysics}},
link = "\url{http://shelf1.library.cmu.edu/HSS/2015/a1626190.pdf}",
year = "2015",
paper = "Glym15.pdf",
keywords = "printed"
}
\end{chunk}
\index{Reynolds, John C.}
\begin{chunk}{axiom.bib}
@article{Reyn93,
author = "Reynolds, John C.",
title = {{The Discoveries of Continuations}},
journal = "Lisp and Symbolic Computation",
volume = "6",
pages = "233248",
year = "1993",
abstract =
"We give a brief account of the discoveries of continuations and
related concepts.",
paper = "Reyn93.pdf",
keywords = "printed"
}
\end{chunk}
\index{Oles, Frank Joseph}
\begin{chunk}{axiom.bib}
@phdthesis{Oles82,
author = "Oles, Frank Joseph",
title = {{A CategoryTheoretic Approach to the Semantics of
Programming Languages}},
school = "Syracuse University",
year = "1982",
abstract =
"Here we create a framework for handling the semantics of fully
typed programming languages with imperative features, higherorder
ALGOLlike procedures, block structure, and implicit
conversions. Our approach involves introduction of a new family of
programming languages, the {\sl coercive typed $\lambda$calculi},
denoted by $L$ in the body of the dissertation. By appropriately
choosing the linguistic constants (i.e. generators) of $L$, we can
view phrases of variants of ALGOL as syntactically sugared phrases
of $L$.
This dissertation breaks into three parts. In the first part,
consisting of the first chapter, we supply basic definitions and
motivate the idea that functor categories arise naturally in the
explanation of block structure and stack discipline. The second
part, consisting of the next three chapters, is dedicated to the
general theory of the semantics of the coercive typed
$\lambda$calculus; the interplay between posets, algebras, and
Cartesian closed categories is particularly intense here. The
remaining four chapters make up the final part, in which we apply
the general theory to give both direct and continuation semantics
for desugared variants of ALGOL. To do so, it is necessary to show
certain functor categories are Cartesian closed and to describe a
category $\Sigma$ of store shapes. An interesting novelty in the
presentation of continuation semantics is the view that commands
form a procedural, rather than a primitive, phrase type.",
paper = "Oles82.pdf"
}
\end{chunk}
\index{Abdali, S. Kamal}
\index{Winkler, Franz}
\begin{chunk}{axiom.bib}
@techreport{Abda81,
author = "Abdali, S. Kamal and Winkler, Franz",
title = {{A LambdaCalculus Model for Generating Verification Conditions}},
type = "technical report",
institution = "Rensselaer Polytechnic Institute",
number = "CS8104",
year = "1981",
abstract =
"A lambdacalculusbased method is developed for the automatic
generation of verification conditions. A programming language is
specified in which inductive assertions associated with a program
are incorporated within the body of the program by means of assert
and maintainwhile statements. This programming language includes
the following features: assignments, conditionals, loops,
compounds, ALGOLtype block structure. A model is developed which
consists of rules to translate each statement in this programming
language into the lambacalculus. The model is such that the
lambdaexpression translation of any program reduces to a list
(tuple) of lambdaexpression representations of all verification
conditions of the program. A proof of this property is given.",
paper = "Abda81.pdf",
keywords = "printed"
}
\end{chunk}
\index{Abdali, S. Kamal}
\begin{chunk}{axiom.bib}
@book{Abda73,
author = "Abdali, S. Kamal",
title = {{A Simple LambdaCalculus Model of Programming Languages}},
isbn = "9781332196029",
publisher = "Forgotten Books",
year = "1973",
abstract =
"We present a simple correspondence between a large subset of
ALGOL 60 language and lambdacalculus. With the aid of this
correspondence, a program can be translated into a single
lambdaexpression. In general, the representation of a program is
specified by means of a system of simultaneous conversion
relations among the representations of the program
constituents. Highlevel programming language features are treated
directly, not in terms of the representations of machinelevel
operations. The model includes inputoutput in such a way that
when the representation of a (convergent) program is applied to
the input item representations, the resulting combination reduces
to a tuple of the representations of the output items. This model
does not introduce any imperative notions into the calculus; the
descriptive programming constructs, such as expressions, and the
imperative ones, such as assignment and jumps, are translated
alike into pure lambda expressions. The applicability of the model
to the problems of proving program equivalence and correctness is
illustrated by means of simple examples."
paper = "Abda73.pdf"
}
\end{chunk}
\index{Abdali, S. Kamal}
\begin{chunk}{axiom.bib}
@article{Abda74,
author = "Abdali, S. Kamal",
title = {{A LambdaCalculus Model of Programming Languages 
I. Simple Constructs}},
journal = "J. of Computer Languages",
volume = "1",
pages = "287301",
year = "1974",
abstract =
"A simple correspondence is presented between the elementary
constructs of programming languages and the lambdacalculus. The
correspondence is obtained by using intuitive, functional
interpretation of programming language constructs, completely
avoiding the notions of machine memory and address. In particular,
the concepts of program variable and assignments are accounted for
in terms of the concepts of mathematical variable and
substitution, respectively. Lambdaexpression representations are
given of assignments, conditional and compound statements,
inputoutput, and blocks. Algol 60 is used as the illustrative
language.",
paper = "Abda74.pdf",
keywords = "printed"
}
\end{chunk}
\index{Abdali, S. Kamal}
\begin{chunk}{axiom.bib}
@article{Abda74a,
author = "Abdali, S. Kamal",
title = {{A LambdaCalculus Model of Programming Languages 
II. Jumps and Procedures}},
journal = "J. of Computer Languages",
volume = "1",
pages = "303320",
year = "1974",
abstract =
"The correspondence between programming languages and the
lambdacalculus presented in Part I of the paper is extended there
to include iteration statements, jumps, and procedures. Programs
containing loops are represented by lambdaexpressions whose
components are specified recursively by means of systems of
simultaneous conversion relations. The representation of
callbyname and sideeffects in a program is accomplished without
any resort to the concepts of memory andaddress by making use of a
number of variables in addition to those declared by the programs;
with the aid of these additional variables, the parameter linkage
operations can be simulated by pure substitution. The
applicability of the model to the problems of proving program
correctness and equivalence is demonstrated by means of examples.",
paper = "Abda74a.pdf",
keywords = "printed"
}
\end{chunk}
\index{Abdali, S. Kamal}
\begin{chunk}{axiom.bib}
@phdthesis{Abda74b,
author = "Abdali, S. Kamal",
title = {{A Combinatory Logic Model of Programming Languages}},
school = "University of Wisconsin",
year = "1974",
abstract =
"A simple correspondence is presented between a large subset of the
ALGOL 60 language and the combinatory logic. With the aid of this
correspondence, a program can be translated into a single combinatory
object. The combinatory object representing a program is specified,
in general, by means of a system of reduction relations among the
representations of the program constituents. This object denotes, in
terms of the combinatory logic, the function that the program is
intended to compute.
The model has been derived by using intuitive, functional
interpretations of the constructs of programming languages, completely
avoiding the notions of machine command and address. In particular,
the concepts of program variable, assignment, and procedure have been
accounted for in terms of the concepts of mathematical variable,
substitution, and function, respectively.
Highlevel programming language features are represented in the
combinatory logic directly, not in terms of the representations of
machinelevel operations. Inputoutput is treated in such a
manner that when the representation of a program is applied to the
representations of the input items, the resulting combination reduces
to a tuple of the representations of the output items.
The applicability of the model to the problems of
proving program equivalence and correctness is illustrated
by means of examples.",
paper = "Abda74b.pdf"
}
\end{chunk}
\index{Krall, Andreas}
\begin{chunk}{axiom.bib}
@misc{Kralxx,
author = "Krall, Andreas",
title = {{Implementation Techniques for Prolog}},
link = "\url{https://pdfs.semanticscholar.org/fdbf/aa46bf6ab2148595f638fe9afe97033583ee.pdf}",
year = "unknown",
abstract =
"This paper is a short survey about currently used implementation
techniques for Prolog. It gives an introduction to unification and
resolution in Prolog and presents the memory model and a basic
execution model. These models are expanded to the Vienna Abstract
Machine (VAM) with its two versions, the VAM${}_{2p}$ and the
VAM${}_{1p}$, and the most famous abstract machine, the Warren
Abstract Machine (WAM). The continuation passing style model of
Prolog, binary Prolog, leands to the BinWAM. Abstract
interpretation can be applied to gather information about a
program. This information is used in the generation of very
specialized machine code and in optimizations like clause indexing
and instruction scheduling on each kind of abstract machine.",
paper = "Kralxx.pdf",
keywords = "printed"
}
\end{chunk}
\index{Abadi, Martin}
\index{Cardelli, Luca}
\index{Curien, PierreLouis}
\index{Levy, JeanJacques}
\begin{chunk}{axiom.bib}
@inproceedings{Abad90,
author = "Abadi, Martin and Cardelli, Luca and Curien, PierreLouis
and Levy, JeanJacques",
title = {{Explicit Substitutions}},
booktitle = "Symp. of Principles of Programming Languages",
publisher = "ACM",
year = "1990",
link = "\url{http://www.hpl.hp.com/techreports/CompaqDEC/SRCRR54.pdf}",
abstract =
"The $lambda\sigma$calculus is a refinement of the
$lambda$calculus where substitutions are manipulated
explicitly. The $\lambda\sigma$calculus provides a setting for
studying the theory of substitutions, with pleasant mathematical
properties. It is also a useful bridge between the classical
$\lambda$calculus and concrete implementations.",
paper = "Abad90.pdf",
keywords = "printed"
}
\end{chunk}
\index{Beeson, Michael}
\begin{chunk}{axiom.bib}
@article{Bees80a,
author = "Beeson, Michael",
title = {{Formalizing Constructive Mathematics: Why and How?}},
journal = "Lecture Notes in Mathematics",
volume = "873",
pages = "146190",
year = "1980",
paper = "Bees80a.pdf"
}
\end{chunk}
\index{Goodman, Nicolas D.}
\begin{chunk}{axiom.bib}
@article{Good80,
author = "Goodman, Nicolas D.",
title = {{Reflections on Bishop's Philosophy of Mathematics}},
journal = "Lecture Notes in Mathematics",
volume = "873",
pages = "135145",
year = "1980",
paper = "Good80.pdf",
keywords = "printed"
}
\end{chunk}
\index{Rosenkranz, Markus}
\begin{chunk}{axiom.bib}
@book{Rose07,
author = "Rosenkranz, Markus",
title = {{Gr\"obner Bases in Symbolic Analysis}},
publisher = "Walter de Gruyter, Berlin Germany",
year = "2007",
isbn = "978311.0193237",
keywords = "axiomref, TPDref"
}
\end{chunk}
\index{Daly, Timothy}
\begin{chunk}{axiom.bib}
@misc{Daly06,
author = "Daly, Timothy",
title = {{Literate Programming}},
link = "\url{http://lambdatheultimate.org/node/1336}",
year = "2006",
keywords = "axiomref, TPDref"
}
\end{chunk}
\index{Prengel, Alex}
\begin{chunk}{axiom.bib}
@misc{Pren16,
author = "Prengel, Alex",
title = {{MIT axiommath_v8.14}},
link = "\url{http://web.mit.edu/axiommath_v8.14/}",
year = "2016",
keywords = "axiomref, TPDref"
}
\end{chunk}
\index{Jenks, Richard D.}
\begin{chunk}{axiom.bib}
@article{Jenk11,
author = "Jenks, Richard D.",
title = {{The 2011 Richard D. Jenks Memorial Prize}},
journal = "ACM Communications in Computer Algebra",
volume = "45",
number = "4",
year = "2011",
abstract =
"The 2011 Richard D. Jenks Memorial Prize for Excellence in
Software Engineering Applied to Computer Algebra was presented by
members of the Prize Selection Committee and its chair, Erich
Kaltofen, at ISSAC and SNC in San Jose, CA, on June 9, 2011 to the
Maple Project at the University of Waterloo.",
paper = "Jenk11.pdf",
keywords = "axiomref"
}
\end{chunk}
\index{Jenks, Richard D.}
\begin{chunk}{axiom.bib}
@article{Jenk13,
author = "Jenks, Richard D.",
title = {{The 2013 Richard D. Jenks Memorial Prize}},
journal = "ACM Communications in Computer Algebra",
volume = "47",
number = "4",
year = "2013",
abstract =
"The 2013 Richard D. Jenks Memorial Prize for Excellence in
Software Engineering Applied to Computer Algebra was announced by
members of the Prize Selection Committee, Mark Giesbrecht
representing its chair Erich Kaltofen, at ISSAC in Boston, MA, on
June 28, 2013 to have been awared to Professor William Arthur
Stein of the Sage Project at the University of Washington.",
paper = "Jenk13.pdf",
keywords = "axiomref"
}
\end{chunk}
\index{Jenks, Richard D.}
\begin{chunk}{axiom.bib}
@article{Jenk15,
author = "Jenks, Richard D.",
title = {{The 2015 Richard D. Jenks Memorial Prize}},
journal = "ACM Communications in Computer Algebra",
volume = "49",
number = "4",
year = "2015",
abstract =
"The 2015 Richard D. Jenks Memorial Prize was awarded on October
30, 2015 at the Fields Institute in Toronto during the Major
Thematic Program on Computer Algebra to Professor Victor Shoup for
NTL: A Library for doing Number Theory.",
paper = "Jenk15.pdf",
keywords = "axiomref"
}
\end{chunk}
\index{Jenks, Richard D.}
\begin{chunk}{axiom.bib}
@article{Jenk17,
author = "Jenks, Richard D.",
title = {{The 2017 Richard D. Jenks Memorial Prize}},
journal = "ACM Communications in Computer Algebra",
volume = "51",
number = "4",
year = "2017",
abstract =
"The 2017 Richard D. Jenks Memorial Prize for Excellence in
Software Engineering Applied to Computer Algebra has been awarded
to Stephen Wolfram for WolframAlpha and Mathematica.",
paper = "Jenk17.pdf",
keywords = "axiomref"
}
\end{chunk}
\index{Lazard, Daniel}
\begin{chunk}{axiom.bib}
@article{Laza01,
author = "Lazard, Daniel",
title = {{Solving Systems of Algebraic Equations}},
journal = "ACM SIGSAM Bulletin",
volume = "35",
number = "3",
year = "2001",
abstract =
"Let $f_1,\ldots,f_k$ be $k$ k multivariate polynomials which have
a finite number of common zeros in the algebraic closure of the ground
field, counting the common zeros at infinity. An algorithm is
given and proved which reduces the computations of these zeros to
the resolution of a single univariate equation whose degree is the
number of common zeros. This algorithm gives the whole algebraic
and geometric structure of the set of zeros (multiplicities,
conjugate zeros,...). When all the polynomials have the same degree,
the complexity of this algorithm is polynomial relative to the generic
number of solutions.",
paper = "Laza01.pdf"
}
\end{chunk}
\index{Abramov, S.A.}
\begin{chunk}{axiom.bib}
@article{Abra00,
author = "Abramov, S.A.",
title = {{A Note on the Number of Division Steps in the Euclidean
Algorithm}},
journal = "ACM SIGSAM",
volume = "34",
number = "4",
year = "2000",
paper = "Abra00.pdf",
keywords = "printed"
}
\end{chunk}
\index{Essex, Christopher}
\index{Davison, Matt}
\index{Schulzky, Christian}
\begin{chunk}{axiom.bib}
@article{Esse00,
author = "Essex, Christopher and Davison, Matt and Schulzky, Christian",
title = {{Numerical Monsters}},
journal = "ACM SIGSAM",
volume = "34",
number = "4",
year = "2000",
abstract =
"When the results of certain computer calculations are shown to be not
simply incorrect but dramatically incorrect, we have a powerful reason
to be cautious about all computerbased calculations. In this paper we
present a 'Rogue's Gallery' of simple calculations whose correct
solutions are obvious to humans but whose numerical solutions are
incorrect in pathological ways. We call these calculations, which can
be guaranteed to wreak numerical mayhem across both software
packages and hardware platforms, 'Numerical Monsters'. Our monsters
can be used to provide deep insights into how computer calculations
fail, and we use t h e m to engender appreciation for the subject of
numerical analysis in our students. Although these monsters are based
on wellunderstood numerical pathologies, even experienced numerical
analysts will find surprises in their behaviour and ,can use the
lessons they bring to become even better masters of their tools.",
paper = "Esse00.pdf"
}
\end{chunk}
\index{Buchberger, Bruno}
\begin{chunk}{axiom.bib}
@article{Buch02,
author = "Buchberger, Bruno",
title = {{Computer Algebra: The End of Mathematics?}},
journal = "ACM SIGSAM",
volume = "36",
number = "1",
year = "2002",
abstract =
"Mathematical software systems, such as Mathematica, Maple, Derive,
and so on, are substantially based on enormous advances in the area of
mathematics known as Computer Algebra or Symbolic Mathematics. In
fact, everything taught in high school and in the first semesters of a
university mathematical education, is available in these systems 'at
the touch of the button'. Will mathematics become unnecessary because
of this? In the three sections of this essay, I answer this question
for nonmathematicians, for mathematicians and for (future) students
of mathematics.",
paper = "Buch02.pdf"
}
\end{chunk}
\index{Barnett, Michael P.}
\begin{chunk}{axiom.bib}
@article{Barn08,
author = "Barnett, Michael P.",
title = {{Reasoning in Symbolic Computation}},
journal = "ACM Communications in Symbolic Algebra",
volume = "42",
number = "1",
year = "2008",
abstract =
"I discuss notations for some styles of mathematical reasoning that
include analogy. These notations extend the conventions of the
mathematica package mathscape that I reported recently in the
Journal of Symbolic Computation. The paper introduces the reasoning
objects that I call 'precursors' and 'consequences lists'.",
paper = "Barn08.pdf",
keywords = "printed"
}
\end{chunk}
\index{Lichtblau, Daniel}
\begin{chunk}{axiom.bib}
@article{Lich11,
author = "Lichtblau, Daniel",
title = {{Symbolic Definite (and Indefinite) Integration: Methods and
Open Issues}},
journal = "ACM Comm. in Computer Algebra",
volume = "45",
number = "1",
year = "2011",
link = "\url{http://www.sigsam.org/bulletin/articles/175/issue175.pdf}",
abstract = "
The computation of definite integrals presents one with a variety of
choices. There are various methods such as NewtonLeibniz or Slater's
convolution method. There are questions such as whether to split or
merge sums, how to search for singularities on the path of
integration, when to issue conditional results, how to assess
(possibly conditional) convergence, and more. These various
considerations moreover interact with one another in a multitude of
ways. Herein we discuss these various issues and illustrate
with examples.",
paper = "Lich11.pdf"
}
\end{chunk}
\index{Zengler, Christoph}
\index{Kubler, Andreas}
\index{Kuchlin, Wolfgang}
\begin{chunk}{axiom.bib}
@article{Zeng11,
author = "Zengler, Christoph and Kubler, Andreas and Kuchlin, Wolfgang",
title = {{New Approaches to Boolean Quantifier Elimination}},
journal = "ACM Comm. in Computer Algebra",
volume = "45",
number = "2",
year = "2011",
abstract =
"We present four different approaches for existential Boolean
quantifier elimination, based on model enumeration, resolution,
knowledge compilation with projection, and substitution. We point out
possible applications in the area of verification and we present
preliminary benchmark results of the different approaches.",
paper = "Zeng11.pdf",
keywords = "printed"
}
\end{chunk}
\index{Stoutemyer, David R.}
\begin{chunk}{axiom.bib}
@article{Stou11,
author = "Stoutemyer, David R.",
title = {{Ways to Implement Computer Algebra Compactly}},
journal = "ACM Comm. in Computer Algebra",
volume = "45",
number = "4",
year = "2011",
abstract =
"Computer algebra had to be implemented compactly to fit on early
personal computers and handheld calculators. Compact implementation
is still important for portable handheld devices. Also, compact
implementation increases comprehensibility while decreasing develop
ment and maintenance time and cost, regardless of the platform. This
article describes several ways to achieve compact implementations,
including:
\begin{itemize}
\item Exploit evaluation followed by interpolation to avoid
implementing a parser, such as in PicoMath
\item Use contiguous storage as an expression stack to avoid garbage
collection and pointerspace overhead, such as in Calculus Demon
and TIMathEngine
\item Use various techniques for saving code space for linkedstorage
representation of expressions and functions, such as muMath and Derive
\end{itemize}",
paper = "Stou11.pdf",
keywords = "axiomref"
}
\end{chunk}
\index{Roche, Daniel S.}
\begin{chunk}{axiom.bib}
@article{Roch11,
author = "Roche, Daniel S.",
title = {{Chunky and EqualSpaced Polynomial Multiplication}},
journal = "J. Symbolic Computation",
volume = "46",
pages = "791806",
year = "2011",
abstract =
"Finding the product of two polynomials is an essential and basic
problem in computer algebra. While most previous results have
focused on the worstcase complexity, we instead employ the
technique of adaptive analysis to give an improvement in many
‘‘easy’’ cases. We present two adaptive measures and methods
for polynomial multiplication, and also show how to effectively
combine them to gain both advantages. One useful feature of these
algorithms is that they essentially provide a gradient between
existing ‘‘sparse’’ and ‘‘dense’’ methods. We prove that these
approaches provide significant improvements in many cases but
in the worst case are still comparable to the fastest existing
algorithms.",
paper = "Roch11.pdf"
}
\end{chunk}
\index{Bailey, David H.}
\index{Borwein, Jonathan M.}
\index{Kaiser, Alexander D.}
\begin{chunk}{axiom.bib}
@article{Bail14,
author = "Bailey, David H. and Borwein, Jonathan M. and
Kaiser, Alexander D.",
title = {{Automated Simplification of Large Symbolic Expressions}},
journal = "J. Symbolic Computation",
volume = "60",
pages = "120136",
year = "2014",
abstract =
"We present a set of algorithms for automated simplification of
symbolic constants of the form
$\sum_i\alpha_i x_i$ with $\alpha_i$ rational and $x_i$
complex. The included algorithms, called SimplifySum and
implemented in Mathematica , remove redundant terms, attempt to make
terms and the full expression real, and remove terms using repeated
application of the multipair PSLQ integer relation detection
algorithm. Also included are facilities for making substitutions
according to userspecified identities. We illustrate this toolset by
giving some realworld examples of its usage, including one, for
instance, where the tool reduced a symbolic expression of
approximately 100 000 characters in size enough to enable manual
manipulation to one with just four simple terms.",
paper = "Bail14.pdf"
}
\end{chunk}
\index{Bailey, David H.}
\index{Borwein, Jonathan M.}
\begin{chunk}{axiom.bib}
@article{Bail11,
author = "Bailey, David H. and Borwein, Jonathan M.",
title = {{Highprecision Numerical Integration: Progress and Challenges}},
journal = "J. Symbolic Computation",
number = "46",
pages = "741754",
year = "2011",
abstract =
"One of the most fruitful advances in the field of experimental
mathematics has been the development of practical methods for very
highprecision numerical integration, a quest initiated by Keith
Geddes and other researchers in the 1980s and 1990s.These
techniques, when coupled with equally powerful integer relation
detection methods, have resulted in the analytic evaluation of many
integrals that previously were beyond the realm of symbolic
techniques.This paper presents a survey of the current stateoftheart
in this area (including results by the present authors and others),
mentions some new results, and then sketches what challenges lie
ahead.",
paper = "Bail11.pdf"
}
\end{chunk}
\index{Huang, Zongyan}
\index{England, Matthew}
\index{Wilson, David}
\index{Davenport, James H.}
\index{Paulson, Lawrence C.}
\begin{chunk}{axiom.bib}
@article{Huan14,
author = "Huang, Zongyan and England, Matthew and Wilson, David and
Davenport, James H. and Paulson, Lawrence C.",
title = {{A Comparison of Three Heuristics to Choose the Variable
Ordering for Cylindrical Algebraic Decomposition}},
journal = "ACM Comm. in Computer Algebra",
volume = "48",
number = "3",
year = "2014",
abstraact =
"Cylindrical algebraic decomposition (CAD) is a key tool for problems
in real algebraic geometry and beyond. When using CAD there is often a
choice over the variable ordering to use, with some problems
infeasible in one ordering but simple in another. Here we discuss a
recent experiment comparing three heuristics for making this choice on
thousands of examples.",
paper = "Huan14.pdf"
}
\end{chunk}
\index{Hamada, Tatsuyoshi}
\begin{chunk}{axiom.bib}
@article{Hama14,
author = "Hamada, Tatsuyoshi",
title = {{MathLibre: Personalizable Computer Environment for
Mathematical Research}},
volume = "48",
number = "3",
year = "2014",
abstract =
"MathLibre is a project to archive free mathematical software and free
mathematical documents and offer them on Live Linux system. MathLibre
Project is the direct descendant of KNOPPIX/Math Project. It provides
a desktop for mathematicians that can be set up easily and quickly.",
paper = "Hama14.pdf"
}
\end{chunk}
\index{Fateman, Richard}
\begin{chunk}{axiom.bib}
@article{Fate14a,
author = "Fateman, Richard",
title = {{Algorithm Differentiation in Lisp: ADIL}},
journal = "ACM Comm. in Computer Algebra",
volume = "48",
number = "3",
year = "2014",
abstract =
"Algorithm differentiation (AD) is a technique used to transform a
program $F$ computing a numerical function of one argument $F(x)$ into
another program $G(p)$ that returns a pair,
$\langle F (p), F^\prime(p)\rangle$ where by $F^\prime(p)$
we mean the derivative of $F$ with respect to its argument $x$,
evaluated at $x = p$. That is, we have a program AD that takes as input
a program, and returns another: $G := AD(F)$. Over the years AD
programs have been developed to allow $F$ to be expressed in some
specialized variant of a popular programming language L (FORTRAN, C,
Matlab, Python) and where $G$ is delivered in that language $L$ or some
other. Alternatively, executing $F(p)$ is some environment will deliver
$\langle F^\prime(p), F(p)\rangle$ directly. AD tools have also
been incorporated in computer algebra systems (CAS) such as
Maple. A CAS is hardly necessary for the task of writing the AD
program, since the main requirement is a set of tools for
manipulation of an internal (typically tree) form of a program.
In Lisp, a normal program is already in this form and so the AD
program in Lisp (ADIL), the target $F$ and the product $G$ can
all be expressed compactly in Lisp. In spite of the brevity and
extensibility of the ADIL program, we can provide
features which are unsupported in other AD programs. In particular,
recursive functions are easily accommodated. Our perspective here is
to point out that for scientists who write programs in Lisp or any
language that can be converted to Lisp, AD is easily at hand.",
paper = "Fate14a.pdf"
}
\end{chunk}
\index{England, M.}
\index{ChebTerrab, E.}
\index{Bradford, R.}
\index{Davenport, J.H.}
\index{Wilson, D.}
\begin{chunk}{axiom.bib}
@article{Engl14c,
author = "England, M. and ChebTerrab, E. and Bradford, R. and
Davenport, J.H. and Wilson, D.",
title = {{Branch Cuts in MAPLE 17}},
journal = "ACM Comm. in Computer Algebra",
volume = "48",
number = "1",
year = "2014",
abstract =
"Accurate and comprehensible knowledge about the position of branch
cuts is essential for correctly working with multivalued functions,
such as the square root and logarithm. We discuss the new tools in
Maple 17 for calculating and visualising the branch cuts of such
functions, and others built up from them. The cuts are described in an
intuitive and accurate form, offering substantial improvement on the
descriptions previously available.",
paper = "Engl14c.pdf"
}
\end{chunk}
\index{Stoutemyer, David R.}
\begin{chunk}{axiom.bib}
@article{Stou13,
author = "Stoutemyer, David R.",
title = {{A Computer Algebra User Interface Manifesto}},
journal = "ACM Communications in Computer Algebra",
volume = "47",
number = "4",
year = "2013",
abstract =
"Many computer algebra systems have more than 1000 builtin functions,
making expertise difficult. Using mock dialog boxes, this article
describes a proposed interactive generalpurpose wizard for organizing
optional transformations and allowing easy fine grain control over the
form of the result – even by amateurs. This wizard integrates ideas
including:
\begin{itemize}
\item flexible subexpression selection;
\item complete control over the ordering of variables and
commutative operands, with wellchosen defaults;
\item interleaving the choice of successively less main
variables with applicable function choices to provide detailed
control without incurring a combinatorial number of applicable
alternatives at any one level;
\item quick applicability tests to reduce the listing of
inapplicable transformations;
\item using an organizing principle to order the alternatives
in a helpful manner;
\item labeling quicklycomputed alternatives in dialog boxes
with a preview of their results, using ellipsis elisions if
necessary or helpful;
\item allowing the user to retreat from a sequence of choices
to explore other branches of the tree of alternatives – or to
return quickly to branches already visited;
\item allowing the user to accumulate more than one of the
alternative forms;
\item integrating direct manipulation into the wizard; and
\item supporting not only the usual inputresult pair mode, but
also the useful alternative derivational and in situ replacement
modes in a unified window.
\end{itemize}",
paper = "Stou13.pdf",
kryeotfd = "printed"
}p
\end{chunk}
\index{Sorenson, Jonathan}
\begin{chunk}{axiom.bib}
@article{Sore94,
author = "Sorenson, Jonathan",
title = {{Two Fast GCD Algorithms}},
journal = "Journal of Algorithms",
volume = "16",
pages = "110144",
year = "1994",
abstract =
"We present two new algorithms for computing geatest common
divisors: the right and leftshift $k$ary GCD algorithms. These
algorithms are generalizations of the binary and leftshift binary
algorithms. Interestingly, both new algorithms have sequential
versions that are practical and efficient and parallel versions
that rival the best previous parallel GCD algorithms. We show that
sequential versions of both algorithms take $O(n^2/log~n)$ bit
operations in the worst case to compute the GCD of two nbit
integers. This compares favorably to the Euclidean and moth
precision versions of these GCD algorithms, and we found that both
$k$ary algorithms are faster than the Euclidean and binary
algorithms on inputs of 100 to 1000 decimal digits in length. We
show that parallel versions of both algorithms match the
complexity of the best previous parallel GCD algorithm due to Chor
and Goldreich. Specifically, if $log~n\le k \le 2^n$ and $k$ is a
power of two, then both algorithms run in $O(n/log~n+log^2~n)$
time using a number of processors bounded by a polynomial in $n$
and $k$ on a common CRCW PRAM. We also discuss extended versions
of both algorithms.",
paper = "Sore94.pdf",
keywords = "printed"
}
\end{chunk}
\index{Weber, Kenneth}
\index{Trevisan, Vilmar}
\index{Martins, Luiz Felipe}
\begin{chunk}{axiom.bib}
@article{Webe05a,
author = "Weber, Kenneth and Trevisan, Vilmar and Martins, Luiz Felipe",
title = {{A Modular Integer GCD Algorithm}},
journal = "J. of Algorithms",
volume = "54",
year = "2005",
pages = "152167",
abstract =
"This paper describes the first algorithm to compute the greatest
common divisor (GCD) of two $n$bit integers using a modular
representation for intermediate values $U$, $V$ and also for the
result. It is based on a reduction step, similar to one used in
the accelerated algorithm when $U$ and $V$ are close to the same
size, that replaces $U$ by $(UbV)/p$, where $p$ is one of the
prime moduli and $b$ is the unique integer in the interval
$(p/2,p/2)$ such that $b\equiv UV^{1} (mod~p)$. When the
algorithm is executed on a bit common CRCW PRAM with
$O(n~log~n~log~log~log~n)$ processors, it takes $(O(n)$ time in
the worst case. A heuristic model of the average case yields
$O(n/log~n)$ time on the same number of processors.",
paper = "Webe05a.pdf",
keywords = "printed"
}
\end{chunk}
\index{Schonhage, A.}
\begin{chunk}{axiom.bib}
@article{Scho88,
author = "Schonhage, A.",
title = {{Probabilistic Computation of Integer Polynomial GCDs}},
journal = "J. of Algorithms",
volume = "9",
pages = "365371",
year = "1988",
abstract =
"We describe a probabilistic algorithm for the computation of the
gcd of two univariate integer polynomials of degrees $\le n$ with
their $l^1$norms being bounded by $2^h$ and estimate its expected
running time by a worstcase bound of
$O(n(n+h)^{l+\epsilon(l)})$.",
paper = "Scho88.pdf",
keywords = "printed"
}
\end{chunk}
\index{LeGuin, Ursula K.}
\begin{chunk}{axiom.bib}
@book{Legu76,
author = "LeGuin, Ursula K.",
title = {{The Left Hand of Darkness}},
publisher = "Penguin Random House",
year = "1976",
isbn = "9781101665398"
}
\end{chunk}
\index{Shulman, Michael}
\begin{chunk}{axiom.bib}
@misc{Shul18,
author = "Shulman, Michael",
title = {{Linear Logic for Constructive Mathematics}},
link = "\url{https://arxiv.org/pdf/1805.07518.pdf}",
year = "2018",
abstract =
"We show that numerous distinctive concepts of constructive
mathematics arise automatically from an interpretation of 'linear
higherorder logic' into intuitionistic higherorder logic via a Chu
construction. This includes apartness relations, complemented
subsets, antisubgroups and antiideals, strict and nonstrict order
pairs, cutvalued metrics, and apartness spaces. We also explain the
constructive bifurcation of classical concept s using the choice
between multiplicative and additive linear connectives. Linear logic
thus systematically 'constructivizes' classical definitions and deals
automatically with the resulting bookkeeping, and could potentially
be used directly as a basis for constructive mathematics in place
of intuitionistic logic.",
paper = "Shul18.pdf",
keywords = "printed"
}
\end{chunk}
\index{Khan, Muhammad Taimoor}
\begin{chunk}{axiom.bib}
@techreport{Khan13,
author = "Khan, Muhammad Taimoor",
title = {{On the Formal Verification of Maple Programs}},
year = "2013",
type = "technical report",
number = "1307",
institution = "RISC Linz",
abstract =
"In this paper, we present an examplebased demonstration of our
recent results on the formal verification of programs written in the
computer algebra language (Mini)Maple (a slightly modified subset of
Maple). The main goal of this work is to develop a verification
framework for behavioral analysis of MiniMaple programs. For
verification, we translate an annotated MiniMaple program into the
language Why3ML of the intermediate verification tool Why3 developed
at LRI, France. We generate verification conditions by the
corresponding component of Why3 and later prove the correctness of
these conditions by various supported by the Why3 backend automatic
and interactive theorem provers. We have used the verification
framework to verify some parts of the main test example of our
verification framework, the Maple package DifferenceDifferential
developed at our institute to compute bivariate differencedifferential
polynomials using relative Gr ̈obner bases.",
paper = "Khan13.pdf",
keywords = "printed"
}
\end{chunk}
\index{Daly, Timothy}
\begin{chunk}{axiom.bib}}
@misc{Daly03,
author = "Daly, Timothy",
title = {{Axiom Website: http://axiomdeveloper.org}},
link = "\url{http://axiomdeveloper.org}",
keywords = "axiomref",
year = "2003"
}
\end{chunk}
\index{Dijkstra, Edsgar W.}
\begin{chunk}{axiom.bib}
@article{Dijk75,
author = "Dijkstra, Edsgar W.",
title = {{Guarded Commands, Nondeterminancy and Formal Derivation
of Programs}},
journal = "Comm. of the ACM",
volume = "18",
number = "8",
year = "1975",
pages = "453457",
abstract =
"Socalled 'guarded commands' are introduced as a building block
for alternative and repetitive constructs that allow
nondeterministic program components for which at least the
activity evoked, but possibly even the final state, is not
necessarily uniquly determined by the initial state. For the
formal derivation of programs expressed in terms of these
constructs, a calculus will be shown.",
paper = "Dijk75.pdf",
keywords = "printed"
}
\end{chunk}
\index{van Emden, M.H.}
\index{Kowalski, R.A.}
\begin{chunk}{axiom.bib}
@article{Emde76,
author = "van Emden, M.H. and Kowalski, R.A.",
title = {{The Semantics of Predicate Logic as a Programming Language}},
journal = "J. Association for Computing Machinery",
volume = "23",
number = "4",
year = "1976",
pages = "733742",
abstract =
"Sentences in firstorder predicate logic can be usefully interpreted
as programs In this paper the operational and fixpomt semantics of
predicate logic programs are defined, and the connections with the
proof theory and model theory of logic are investigated It is
concluded that operational semantics is a part of proof theory and
that fixpolnt semantics is a special case of modeltheoret:c
semantics.",
paper = "Emde76.pdf",
keywords = "printed"
}
\end{chunk}
\index{Tarski, Alfred}
\begin{chunk}{axiom.bib}
@article{Tars69,
author = "Tarski, Alfred",
title = {{Truth and Proof}},
journal = "Scientific American",
volume = "1969",
pages = "6377",
year = "1969",
paper = "Tars69.pdf",
keywords = "printed"
}
\end{chunk}
\index{Apt, Krysztof R.}
\index{Bezem, Marc}
\begin{chunk}{axiom.bib}
@inbook{Aptx99,
author = "Apt, Krysztof R. and Bezem, Marc",
title = {{Formulas as Programs}},
booktitle = "The Logic Programming Paradigm",
year = "1999",
publisher = "Springer Berlin Heidelberg",
pages = "75107",
isbn = "9783642600852",
abstract =
"We provide here a computational interpretation of firstorder
logic based on a constructive interpretation of satisfiability
w.r.t. a fixed but arbitrary interpretation. In this approach the
formulas themselves are programs. This contrasts with the
socalled formulas as types approach in which the proofs of the
formulas are typed terms that can be taken as programs. This view
of computing is inspired by logic programming and constraint logic
programming but differs from them in a number of crucial aspects.
Formulas as programs is argued to yield a realistic approach to
programming that has been realized in the implemented programming
language Alma0 Apt, Brunekreef, Partington and Schaerf (1998)
that combines the advantages of imperative and logic
programming. The work here reported can also be used to reason
about the correctness of nonrecursive Alma0 programs that do not
include destructive assignment.",
paper = "Aptx99.pdf",
keywords = "printed"
}
\end{chunk}
\index{Mazur, Barry}
\begin{chunk}{axiom.bib}
@misc{Mazu07,
author = "Mazur, Barry",
title = {{When is One Thing Equal to Some Other Thing?}},
link = "\url{http://www.math.harvard.edu/~mazur/preprints/when_is_one.pdf}",
year = "2007",
paper = "Mazu07.pdf"
}
\end{chunk}
\index{Kant, Immanuel}
\begin{chunk}{axiom.bib}
@book{Kant98,
author = "Kant, Immanuel",
title = {{The Critique of Pure Reason}},
publisher = "Cambridge University Press",
year = "1998",
isbn = "0521354021",
link = "\url{http://strangebeautiful.com/othertexts/kantfirstcritiquecambridge.pdf}",
paper = "Kant98.pdf"
}
\end{chunk}
\index{Smith, A.}
\begin{chunk}{axiom.bib}
@techreport{Smit90,
author = "Smith, A.",
title = {{The KnuthBendix Completion Algorithm and its Specification in Z}},
type = "technical report",
institution = "Ministry of Defence, RSRE Malvern WORCS",
year = "1990",
number = "RSRE Memorandum 4323",
abstract =
"Proving that something is a consequence of a set of axioms can be
very difficult. The KnuthBendix completion algorithm attempts to
automate this process when the axioms are equations. The algorithm
is bound up in the area of term rewriting, and so this memorandum
contains an introduction to the tehory of term rewriting, followed
by an overview of the algorithm. Finally a formal specification of
the algorithm is given using the language Z.",
paper = "Smit90.pdf",
keywords = "printed"
}
\end{chunk}
\index{Dick, A.J.J.}
\begin{chunk}{axiom.bib}
@techreport{Dick88,
author = "Dick, A.J.J.",
title = {{Automated Equational Reasoning and the KnuthBendix Algorithm:
An Informal Introduction}},
year = "1988",
type = "technical report",
institution = "Rutherford Appelton Laboratory",
number = "RAL88043",
paper = "Dick88.pdf",
keywords = "printed"
}
\end{chunk}
\index{Dick, Jeremy}
\begin{chunk}{axiom.bib}
@article{Dick91,
author = "Dick, Jeremy",
title = {{An Introduction to KnuthBendix Completion}},
journal = "The Computer Journal",
volume = "34",
number = "1",
year = "1991",
abstract =
"An informal introduction is given to the underlying concepts of
term rewriting. Topics covered are KnuthBendix completion,
completion modulo equations, unfailing completion and theorem
proving by completion.",
paper = "Dick91.pdf",
keywords = "printed"
}
\end{chunk}
\index{Knuth, Donald E.}
\index{Bendix, Peter B.}
\begin{chunk}
\incollection{Knut70,
author = "Knuth, Donald E. and Bendix, Peter B.",
title = {{Simple Word Problems in Unversal Algebras}},
booktitle = "Computational Problems in Abstract Algebra",
editor = "Leech, John",
publisher = "Pergamon Press",
isbn = "080129757",
year = "1970",
pages = "263298",
paper = "Knut70.pdf",
keywords = "printed"
}
\end{chunk}
\index{Leech, John}
\begin{chunk}{axiom.bib}
@book{Leec70,
author = "Leech, John",
title = {{Computational Problems in Abstract Algebra}},
publisher = "Pergamon Press",
year = "1970",
isbn = "080129757",
paper = "Leec70.pdf"
}
\end{chunk}
\index{Dershowitz, Nachum}
\begin{chunk}{axiom.bib}
@article{Ders87,
author = "Dershowitz, Nachum",
title = {{Termination of Rewriting}},
journal = "J. Symbolic Computation",
volume = "3",
year = "1987",
pages = "69116",
abstract =
"This survey describes methods for proving that systems of rewrite
rules are terminating programs. We illustrate the use in termination
proofs of various kinds of orderings on terms, including polynomial
interpretations and path orderings. The effect of restrictions, such
as linearity, on the form of rules is also considered. In general,
however, termination is an undeeidable property of rewrite systems.",
paper = "Ders87.pdf",
keywords = "printed"
}
\end{chunk}
\index{Atkey, Robert}
\begin{chunk}{axiom.bib}
@misc{Atke18,
author = "Atkey, Robert",
title = {{Parameterised Notions of Computation}},
link = "\url{https://bentnib.org/paramnotionsjfp.pdf}",
year = "2018",
abstract =
"Moggi’s Computational Monads and Power et al ’s equivalent notion of
Freyd category have captured a large range of computational effects
present in programming languages. Examples include nontermination,
nondeterminism, exceptions, continuations, sideeffects and
input/output. We present generalisations of both computational monads
and Freyd categories, which we call parameterised monads and
parameterised Freyd categories, that also capture computational
effects with parameters. Examples of such are composable
continuations, sideeffects where the type of the state varies and
input/output where the range of inputs and outputs varies. By also
considering structured parameterisation, we extend the range of
effects to cover separated sideeffects and multiple independent
streams of I/O. We also present two typed $\lambda$calculi that
soundly and completely model our categorical definitions — with and
without symmetric monoidal parameterisation — and act as prototypical
languages with parameterised effects.",
paper = "Atke18.pdf",
keywords = "printed"
}
\end{chunk}
\index{Bozman, Gerald}
\index{Buco, William}
\index{Daly, Timothy}
\index{Tetzlaff, William}
\begin{chunk}{axiom.bib}
@article{Bozm84,
author = "Bozman, Gerald and Buco, William and Daly, Timothy and
Tetzlaff, William",
title = {{Analysis of Free Storage Algorithms  Revisited}},
journal = "IBM Systems Journal",
volume = "23",
number = "1",
year = "1984",
abstract =
"Most research in freestorage management has centered around
strategies that search a linked list and strategies that partition
storage into predetermined sizes. Such algorithms are analyzed in
terms of CPU efficiency and storage efficiency. The subject of this
study is the freestorage management in the Virtual Machine/System
Product (VM/SP) system control program. As a part of this study,
simulations were done of established, and proposed, dynamic storage
algorithms for the VM/SP operating system. Empirical evidence is given
that simplifying statistical assumptions about the distribution of
interarrival times and holding times has high predictive
ability. Algorithms such as firstfit, modified firstfit, and
bestfit are found to be CPUinefficient. Buddy systems are found to
be very fast but suffer from a high degree of internal
fragmentation. A form of extended subpooling is shown to be as fast as
buddy systems with improved storage efficiency. This algorithm was
implemented for VM/SP, and then measured. Results for this algorithm
are given for several production VM/SP systems.",
paper = "Bozm84.pdf"
}
\end{chunk}

books/axiom.bib  1401 +++++++++++++++++++++++++++++++
books/bookvolbib.pamphlet  1743 ++++++++++++++++++++++++++++++++++++++
changelog  2 +
patch  1530 +++++++++++++++++++++++++++++++++++
src/axiomwebsite/patches.html  2 +
5 files changed, 4566 insertions(+), 112 deletions()
diff git a/books/axiom.bib b/books/axiom.bib
index 3487700..4883459 100644
 a/books/axiom.bib
+++ b/books/axiom.bib
@@ 9445,6 +9445,174 @@ paper = "Brea89.pdf"
link = "\url{http://www.wolfram.com}"
}
+@inproceedings{Abad90,
+ author = "Abadi, Martin and Cardelli, Luca and Curien, PierreLouis
+ and Levy, JeanJacques",
+ title = {{Explicit Substitutions}},
+ booktitle = "Symp. of Principles of Programming Languages",
+ publisher = "ACM",
+ year = "1990",
+ link = "\url{http://www.hpl.hp.com/techreports/CompaqDEC/SRCRR54.pdf}",
+ abstract =
+ "The $lambda\sigma$calculus is a refinement of the
+ $lambda$calculus where substitutions are manipulated
+ explicitly. The $\lambda\sigma$calculus provides a setting for
+ studying the theory of substitutions, with pleasant mathematical
+ properties. It is also a useful bridge between the classical
+ $\lambda$calculus and concrete implementations.",
+ paper = "Abad90.pdf",
+ keywords = "printed"
+}
+
+@book{Abda73,
+ author = "Abdali, S. Kamal",
+ title = {{A Simple LambdaCalculus Model of Programming Languages}},
+ isbn = "9781332196029",
+ publisher = "Forgotten Books",
+ year = "1973",
+ abstract =
+ "We present a simple correspondence between a large subset of
+ ALGOL 60 language and lambdacalculus. With the aid of this
+ correspondence, a program can be translated into a single
+ lambdaexpression. In general, the representation of a program is
+ specified by means of a system of simultaneous conversion
+ relations among the representations of the program
+ constituents. Highlevel programming language features are treated
+ directly, not in terms of the representations of machinelevel
+ operations. The model includes inputoutput in such a way that
+ when the representation of a (convergent) program is applied to
+ the input item representations, the resulting combination reduces
+ to a tuple of the representations of the output items. This model
+ does not introduce any imperative notions into the calculus; the
+ descriptive programming constructs, such as expressions, and the
+ imperative ones, such as assignment and jumps, are translated
+ alike into pure lambda expressions. The applicability of the model
+ to the problems of proving program equivalence and correctness is
+ illustrated by means of simple examples.",
+ paper = "Abda73.pdf"
+}
+
+@article{Abda74,
+ author = "Abdali, S. Kamal",
+ title = {{A LambdaCalculus Model of Programming Languages 
+ I. Simple Constructs}},
+ journal = "J. of Computer Languages",
+ volume = "1",
+ pages = "287301",
+ year = "1974",
+ abstract =
+ "A simple correspondence is presented between the elementary
+ constructs of programming languages and the lambdacalculus. The
+ correspondence is obtained by using intuitive, functional
+ interpretation of programming language constructs, completely
+ avoiding the notions of machine memory and address. In particular,
+ the concepts of program variable and assignments are accounted for
+ in terms of the concepts of mathematical variable and
+ substitution, respectively. Lambdaexpression representations are
+ given of assignments, conditional and compound statements,
+ inputoutput, and blocks. Algol 60 is used as the illustrative
+ language.",
+ paper = "Abda74.pdf",
+ keywords = "printed"
+}
+
+@article{Abda74a,
+ author = "Abdali, S. Kamal",
+ title = {{A LambdaCalculus Model of Programming Languages 
+ II. Jumps and Procedures}},
+ journal = "J. of Computer Languages",
+ volume = "1",
+ pages = "303320",
+ year = "1974",
+ abstract =
+ "The correspondence between programming languages and the
+ lambdacalculus presented in Part I of the paper is extended there
+ to include iteration statements, jumps, and procedures. Programs
+ containing loops are represented by lambdaexpressions whose
+ components are specified recursively by means of systems of
+ simultaneous conversion relations. The representation of
+ callbyname and sideeffects in a program is accomplished without
+ any resort to the concepts of memory andaddress by making use of a
+ number of variables in addition to those declared by the programs;
+ with the aid of these additional variables, the parameter linkage
+ operations can be simulated by pure substitution. The
+ applicability of the model to the problems of proving program
+ correctness and equivalence is demonstrated by means of examples.",
+ paper = "Abda74a.pdf",
+ keywords = "printed"
+}
+
+@phdthesis{Abda74b,
+ author = "Abdali, S. Kamal",
+ title = {{A Combinatory Logic Model of Programming Languages}},
+ school = "University of Wisconsin",
+ year = "1974",
+ abstract =
+ "A simple correspondence is presented between a large subset of the
+ ALGOL 60 language and the combinatory logic. With the aid of this
+ correspondence, a program can be translated into a single combinatory
+ object. The combinatory object representing a program is specified,
+ in general, by means of a system of reduction relations among the
+ representations of the program constituents. This object denotes, in
+ terms of the combinatory logic, the function that the program is
+ intended to compute.
+
+ The model has been derived by using intuitive, functional
+ interpretations of the constructs of programming languages, completely
+ avoiding the notions of machine command and address. In particular,
+ the concepts of program variable, assignment, and procedure have been
+ accounted for in terms of the concepts of mathematical variable,
+ substitution, and function, respectively.
+
+ Highlevel programming language features are represented in the
+ combinatory logic directly, not in terms of the representations of
+ machinelevel operations. Inputoutput is treated in such a
+ manner that when the representation of a program is applied to the
+ representations of the input items, the resulting combination reduces
+ to a tuple of the representations of the output items.
+
+ The applicability of the model to the problems of
+ proving program equivalence and correctness is illustrated
+ by means of examples.",
+ paper = "Abda74b.pdf"
+}
+
+@techreport{Abda81,
+ author = "Abdali, S. Kamal and Winkler, Franz",
+ title = {{A LambdaCalculus Model for Generating Verification Conditions}},
+ type = "technical report",
+ institution = "Rensselaer Polytechnic Institute",
+ number = "CS8104",
+ year = "1981",
+ abstract =
+ "A lambdacalculusbased method is developed for the automatic
+ generation of verification conditions. A programming language is
+ specified in which inductive assertions associated with a program
+ are incorporated within the body of the program by means of assert
+ and maintainwhile statements. This programming language includes
+ the following features: assignments, conditionals, loops,
+ compounds, ALGOLtype block structure. A model is developed which
+ consists of rules to translate each statement in this programming
+ language into the lambacalculus. The model is such that the
+ lambdaexpression translation of any program reduces to a list
+ (tuple) of lambdaexpression representations of all verification
+ conditions of the program. A proof of this property is given.",
+ paper = "Abda81.pdf",
+ keywords = "printed"
+}
+
+@article{Abra00,
+ author = "Abramov, S.A.",
+ title = {{A Note on the Number of Division Steps in the Euclidean
+ Algorithm}},
+ journal = "ACM SIGSAM",
+ volume = "34",
+ number = "4",
+ year = "2000",
+ paper = "Abra00.pdf",
+ keywords = "printed"
+}
+
@article{Abra95,
author = "Abrams, Marshall D. and Zelkowitz, Marvin V.",
title = {{Striving for Correctness}},
@@ 9676,6 +9844,35 @@ paper = "Brea89.pdf"
isbn = "0521607647"
}
+@inbook{Aptx99,
+ author = "Apt, Krysztof R. and Bezem, Marc",
+ title = {{Formulas as Programs}},
+ booktitle = "The Logic Programming Paradigm",
+ year = "1999",
+ publisher = "Springer Berlin Heidelberg",
+ pages = "75107",
+ isbn = "9783642600852",
+ abstract =
+ "We provide here a computational interpretation of firstorder
+ logic based on a constructive interpretation of satisfiability
+ w.r.t. a fixed but arbitrary interpretation. In this approach the
+ formulas themselves are programs. This contrasts with the
+ socalled formulas as types approach in which the proofs of the
+ formulas are typed terms that can be taken as programs. This view
+ of computing is inspired by logic programming and constraint logic
+ programming but differs from them in a number of crucial aspects.
+
+ Formulas as programs is argued to yield a realistic approach to
+ programming that has been realized in the implemented programming
+ language Alma0 Apt, Brunekreef, Partington and Schaerf (1998)
+ that combines the advantages of imperative and logic
+ programming. The work here reported can also be used to reason
+ about the correctness of nonrecursive Alma0 programs that do not
+ include destructive assignment.",
+ paper = "Aptx99.pdf",
+ keywords = "printed"
+}
+
@incollection{Aspi05,
author = "Aspinall, David and Hofmann, Martin",
title = {{Dependent Types}},
@@ 9688,6 +9885,32 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@misc{Atke18,
+ author = "Atkey, Robert",
+ title = {{Parameterised Notions of Computation}},
+ link = "\url{https://bentnib.org/paramnotionsjfp.pdf}",
+ year = "2018",
+ abstract =
+ "Moggi’s Computational Monads and Power et al ’s equivalent notion of
+ Freyd category have captured a large range of computational effects
+ present in programming languages. Examples include nontermination,
+ nondeterminism, exceptions, continuations, sideeffects and
+ input/output. We present generalisations of both computational monads
+ and Freyd categories, which we call parameterised monads and
+ parameterised Freyd categories, that also capture computational
+ effects with parameters. Examples of such are composable
+ continuations, sideeffects where the type of the state varies and
+ input/output where the range of inputs and outputs varies. By also
+ considering structured parameterisation, we extend the range of
+ effects to cover separated sideeffects and multiple independent
+ streams of I/O. We also present two typed $\lambda$calculi that
+ soundly and completely model our categorical definitions — with and
+ without symmetric monoidal parameterisation — and act as prototypical
+ languages with parameterised effects.",
+ paper = "Atke18.pdf",
+ keywords = "printed"
+}
+
@article{Avig18a,
author = "Avigad, Jeremy",
title = {{The Mechanization of Mathematics}},
@@ 9727,6 +9950,53 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@article{Bail11,
+ author = "Bailey, David H. and Borwein, Jonathan M.",
+ title = {{Highprecision Numerical Integration: Progress and Challenges}},
+ journal = "J. Symbolic Computation",
+ number = "46",
+ pages = "741754",
+ year = "2011",
+ abstract =
+ "One of the most fruitful advances in the field of experimental
+ mathematics has been the development of practical methods for very
+ highprecision numerical integration, a quest initiated by Keith
+ Geddes and other researchers in the 1980s and 1990s.These
+ techniques, when coupled with equally powerful integer relation
+ detection methods, have resulted in the analytic evaluation of many
+ integrals that previously were beyond the realm of symbolic
+ techniques.This paper presents a survey of the current stateoftheart
+ in this area (including results by the present authors and others),
+ mentions some new results, and then sketches what challenges lie
+ ahead.",
+ paper = "Bail11.pdf"
+}
+
+@article{Bail14,
+ author = "Bailey, David H. and Borwein, Jonathan M. and
+ Kaiser, Alexander D.",
+ title = {{Automated Simplification of Large Symbolic Expressions}},
+ journal = "J. Symbolic Computation",
+ volume = "60",
+ pages = "120136",
+ year = "2014",
+ abstract =
+ "We present a set of algorithms for automated simplification of
+ symbolic constants of the form
+ $\sum_i\alpha_i x_i$ with $\alpha_i$ rational and $x_i$
+ complex. The included algorithms, called SimplifySum and
+ implemented in Mathematica , remove redundant terms, attempt to make
+ terms and the full expression real, and remove terms using repeated
+ application of the multipair PSLQ integer relation detection
+ algorithm. Also included are facilities for making substitutions
+ according to userspecified identities. We illustrate this toolset by
+ giving some realworld examples of its usage, including one, for
+ instance, where the tool reduced a symbolic expression of
+ approximately 100 000 characters in size enough to enable manual
+ manipulation to one with just four simple terms.",
+ paper = "Bail14.pdf"
+}
+
@article{Bals91,
author = "Balsters, Herman and Fokkinga, Maarten M.",
title = {{Subtyping can have a simple semantics}},
@@ 9820,6 +10090,23 @@ paper = "Brea89.pdf"
isbn = "9780521766142"
}
+@article{Barn08,
+ author = "Barnett, Michael P.",
+ title = {{Reasoning in Symbolic Computation}},
+ journal = "ACM Communications in Symbolic Algebra",
+ volume = "42",
+ number = "1",
+ year = "2008",
+ abstract =
+ "I discuss notations for some styles of mathematical reasoning that
+ include analogy. These notations extend the conventions of the
+ mathematica package mathscape that I reported recently in the
+ Journal of Symbolic Computation. The paper introduces the reasoning
+ objects that I call 'precursors' and 'consequences lists'.",
+ paper = "Barn08.pdf",
+ keywords = "printed"
+}
+
@techreport{Barr96a,
author = "Barras, Bruno",
title = {{Coq en Coq}},
@@ 9899,6 +10186,17 @@ paper = "Brea89.pdf"
isbn = "3540121730"
}
+@article{Bees80a,
+ author = "Beeson, Michael",
+ title = {{Formalizing Constructive Mathematics: Why and How?}},
+ journal = "Lecture Notes in Mathematics",
+ volume = "873",
+ pages = "146190",
+ year = "1980",
+ paper = "Bees80a.pdf",
+ keywords = "printed"
+}
+
@misc{Beni95,
author = "Benini, Marco",
title = {{Barendregt's $\lambda$Cube in Isabelle}},
@@ 10028,6 +10326,26 @@ paper = "Brea89.pdf"
paper = "Broo87a.pdf"
}
+@article{Buch02,
+ author = "Buchberger, Bruno",
+ title = {{Computer Algebra: The End of Mathematics?}},
+ journal = "ACM SIGSAM",
+ volume = "36",
+ number = "1",
+ year = "2002",
+ abstract =
+ "Mathematical software systems, such as Mathematica, Maple, Derive,
+ and so on, are substantially based on enormous advances in the area of
+ mathematics known as Computer Algebra or Symbolic Mathematics. In
+ fact, everything taught in high school and in the first semesters of a
+ university mathematical education, is available in these systems 'at
+ the touch of the button'. Will mathematics become unnecessary because
+ of this? In the three sections of this essay, I answer this question
+ for nonmathematicians, for mathematicians and for (future) students
+ of mathematics.",
+ paper = "Buch02.pdf"
+}
+
@misc{Byte79,
author = "Byte Publications",
title = {{LISP}},
@@ 10514,6 +10832,14 @@ paper = "Brea89.pdf"
pages = "175220"
}
+@misc{Daly06a,
+ author = "Daly, Timothy",
+ title = {{Literate Programming}},
+ link = "\url{http://lambdatheultimate.org/node/1336}",
+ year = "2006",
+ keywords = "axiomref, TPDref"
+}
+
@misc{Daly18,
author = "Daly, Timothy",
title = {{Proving Axiom Sane: Survey of CAS and Proof Cooperation}},
@@ 10546,6 +10872,30 @@ paper = "Brea89.pdf"
paper = "Darg07.pdf"
}
+@article{Davi01,
+ author = "Davies, Rowan and Pfenning, Frank",
+ title = {{A Modal Analysis of Staged Computation}},
+ journal = "J. ACM",
+ volume = "48",
+ number = "3",
+ pages = "555604",
+ year = "2001",
+ abstract =
+ "We show that a type system based on the intuitionistic modal logic S4
+ provides an expressive framework for specifying and analyzing
+ computation stages in the context of typed $\lambda$calculi and
+ functional languages. We directly demonstrate the sense in which our
+ $\lambda_e^{\rightarrow\Box}$calculus captures staging, and also give
+ a conservative embedding of Nielson and Nielson's twolevel functional
+ language in our functional language MiniML${}^\Box$, thus proving that
+ bindingtime correctness is equivalent to modal correctness on this
+ fragment. In addition, MiniML${}^\Box$ can also express immediate
+ evaluation and sharing of code across multiple stages, thus supporting
+ runtime code generation as well as partial evaluation.",
+ paper = "Davi01.pdf",
+ keywords = "printed"
+}
+
@phdthesis{Davi09,
author = "Davis, Jared Curran",
title = {{A SelfVerifying Theorem Prover}},
@@ 10598,6 +10948,7 @@ paper = "Brea89.pdf"
number = "2",
pages = "117183",
year = "2015",
+ link = "\url{https://www.cl.cam.ac.uk/~mom22/jitawa/}",
abstract =
"This paper presents, we believe, the most comprehensive evidence of a
theorem prover’s soundness to date. Our subject is the Milawa theorem
@@ 10658,6 +11009,52 @@ paper = "Brea89.pdf"
keywords = "printed, axiomref"
}
+@article{Ders87,
+ author = "Dershowitz, Nachum",
+ title = {{Termination of Rewriting}},
+ journal = "J. Symbolic Computation",
+ volume = "3",
+ year = "1987",
+ pages = "69116",
+ abstract =
+ "This survey describes methods for proving that systems of rewrite
+ rules are terminating programs. We illustrate the use in termination
+ proofs of various kinds of orderings on terms, including polynomial
+ interpretations and path orderings. The effect of restrictions, such
+ as linearity, on the form of rules is also considered. In general,
+ however, termination is an undeeidable property of rewrite systems.",
+ paper = "Ders87.pdf",
+ keywords = "printed"
+}
+
+@techreport{Dick88,
+ author = "Dick, A.J.J.",
+ title = {{Automated Equational Reasoning and the KnuthBendix Algorithm:
+ An Informal Introduction}},
+ year = "1988",
+ type = "technical report",
+ institution = "Rutherford Appelton Laboratory",
+ number = "RAL88043",
+ paper = "Dick88.pdf",
+ keywords = "printed"
+}
+
+@article{Dick91,
+ author = "Dick, Jeremy",
+ title = {{An Introduction to KnuthBendix Completion}},
+ journal = "The Computer Journal",
+ volume = "34",
+ number = "1",
+ year = "1991",
+ abstract =
+ "An informal introduction is given to the underlying concepts of
+ term rewriting. Topics covered are KnuthBendix completion,
+ completion modulo equations, unfailing completion and theorem
+ proving by completion.",
+ paper = "Dick91.pdf",
+ keywords = "printed"
+}
+
@misc{Dijk71,
author = "Dijkstra, E.W.",
title = {{A Short Introduction to the Art of Programming}},
@@ 10675,6 +11072,27 @@ paper = "Brea89.pdf"
pages = "182"
}
+@article{Dijk75,
+ author = "Dijkstra, Edsgar W.",
+ title = {{Guarded Commands, Nondeterminancy and Formal Derivation
+ of Programs}},
+ journal = "Comm. of the ACM",
+ volume = "18",
+ number = "8",
+ year = "1975",
+ pages = "453457",
+ abstract =
+ "Socalled 'guarded commands' are introduced as a building block
+ for alternative and repetitive constructs that allow
+ nondeterministic program components for which at least the
+ activity evoked, but possibly even the final state, is not
+ necessarily uniquly determined by the initial state. For the
+ formal derivation of programs expressed in terms of these
+ constructs, a calculus will be shown.",
+ paper = "Dijk75.pdf",
+ keywords = "printed"
+}
+
@phdthesis{Dola16,
author = "Dolan, Stephen",
title = {{Algebraic Subtyping}},
@@ 10849,6 +11267,45 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@article{Emde76,
+ author = "van Emden, M.H. and Kowalski, R.A.",
+ title = {{The Semantics of Predicate Logic as a Programming Language}},
+ journal = "J. Association for Computing Machinery",
+ volume = "23",
+ number = "4",
+ year = "1976",
+ pages = "733742",
+ abstract =
+ "Sentences in firstorder predicate logic can be usefully interpreted
+ as programs In this paper the operational and fixpomt semantics of
+ predicate logic programs are defined, and the connections with the
+ proof theory and model theory of logic are investigated It is
+ concluded that operational semantics is a part of proof theory and
+ that fixpolnt semantics is a special case of modeltheoret:c
+ semantics.",
+ paper = "Emde76.pdf",
+ keywords = "printed"
+}
+
+@article{Engl14c,
+ author = "England, M. and ChebTerrab, E. and Bradford, R. and
+ Davenport, J.H. and Wilson, D.",
+ title = {{Branch Cuts in MAPLE 17}},
+ journal = "ACM Comm. in Computer Algebra",
+ volume = "48",
+ number = "1",
+ year = "2014",
+ abstract =
+ "Accurate and comprehensible knowledge about the position of branch
+ cuts is essential for correctly working with multivalued functions,
+ such as the square root and logarithm. We discuss the new tools in
+ Maple 17 for calculating and visualising the branch cuts of such
+ functions, and others built up from them. The cuts are described in an
+ intuitive and accurate form, offering substantial improvement on the
+ descriptions previously available.",
+ paper = "Engl14c.pdf"
+}
+
@book{Espa17,
author = "Esparza, Javier",
title = {{Automata Theory: An Algorithmic Approach}},
@@ 10858,6 +11315,31 @@ paper = "Brea89.pdf"
paper = "Espa17.pdf"
}
+@article{Esse00,
+ author = "Essex, Christopher and Davison, Matt and Schulzky, Christian",
+ title = {{Numerical Monsters}},
+ journal = "ACM SIGSAM",
+ volume = "34",
+ number = "4",
+ year = "2000",
+ abstract =
+ "When the results of certain computer calculations are shown to be not
+ simply incorrect but dramatically incorrect, we have a powerful reason
+ to be cautious about all computerbased calculations. In this paper we
+ present a 'Rogue's Gallery' of simple calculations whose correct
+ solutions are obvious to humans but whose numerical solutions are
+ incorrect in pathological ways. We call these calculations, which can
+ be guaranteed to wreak numerical mayhem across both software
+ packages and hardware platforms, 'Numerical Monsters'. Our monsters
+ can be used to provide deep insights into how computer calculations
+ fail, and we use t h e m to engender appreciation for the subject of
+ numerical analysis in our students. Although these monsters are based
+ on wellunderstood numerical pathologies, even experienced numerical
+ analysts will find surprises in their behaviour and ,can use the
+ lessons they bring to become even better masters of their tools.",
+ paper = "Esse00.pdf"
+}
+
@article{Farm95b,
author = "Farmer, William M.",
title = {{Reasoning about Partial Functions with the Aid of a
@@ 11052,6 +11534,41 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@article{Fate14a,
+ author = "Fateman, Richard",
+ title = {{Algorithm Differentiation in Lisp: ADIL}},
+ journal = "ACM Comm. in Computer Algebra",
+ volume = "48",
+ number = "3",
+ year = "2014",
+ abstract =
+ "Algorithm differentiation (AD) is a technique used to transform a
+ program $F$ computing a numerical function of one argument $F(x)$ into
+ another program $G(p)$ that returns a pair,
+ $\langle F (p), F^\prime(p)\rangle$ where by $F^\prime(p)$
+ we mean the derivative of $F$ with respect to its argument $x$,
+ evaluated at $x = p$. That is, we have a program AD that takes as input
+ a program, and returns another: $G := AD(F)$. Over the years AD
+ programs have been developed to allow $F$ to be expressed in some
+ specialized variant of a popular programming language L (FORTRAN, C,
+ Matlab, Python) and where $G$ is delivered in that language $L$ or some
+ other. Alternatively, executing $F(p)$ is some environment will deliver
+ $\langle F^\prime(p), F(p)\rangle$ directly. AD tools have also
+ been incorporated in computer algebra systems (CAS) such as
+ Maple. A CAS is hardly necessary for the task of writing the AD
+ program, since the main requirement is a set of tools for
+ manipulation of an internal (typically tree) form of a program.
+ In Lisp, a normal program is already in this form and so the AD
+ program in Lisp (ADIL), the target $F$ and the product $G$ can
+ all be expressed compactly in Lisp. In spite of the brevity and
+ extensibility of the ADIL program, we can provide
+ features which are unsupported in other AD programs. In particular,
+ recursive functions are easily accommodated. Our perspective here is
+ to point out that for scientists who write programs in Lisp or any
+ language that can be converted to Lisp, AD is easily at hand.",
+ paper = "Fate14a.pdf"
+}
+
@misc{Fefe95,
author = "Feferman, Solomon",
title = {{Definedness}},
@@ 11352,6 +11869,15 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@misc{Glym15,
+ author = "Glymour, Clark and Serafin, Luke",
+ title = {{Mathematical Metaphysics}},
+ link = "\url{http://shelf1.library.cmu.edu/HSS/2015/a1626190.pdf}",
+ year = "2015",
+ paper = "Glym15.pdf",
+ keywords = "printed"
+}
+
@article{Gont09a,
author = "Gonthier, Georges",
title = {{Software Engineering for Mathematics}},
@@ 11413,6 +11939,17 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@article{Good80,
+ author = "Goodman, Nicolas D.",
+ title = {{Reflections on Bishop's Philosophy of Mathematics}},
+ journal = "Lecture Notes in Mathematics",
+ volume = "873",
+ pages = "135145",
+ year = "1980",
+ paper = "Good80.pdf",
+ keywords = "printed"
+}
+
@article{Gord79,
author = "Gordon, Michael J. and Milner, Arthur j. and
Wadsworth, Christopher P.",
@@ 11699,6 +12236,21 @@ paper = "Brea89.pdf"
paper = "Gutt95.pdf"
}
+@article{Hama14,
+ author = "Hamada, Tatsuyoshi",
+ title = {{MathLibre: Personalizable Computer Environment for
+ Mathematical Research}},
+ volume = "48",
+ number = "3",
+ year = "2014",
+ abstract =
+ "MathLibre is a project to archive free mathematical software and free
+ mathematical documents and offer them on Live Linux system. MathLibre
+ Project is the direct descendant of KNOPPIX/Math Project. It provides
+ a desktop for mathematicians that can be set up easily and quickly.",
+ paper = "Hama14.pdf"
+}
+
@misc{Hamm95,
author = "Hamming, Richard",
title = {{Hamming, 'You and Your Research'}},
@@ 11868,6 +12420,72 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@article{Jenk11,
+ author = "Jenks, Richard D.",
+ title = {{The 2011 Richard D. Jenks Memorial Prize}},
+ journal = "ACM Communications in Computer Algebra",
+ volume = "45",
+ number = "4",
+ year = "2011",
+ abstract =
+ "The 2011 Richard D. Jenks Memorial Prize for Excellence in
+ Software Engineering Applied to Computer Algebra was presented by
+ members of the Prize Selection Committee and its chair, Erich
+ Kaltofen, at ISSAC and SNC in San Jose, CA, on June 9, 2011 to the
+ Maple Project at the University of Waterloo.",
+ paper = "Jenk11.pdf",
+ keywords = "axiomref"
+}
+
+@article{Jenk13,
+ author = "Jenks, Richard D.",
+ title = {{The 2013 Richard D. Jenks Memorial Prize}},
+ journal = "ACM Communications in Computer Algebra",
+ volume = "47",
+ number = "4",
+ year = "2013",
+ abstract =
+ "The 2013 Richard D. Jenks Memorial Prize for Excellence in
+ Software Engineering Applied to Computer Algebra was announced by
+ members of the Prize Selection Committee, Mark Giesbrecht
+ representing its chair Erich Kaltofen, at ISSAC in Boston, MA, on
+ June 28, 2013 to have been awared to Professor William Arthur
+ Stein of the Sage Project at the University of Washington.",
+ paper = "Jenk13.pdf",
+ keywords = "axiomref"
+}
+
+@article{Jenk15,
+ author = "Jenks, Richard D.",
+ title = {{The 2015 Richard D. Jenks Memorial Prize}},
+ journal = "ACM Communications in Computer Algebra",
+ volume = "49",
+ number = "4",
+ year = "2015",
+ abstract =
+ "The 2015 Richard D. Jenks Memorial Prize was awarded on October
+ 30, 2015 at the Fields Institute in Toronto during the Major
+ Thematic Program on Computer Algebra to Professor Victor Shoup for
+ NTL: A Library for doing Number Theory.",
+ paper = "Jenk15.pdf",
+ keywords = "axiomref"
+}
+
+@article{Jenk17,
+ author = "Jenks, Richard D.",
+ title = {{The 2017 Richard D. Jenks Memorial Prize}},
+ journal = "ACM Communications in Computer Algebra",
+ volume = "51",
+ number = "4",
+ year = "2017",
+ abstract =
+ "The 2017 Richard D. Jenks Memorial Prize for Excellence in
+ Software Engineering Applied to Computer Algebra has been awarded
+ to Stephen Wolfram for WolframAlpha and Mathematica.",
+ paper = "Jenk17.pdf",
+ keywords = "axiomref"
+}
+
@article{John96,
author = "Johnson, C.W.",
title = {{Literate Specifications}},
@@ 11997,6 +12615,16 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@book{Kant98,
+ author = "Kant, Immanuel",
+ title = {{The Critique of Pure Reason}},
+ publisher = "Cambridge University Press",
+ year = "1998",
+ isbn = "0521354021",
+ link = "\url{http://strangebeautiful.com/othertexts/kantfirstcritiquecambridge.pdf}",
+ paper = "Kant98.pdf"
+}
+
@article{Keim09,
author = "Keimel, Klaus and Plotkin, Gordon D.",
title = {{Predicate Transformers for Extended Probability and
@@ 12164,6 +12792,28 @@ paper = "Brea89.pdf"
paper = "Koze93.pdf"
}
+@misc{Kralxx,
+ author = "Krall, Andreas",
+ title = {{Implementation Techniques for Prolog}},
+ link = "\url{https://pdfs.semanticscholar.org/fdbf/aa46bf6ab2148595f638fe9afe97033583ee.pdf}",
+ year = "unknown",
+ abstract =
+ "This paper is a short survey about currently used implementation
+ techniques for Prolog. It gives an introduction to unification and
+ resolution in Prolog and presents the memory model and a basic
+ execution model. These models are expanded to the Vienna Abstract
+ Machine (VAM) with its two versions, the VAM${}_{2p}$ and the
+ VAM${}_{1p}$, and the most famous abstract machine, the Warren
+ Abstract Machine (WAM). The continuation passing style model of
+ Prolog, binary Prolog, leands to the BinWAM. Abstract
+ interpretation can be applied to gather information about a
+ program. This information is used in the generation of very
+ specialized machine code and in optimizations like clause indexing
+ and instruction scheduling on each kind of abstract machine.",
+ paper = "Kralxx.pdf",
+ keywords = "printed"
+}
+
@inproceedings{Kran86,
author = "Kranz, David and Kelsey, Richard and Rees, Jonathan and
Hudak, Paul and Philbin, James and Adams, Norman",
@@ 12244,6 +12894,54 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@misc{Lamp03,
+ author = "Lamport, Leslie",
+ title = {{The Future of Computing: Logic or Biology}},
+ link =
+ "\url{https://lamport.azurewebsites.net/pubs/futureofcomputing.pdf}",
+ year = "2003",
+ paper = "Lamp03.pdf",
+ keywords = "printed"
+}
+
+@article{Laza01,
+ author = "Lazard, Daniel",
+ title = {{Solving Systems of Algebraic Equations}},
+ journal = "ACM SIGSAM Bulletin",
+ volume = "35",
+ number = "3",
+ year = "2001",
+ abstract =
+ "Let $f_1,\ldots,f_k$ be $k$ multivariate polynomials which have
+ a finite number of common zeros in the algebraic closure of the ground
+ field, counting the common zeros at infinity. An algorithm is
+ given and proved which reduces the computations of these zeros to
+ the resolution of a single univariate equation whose degree is the
+ number of common zeros. This algorithm gives the whole algebraic
+ and geometric structure of the set of zeros (multiplicities,
+ conjugate zeros,...). When all the polynomials have the same degree,
+ the complexity of this algorithm is polynomial relative to the generic
+ number of solutions.",
+ paper = "Laza01.pdf"
+}
+
+@book{Leec70,
+ author = "Leech, John",
+ title = {{Computational Problems in Abstract Algebra}},
+ publisher = "Pergamon Press",
+ year = "1970",
+ isbn = "080129757",
+ paper = "Leec70.pdf"
+}
+
+@book{Legu76,
+ author = "LeGuin, Ursula K.",
+ title = {{The Left Hand of Darkness}},
+ publisher = "Penguin Random House",
+ year = "1976",
+ isbn = "9781101665398"
+}
+
@techreport{Lero90,
author = "Leroy, Xavier",
title = {{The ZINC Experiment: An Economical Implementation of the
@@ 12446,6 +13144,14 @@ paper = "Brea89.pdf"
paper = "Mart82.pdf"
}
+@misc{Mazu07,
+ author = "Mazur, Barry",
+ title = {{When is One Thing Equal to Some Other Thing?}},
+ link = "\url{http://www.math.harvard.edu/~mazur/preprints/when_is_one.pdf}",
+ year = "2007",
+ paper = "Mazu07.pdf"
+}
+
@article{Mcca60,
author = "McCarthy, John",
title = {{Recursive Functions of Symbolic Expressions and Their
@@ 12598,6 +13304,14 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@misc{Pren16,
+ author = "Prengel, Alex",
+ title = {{MIT axiommath\_v8.14}},
+ link = "\url{http://web.mit.edu/axiommath_v8.14/}",
+ year = "2016",
+ keywords = "axiomref, TPDref"
+}
+
@inproceedings{Mitc84,
author = "Mitchell, John",
title = {{Type Inference and Type Containment}},
@@ 12925,6 +13639,7 @@ paper = "Brea89.pdf"
volume = "6898",
pages = "265280",
year = "2011",
+ link = "\url{https://www.cl.cam.ac.uk/~mom22/jitawa/}",
abstract =
"Theorem provers, such as ACL2, HOL, Isabelle and Coq, rely on the
correctness of runtime systems for programming languages like ML,
@@ 12956,6 +13671,7 @@ paper = "Brea89.pdf"
volume = "7406",
pages = "412417",
year = "2012",
+ link = "\url{https://www.cl.cam.ac.uk/~mom22/jitawa/}",
abstract =
"This paper presents a method which simplifies verification of deeply
embedded functional programs. We present a technique by which
@@ 13091,6 +13807,41 @@ paper = "Brea89.pdf"
paper = "Okas96.pdf"
}
+@phdthesis{Oles82,
+ author = "Oles, Frank Joseph",
+ title = {{A CategoryTheoretic Approach to the Semantics of
+ Programming Languages}},
+ school = "Syracuse University",
+ year = "1982",
+ abstract =
+ "Here we create a framework for handling the semantics of fully
+ typed programming languages with imperative features, higherorder
+ ALGOLlike procedures, block structure, and implicit
+ conversions. Our approach involves introduction of a new family of
+ programming languages, the {\sl coercive typed $\lambda$calculi},
+ denoted by $L$ in the body of the dissertation. By appropriately
+ choosing the linguistic constants (i.e. generators) of $L$, we can
+ view phrases of variants of ALGOL as syntactically sugared phrases
+ of $L$.
+
+ This dissertation breaks into three parts. In the first part,
+ consisting of the first chapter, we supply basic definitions and
+ motivate the idea that functor categories arise naturally in the
+ explanation of block structure and stack discipline. The second
+ part, consisting of the next three chapters, is dedicated to the
+ general theory of the semantics of the coercive typed
+ $\lambda$calculus; the interplay between posets, algebras, and
+ Cartesian closed categories is particularly intense here. The
+ remaining four chapters make up the final part, in which we apply
+ the general theory to give both direct and continuation semantics
+ for desugared variants of ALGOL. To do so, it is necessary to show
+ certain functor categories are Cartesian closed and to describe a
+ category $\Sigma$ of store shapes. An interesting novelty in the
+ presentation of continuation semantics is the view that commands
+ form a procedural, rather than a primitive, phrase type.",
+ paper = "Oles82.pdf"
+}
+
@inproceedings{Oury08,
author = "Oury, Nicolas and Swierstra, Wouter",
title = {{The Power of Pi}},
@@ 13241,6 +13992,28 @@ paper = "Brea89.pdf"
year = "2017"
}
+@article{Pfen01,
+ author = "Pfenning, Frank and Davies, Rowan",
+ title = {{A Judgemental Reconstruction of Modal Logic}},
+ journal = "Mathematical Structures in Computer Science",
+ volume = "11",
+ pages = "511540",
+ year = "2001",
+ abstract =
+ "We reconsider the foundations of modal logic, following MartinLof's
+ methodology of distinguishing judgments from propositions. We give
+ constructive meaning explanations for necessity and possibility which
+ yields a simple and uniform system of natural deduction for
+ intuitionistic modal logic which does not exhibit anomalies found in
+ other proposals. We also give a new presentation of lax logic and nd
+ that the lax modality is already expressible using possibility and
+ necessity. Through a computational interpretation of proofs in modal
+ logic we further obtain a new formulation of Moggi's monadic
+ metalanguage.",
+ paper = "Pfen01.pdf",
+ keywords = "printed"
+}
+
@misc{Pfen04,
author = "Pfenning, Frank",
title = {{Automated Theorem Proving}},
@@ 13525,6 +14298,20 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@article{Reyn93,
+ author = "Reynolds, John C.",
+ title = {{The Discoveries of Continuations}},
+ journal = "Lisp and Symbolic Computation",
+ volume = "6",
+ pages = "233248",
+ year = "1993",
+ abstract =
+ "We give a brief account of the discoveries of continuations and
+ related concepts.",
+ paper = "Reyn93.pdf",
+ keywords = "printed"
+}
+
@book{Robi01,
author = "Robinson, Alan and Voronkov, Andrei",
title = {{Handbook of Automated Reasoning (2 Volumes)}},
@@ 13533,6 +14320,29 @@ paper = "Brea89.pdf"
isbn = "0262182238"
}
+@article{Roch11,
+ author = "Roche, Daniel S.",
+ title = {{Chunky and EqualSpaced Polynomial Multiplication}},
+ journal = "J. Symbolic Computation",
+ volume = "46",
+ pages = "791806",
+ year = "2011",
+ abstract =
+ "Finding the product of two polynomials is an essential and basic
+ problem in computer algebra. While most previous results have
+ focused on the worstcase complexity, we instead employ the
+ technique of adaptive analysis to give an improvement in many
+ ‘‘easy’’ cases. We present two adaptive measures and methods
+ for polynomial multiplication, and also show how to effectively
+ combine them to gain both advantages. One useful feature of these
+ algorithms is that they essentially provide a gradient between
+ existing ‘‘sparse’’ and ‘‘dense’’ methods. We prove that these
+ approaches provide significant improvements in many cases but
+ in the worst case are still comparable to the fastest existing
+ algorithms.",
+ paper = "Roch11.pdf"
+}
+
@phdthesis{Roor00,
author = "Roorda, JanWillem",
title = {{Pure Type Systems for Functional Programming}},
@@ 13565,6 +14375,15 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@book{Rose07,
+ author = "Rosenkranz, Markus",
+ title = {{Gr\"obner Bases in Symbolic Analysis}},
+ publisher = "Walter de Gruyter, Berlin Germany",
+ year = "2007",
+ isbn = "978311.0193237",
+ keywords = "axiomref, TPDref"
+}
+
@book{Royx03,
author = "Roy, Peter Van and Haridi, Seif",
title = {{Concepts, Techniques, and Models of Computer Programming}},
@@ 13669,6 +14488,46 @@ paper = "Brea89.pdf"
paper = "Schm86.pdf"
}
+@article{Scho88,
+ author = "Schonhage, A.",
+ title = {{Probabilistic Computation of Integer Polynomial GCDs}},
+ journal = "J. of Algorithms",
+ volume = "9",
+ pages = "365371",
+ year = "1988",
+ abstract =
+ "We describe a probabilistic algorithm for the computation of the
+ gcd of two univariate integer polynomials of degrees $\le n$ with
+ their $l^1$norms being bounded by $2^h$ and estimate its expected
+ running time by a worstcase bound of
+ $O(n(n+h)^{l+\epsilon(l)})$.",
+ paper = "Scho88.pdf",
+ keywords = "printed"
+}
+
+@article{Scot93,
+ author = "Scott, Dana S.",
+ title = {{A TypeTheoretical Alternative to ISWIM, CUCH, OWHY}},
+ journal = "Theoretical Computer Science",
+ volume = 121,
+ number = "12",
+ year = "1993",
+ pages = "411440",
+ abstract =
+ "The paper (first written in 1969 and circulated privately) concerns
+ the definition, axiomatization, and applications of the hereditarily
+ monotone and continuous functionals generated from the integers and
+ the Booleans (plus “undefined” elements). The system is formulated as
+ a typed system of combinators (or as a typed λcalculus) with a
+ recursion operator (the least fixedpoint operator), and its proof
+ rules are contrasted to a certain extent with those of the untyped
+ λcalculus. For publication (1993), a new preface has been added, and
+ many bibliographical references and comments in footnotes have been
+ appended.",
+ paper = "Scot93.pdf",
+ keywords = "printed"
+}
+
@article{Scot71,
author = "Scott, Dana S. and Strachey, C.",
title = {{Towards a Mathematical Semantics for Computer Languages}},
@@ 13697,6 +14556,21 @@ paper = "Brea89.pdf"
paper = "Scot71.pdf"
}
+@article{Sedj13,
+ author = "Sedjelmaci, Sidi M.",
+ title = {{Fast Parallel GCD Algorithm of Many Integers}},
+ journal = "ACM Comm in Computer Algebra",
+ volume = "47",
+ number = "3",
+ year = "2013",
+ abstract =
+ "We present a new parallel algorithm which computes the GCD of $n$
+ integers of $O(n)$ bits in $O(n/log~n)$ time with
+ $O(n^{2+\epsilon})$ processors, for any $\epsilon > 0$ on CRCW
+ PRAM model.",
+ paper = "Sedj13.pdf"
+}
+
@article{Shie95,
author = "Shieber, Stuart M. and Schabes, Yves and Pereira, Fernando C.N.",
title = {{Principles and Implementation of Deductive Parsing}},
@@ 13720,6 +14594,14 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@book{Shan94,
+ author = "Shankar, N.",
+ title = {{Metamathematics, Machines, and Godel's Proof}},
+ publisher = "Cambridge University Press",
+ year = "1994",
+ isbn = "0521585333"
+}
+
@inproceedings{Shie02,
author = "Shields, Mark and Jones, Simon Peyton",
title = {{FirstClass Modules for Haskell}},
@@ 13754,14 +14636,6 @@ paper = "Brea89.pdf"
keywords = "printed"
}
@book{Shan94,
 author = "Shankar, N.",
 title = {{Metamathematics, Machines, and Godel's Proof}},
 publisher = "Cambridge University Press",
 year = "1994",
 isbn = "0521585333"
}

@book{Shoe67,
author = "Shoenfield, Joseph R.",
title = {{Mathematical Logic}},
@@ 13770,6 +14644,47 @@ paper = "Brea89.pdf"
isbn = "1568811357"
}
+@misc{Shul18,
+ author = "Shulman, Michael",
+ title = {{Linear Logic for Constructive Mathematics}},
+ link = "\url{https://arxiv.org/pdf/1805.07518.pdf}",
+ year = "2018",
+ abstract =
+ "We show that numerous distinctive concepts of constructive
+ mathematics arise automatically from an interpretation of 'linear
+ higherorder logic' into intuitionistic higherorder logic via a Chu
+ construction. This includes apartness relations, complemented
+ subsets, antisubgroups and antiideals, strict and nonstrict order
+ pairs, cutvalued metrics, and apartness spaces. We also explain the
+ constructive bifurcation of classical concept s using the choice
+ between multiplicative and additive linear connectives. Linear logic
+ thus systematically 'constructivizes' classical definitions and deals
+ automatically with the resulting bookkeeping, and could potentially
+ be used directly as a basis for constructive mathematics in place
+ of intuitionistic logic.",
+ paper = "Shul18.pdf",
+ keywords = "printed"
+}
+
+@techreport{Smit90,
+ author = "Smith, A.",
+ title = {{The KnuthBendix Completion Algorithm and its Specification in Z}},
+ type = "technical report",
+ institution = "Ministry of Defence, RSRE Malvern WORCS",
+ year = "1990",
+ number = "RSRE Memorandum 4323",
+ abstract =
+ "Proving that something is a consequence of a set of axioms can be
+ very difficult. The KnuthBendix completion algorithm attempts to
+ automate this process when the axioms are equations. The algorithm
+ is bound up in the area of term rewriting, and so this memorandum
+ contains an introduction to the tehory of term rewriting, followed
+ by an overview of the algorithm. Finally a formal specification of
+ the algorithm is given using the language Z.",
+ paper = "Smit90.pdf",
+ keywords = "printed"
+}
+
@misc{Smit15,
author = "Smith, Peter",
title = {{Some Big Books on Mathematical Logic}},
@@ 13798,6 +14713,37 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@article{Sore94,
+ author = "Sorenson, Jonathan",
+ title = {{Two Fast GCD Algorithms}},
+ journal = "Journal of Algorithms",
+ volume = "16",
+ pages = "110144",
+ year = "1994",
+ abstract =
+ "We present two new algorithms for computing geatest common
+ divisors: the right and leftshift $k$ary GCD algorithms. These
+ algorithms are generalizations of the binary and leftshift binary
+ algorithms. Interestingly, both new algorithms have sequential
+ versions that are practical and efficient and parallel versions
+ that rival the best previous parallel GCD algorithms. We show that
+ sequential versions of both algorithms take $O(n^2/log~n)$ bit
+ operations in the worst case to compute the GCD of two nbit
+ integers. This compares favorably to the Euclidean and moth
+ precision versions of these GCD algorithms, and we found that both
+ $k$ary algorithms are faster than the Euclidean and binary
+ algorithms on inputs of 100 to 1000 decimal digits in length. We
+ show that parallel versions of both algorithms match the
+ complexity of the best previous parallel GCD algorithm due to Chor
+ and Goldreich. Specifically, if $log~n\le k \le 2^n$ and $k$ is a
+ power of two, then both algorithms run in $O(n/log~n+log^2~n)$
+ time using a number of processors bounded by a polynomial in $n$
+ and $k$ on a common CRCW PRAM. We also discuss extended versions
+ of both algorithms.",
+ paper = "Sore94.pdf",
+ keywords = "printed"
+}
+
@techreport{Stee78,
author = "Steele, Guy Lewis",
title = {{RABBIT: A Compiler for SCHEME}},
@@ 13859,8 +14805,8 @@ paper = "Brea89.pdf"
number = "AI Memo No. 453",
year = "1978",
abstract =
 "We examine the effes of various language design decisions on the
 programming styles available to a user of the language, with
+ "We examine the effects of various language design decisions on
+ the programming styles available to a user of the language, with
particular emphasis on the ability to incrementatlly construct
modular systems. At each step we exhibit an interactive
metacircular interpreter for the language under
@@ 13883,6 +14829,67 @@ paper = "Brea89.pdf"
actual evolution of LISP."
}
+@article{Stou11,
+ author = "Stoutemyer, David R.",
+ title = {{Ways to Implement Computer Algebra Compactly}},
+ journal = "ACM Comm. in Computer Algebra",
+ volume = "45",
+ number = "4",
+ year = "2011",
+ abstract =
+ "Computer algebra had to be implemented compactly to fit on early
+ personal computers and handheld calculators. Compact implementation
+ is still important for portable handheld devices. Also, compact
+ implementation increases comprehensibility while decreasing develop
+ ment and maintenance time and cost, regardless of the platform. This
+ article describes several ways to achieve compact implementations,
+ including:
+ \begin{itemize}
+ \item Exploit evaluation followed by interpolation to avoid
+ implementing a parser, such as in PicoMath
+ \item Use contiguous storage as an expression stack to avoid garbage
+ collection and pointerspace overhead, such as in Calculus Demon
+ and TIMathEngine
+ \item Use various techniques for saving code space for linkedstorage
+ representation of expressions and functions, such as muMath and Derive
+ \end{itemize}",
+ paper = "Stou11.pdf",
+ keywords = "axiomref"
+}
+
+@article{Stou11a,
+ author = "Stoutemyer, David R.",
+ title = {{Ten Commandments for Good Default Expression Simplification}},
+ journal = "J. Symbolic Computation",
+ volume = "46",
+ pages = "859887",
+ year = "2011",
+ abstract =
+ "This article provides goals for the design and improvement of default
+ computer algebra expression simplification. These goals can also help
+ users recognize and partially circumvent some limitations of their
+ current computer algebra systems. Although motivated by computer
+ algebra, many of the goals are also applicable to manual
+ simplification, indicating what transformations are necessary and
+ sufficient for good simplification when no particular canonical result
+ form is required.
+
+ After motivating the ten goals, the article then explains how the
+ Altran partially factored form for rational expressions was extended
+ for Derive and for the computer algebra in Texas Instruments products
+ to help fulfill these goals. In contrast to the distributed Altran
+ representation, this recursive partially factored semifraction form:
+ \begin{itemize}
+ \item does not unnecessarily force common denominators
+ \item discovers and preserves significantly more factors
+ \item can represent general expressions
+ \item can produce an entire spectrum from fully factored over a
+ common denominator through complete multivariate partial fractions,
+ including a dense subset of all intermediate forms.
+ \end{itemize}",
+ paper = "Stou11a.pdf"
+}
+
@article{Stou12,
author = "Stoutemyer, David R.",
title = {{Series Crimes}},
@@ 13925,6 +14932,49 @@ paper = "Brea89.pdf"
paper = "Stou12.pdf"
}
+@article{Stou13,
+ author = "Stoutemyer, David R.",
+ title = {{A Computer Algebra User Interface Manifesto}},
+ journal = "ACM Communications in Computer Algebra",
+ volume = "47",
+ number = "4",
+ year = "2013",
+ abstract =
+ "Many computer algebra systems have more than 1000 builtin functions,
+ making expertise difficult. Using mock dialog boxes, this article
+ describes a proposed interactive generalpurpose wizard for organizing
+ optional transformations and allowing easy fine grain control over the
+ form of the result – even by amateurs. This wizard integrates ideas
+ including:
+ \begin{itemize}
+ \item flexible subexpression selection;
+ \item complete control over the ordering of variables and
+ commutative operands, with wellchosen defaults;
+ \item interleaving the choice of successively less main
+ variables with applicable function choices to provide detailed
+ control without incurring a combinatorial number of applicable
+ alternatives at any one level;
+ \item quick applicability tests to reduce the listing of
+ inapplicable transformations;
+ \item using an organizing principle to order the alternatives
+ in a helpful manner;
+ \item labeling quicklycomputed alternatives in dialog boxes
+ with a preview of their results, using ellipsis elisions if
+ necessary or helpful;
+ \item allowing the user to retreat from a sequence of choices
+ to explore other branches of the tree of alternatives – or to
+ return quickly to branches already visited;
+ \item allowing the user to accumulate more than one of the
+ alternative forms;
+ \item integrating direct manipulation into the wizard; and
+ \item supporting not only the usual inputresult pair mode, but
+ also the useful alternative derivational and in situ replacement
+ modes in a unified window.
+ \end{itemize}",
+ paper = "Stou13.pdf",
+ kryeotfd = "printed"
+}p
+
@article{Stuc05,
author = "Stuckey, Peter J. and Sulzmann, Martin",
title = {{A Theory of Overloading}},
@@ 14021,6 +15071,17 @@ paper = "Brea89.pdf"
isbn = "139780486284620"
}
+@article{Tars69,
+ author = "Tarski, Alfred",
+ title = {{Truth and Proof}},
+ journal = "Scientific American",
+ volume = "1969",
+ pages = "6377",
+ year = "1969",
+ paper = "Tars69.pdf",
+ keywords = "printed"
+}
+
@misc{Tobi11,
author = "TobinHochstadt, Sam and Felleisen, Matthias",
title = {{The Design and Implementation of Typed Scheme: From
@@ 14244,6 +15305,30 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@article{Webe05a,
+ author = "Weber, Kenneth and Trevisan, Vilmar and Martins, Luiz Felipe",
+ title = {{A Modular Integer GCD Algorithm}},
+ journal = "J. of Algorithms",
+ volume = "54",
+ year = "2005",
+ pages = "152167",
+ abstract =
+ "This paper describes the first algorithm to compute the greatest
+ common divisor (GCD) of two $n$bit integers using a modular
+ representation for intermediate values $U$, $V$ and also for the
+ result. It is based on a reduction step, similar to one used in
+ the accelerated algorithm when $U$ and $V$ are close to the same
+ size, that replaces $U$ by $(UbV)/p$, where $p$ is one of the
+ prime moduli and $b$ is the unique integer in the interval
+ $(p/2,p/2)$ such that $b\equiv UV^{1} (mod~p)$. When the
+ algorithm is executed on a bit common CRCW PRAM with
+ $O(n~log~n~log~log~log~n)$ processors, it takes $(O(n)$ time in
+ the worst case. A heuristic model of the average case yields
+ $O(n/log~n)$ time on the same number of processors.",
+ paper = "Webe05a.pdf",
+ keywords = "printed"
+}
+
@phdthesis{Wehr05,
author = "Wehr, Stefan",
title = {{ML Modules and Haskell Type Classes: A Constructive
@@ 14569,6 +15654,33 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@article{Zeng11,
+ author = "Zengler, Christoph and Kubler, Andreas and Kuchlin, Wolfgang",
+ title = {{New Approaches to Boolean Quantifier Elimination}},
+ journal = "ACM Comm. in Computer Algebra",
+ volume = "45",
+ number = "2",
+ year = "2011",
+ abstract =
+ "We present four different approaches for existential Boolean
+ quantifier elimination, based on model enumeration, resolution,
+ knowledge compilation with projection, and substitution. We point out
+ possible applications in the area of verification and we present
+ preliminary benchmark results of the different approaches.",
+ paper = "Zeng11.pdf",
+ keywords = "printed"
+}
+
+@misc{Zhan02,
+ author = "Zhang, Ting",
+ title = {{A Survey of Quantifier Elimination: Syntactic and Semantic
+ Approaches}},
+ year = "2002",
+ link = "\url{http://theory.stanford.edu/~tingz/talks/qe.ps}",
+ paper = "Zhan02.pdf",
+ keywords = "printed"
+}
+
@incollection{Soze06,
author = "Sozeau, Matthieu",
title = {{Subset Coercions in Coq}},
@@ 21884,6 +22996,28 @@ paper = "Brea89.pdf"
paper = "Krag09.pdf"
}
+@article{Lich11,
+ author = "Lichtblau, Daniel",
+ title = {{Symbolic Definite (and Indefinite) Integration: Methods and
+ Open Issues}},
+ journal = "ACM Comm. in Computer Algebra",
+ volume = "45",
+ number = "1",
+ year = "2011",
+ link = "\url{http://www.sigsam.org/bulletin/articles/175/issue175.pdf}",
+ abstract = "
+ The computation of definite integrals presents one with a variety of
+ choices. There are various methods such as NewtonLeibniz or Slater's
+ convolution method. There are questions such as whether to split or
+ merge sums, how to search for singularities on the path of
+ integration, when to issue conditional results, how to assess
+ (possibly conditional) convergence, and more. These various
+ considerations moreover interact with one another in a multitude of
+ ways. Herein we discuss these various issues and illustrate
+ with examples.",
+ paper = "Lich11.pdf"
+}
+
@article{Liou1833a,
author = "Liouville, Joseph",
title = {{Premier m\'{e}moire sur la d\'{e}termination des int\'{e}grales
@@ 25842,6 +26976,25 @@ paper = "Brea89.pdf"
paper = "Hong12.pdf"
}
+@article{Huan14,
+ author = "Huang, Zongyan and England, Matthew and Wilson, David and
+ Davenport, James H. and Paulson, Lawrence C.",
+ title = {{A Comparison of Three Heuristics to Choose the Variable
+ Ordering for Cylindrical Algebraic Decomposition}},
+ journal = "ACM Comm. in Computer Algebra",
+ volume = "48",
+ number = "3",
+ year = "2014",
+ abstraact =
+ "Cylindrical algebraic decomposition (CAD) is a key tool for problems
+ in real algebraic geometry and beyond. When using CAD there is often a
+ choice over the variable ordering to use, with some problems
+ infeasible in one ordering but simple in another. Here we discuss a
+ recent experiment comparing three heuristics for making this choice on
+ thousands of examples.",
+ paper = "Huan14.pdf"
+}
+
@misc{Jova12,
author = "Jovanovic, Dejan and de Moura, Leonardo",
title = {{Solving NonLinear Arithmetic}},
@@ 26946,6 +28099,35 @@ paper = "Brea89.pdf"
year = "1989"
}
+@article{Bozm84,
+ author = "Bozman, Gerald and Buco, William and Daly, Timothy and
+ Tetzlaff, William",
+ title = {{Analysis of Free Storage Algorithms  Revisited}},
+ journal = "IBM Systems Journal",
+ volume = "23",
+ number = "1",
+ year = "1984",
+ abstract =
+ "Most research in freestorage management has centered around
+ strategies that search a linked list and strategies that partition
+ storage into predetermined sizes. Such algorithms are analyzed in
+ terms of CPU efficiency and storage efficiency. The subject of this
+ study is the freestorage management in the Virtual Machine/System
+ Product (VM/SP) system control program. As a part of this study,
+ simulations were done of established, and proposed, dynamic storage
+ algorithms for the VM/SP operating system. Empirical evidence is given
+ that simplifying statistical assumptions about the distribution of
+ interarrival times and holding times has high predictive
+ ability. Algorithms such as firstfit, modified firstfit, and
+ bestfit are found to be CPUinefficient. Buddy systems are found to
+ be very fast but suffer from a high degree of internal
+ fragmentation. A form of extended subpooling is shown to be as fast as
+ buddy systems with improved storage efficiency. This algorithm was
+ implemented for VM/SP, and then measured. Results for this algorithm
+ are given for several production VM/SP systems.",
+ paper = "Bozm84.pdf"
+}
+
@article{Calm92,
author = "Calmet, J. and Campbell, J.A.",
title = {{Artificial Intelligence and Symbolic Mathematical
@@ 31230,6 +32412,14 @@ paper = "Brea89.pdf"
beebe = "Daly:2002:AOS"
}
+@misc{Daly03,
+ author = "Daly, Timothy",
+ title = {{Axiom Website: http://axiomdeveloper.org}},
+ link = "\url{http://axiomdeveloper.org}",
+ keywords = "axiomref",
+ year = "2003"
+}
+
@misc{Daly05,
author = "Daly, Timothy",
title = {{LispNYC Presentation at Trinity}},
@@ 35454,7 +36644,7 @@ paper = "Brea89.pdf"
covered in the survey, but different in many ways as well. Axiom,
Maxima, and SAGE, are the largest of the generalpurpose opensource
CASs.",
 keywords = "axiomref",
+ keywords = "axiomref, TPDref",
beebe = "Joyner:2008:OSC"
}
@@ 35508,6 +36698,36 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@inproceedings{Kand89,
+ author = "KandriRody, Abdelilah and Kapur, Deepak and Winkler, Franz",
+ title = {{KnuthBendix Procedure and Buchberger Algorithm  A Synthesis}},
+ booktitle = "ISSAC'89",
+ publisher = "ACM Press",
+ pages = "5567",
+ year = "1989",
+ isbn = "0897913256",
+ abstract =
+ "The KnuthBendix procedure for the completion of a rewrite rule
+ system and the Buchberger algorithm for computing a Groebner basis
+ of a polynomial ideal are very similar in two respects: they both
+ start wtih an arbitrary specification of an algebraic structure
+ (axioms for an equational theory and a basis for a polynomial
+ ideal, respectively) which is transformed to a very special
+ specification of this algebraic structure (a complete rewrite rule
+ system and a Groebner basis of the polynomial ideal, respectively).
+ This special specification allows to decide many problems concerning
+ the given algebraic structure. Moreover, both algorithms achieve
+ their goals by employing the same basic concepts: formation of
+ critical pairs and completion.
+
+ Although the two methods are obviously related, the exact nature
+ of this relation remains to be clarified. Based on previous work
+ we show how the KnuthBendix procedure and the Buchberger algorithm
+ can be seen as special cases of a more general completion procedure.",
+ paper = "Kand89.pdf",
+ keywords = "printed"
+}
+
@misc{Kani16,
author = "Kanigel, Robert",
title = {{OldQuotes}},
@@ 37752,7 +38972,7 @@ paper = "Brea89.pdf"
This exhibit includes a laptop computer running a recent version
of Axiom, Internet access (if available) to the Axiom Wiki website[4],
and CDs containing Axiom software for free distribution[5].",
 keywords = "axiomref",
+ keywords = "axiomref, TPDref",
beebe = "Page:2007:AOS"
}
@@ 37808,8 +39028,8 @@ paper = "Brea89.pdf"
@InProceedings{Prit06,
author = "Pritchard, F. Leon and Sit, William Y.",
 title = {{On initial value problems for ordinary differentialalgebraic
 equations}},
+ title = {{On Initial Value Problems for Ordinary DifferentialAlgebraic
+ Equations}},
booktitle = "Radon Series on Computational and Applied Mathematics",
year = "2006",
pages = "283340",
@@ 37833,7 +39053,7 @@ paper = "Brea89.pdf"
algebraic index of the system, defined as the number of steps taken
by the process to stabilize. Over and underdetermined systems are
also accommodated in their framework.",
 keywords = "axiomref"
+ keywords = "axiomref, TPDref"
}
@inproceedings{Purt86,
@@ 39253,12 +40473,6 @@ paper = "Brea89.pdf"
beebe = "Sutor:1987:TICa"
}
 author = "R. D. Jenks R. S. Sutor and S. M. Watt",
 title = {{Scratchpad II: An abstract Datatype system for
 mathematical computation}},
 pages = "1237",
 year = "1988"
}
@misc{Swmath,
author = "Unknown",
title = {{Axiom}},
@@ 40132,6 +41346,37 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@inproceedings{Wink85,
+ author = "Winkler, Franz",
+ title = {{Reducing the Complexity of the KnuthBendix Completion
+ Algorithm: A ``Unification'' of Different Approaches}},
+ booktitle = "European Conference on Computer Algebra (EUROCAL 85)",
+ pages = "378389",
+ publisher = "Springer",
+ year = "1985",
+ isbn = "9783540159834",
+ abstract =
+ "The KnuthBendix completion procedure for rewrite rule systems is
+ of wide applicability in symbolic and algebraic computation.
+ Attempts to reduce the complexity of this completion algorithm are
+ reported in the literature. Already in their seminal 1967 paper
+ D.E. Knuth and P.B. Bendix have suggested to keep all the rules
+ iterreduced during the execution of the algorithm. G. Huet has
+ presented a version of the completion algorithm in which every
+ rewrite rule is kept in reduced form with respect to all the other
+ rules in the system. Borrowing an idea of Buchberger's for the
+ completion of bases of polynomial ideals the author has proposed
+ in 1983 a criterion for detecting ``unnecessary'' critical
+ pairs. If a critical pair is recognized as unnecessary then one
+ need not apply the costly process of computing normal forms to
+ it. It has been unclear whether these approaches can be
+ combined. We demonstrate that it is possible to keep all the
+ rewrite rules interreduced and still use a criterion for
+ eliminating unnecessary critical pairs.",
+ paper = "Wink85.pdf",
+ keywords = "printed"
+}
+
@misc{Wink89,
author = "Winkler, Franz",
title = {{Equational Theorem Proving and Rewrite Rule Systems}},
@@ 40166,7 +41411,32 @@ paper = "Brea89.pdf"
We show how rewrite systems can be used for proving theorems in
equational and inductive theories, and how an equational specification
of a problem can be turned into a rewrite program.",
 paper = "Wink89.pdf"
+ paper = "Wink89.pdf",
+ keywords = "printed"
+}
+
+@inbook{Wink90,
+ author = "Winkler, Franz",
+ title = {{Solution of Equations I: Polynomial Ideals and Grobner Bases}},
+ booktitle = "Computers in Mathematics",
+ year = "1990",
+ publisher = "Marcel Dekker, Inc",
+ pages = "383407",
+ isbn = "0824783417",
+ paper = "Wink90.pdf",
+ keywords = "printed"
+}
+
+@misc{Wink93a,
+ author = "Winkler, Franz",
+ title = {{Computer Algebra}},
+ booktitle = "Concise Encyclopedia of Computer Science",
+ year = "1993",
+ publisher = "Wiley",
+ isbn = "0470090952",
+ pages = "227231",
+ paper = "Wink93a.pdf",
+ keywords = "printed"
}
@article{Wink93,
@@ 40174,7 +41444,8 @@ paper = "Brea89.pdf"
title = {{Algebraic Computation in Geometry}},
year = "1993",
journal = "IMACS Symposium SC1993",
 link = "\url{http://www.risc.jku.at/publications/download/risc_3777/paper_35.pdf}",
+ link =
+ "\url{http://www.risc.jku.at/publications/download/risc_3777/paper_35.pdf}",
abstract =
"Computation with algebraic curves and surfaces are very well suited
for being treated with computer algebra. Many aspects of computer
@@ 40188,6 +41459,16 @@ paper = "Brea89.pdf"
paper = "Wink93.pdf"
}
+@inproceedings{Wink95,
+ author = "Winkler, Franz",
+ title = {{Computer Algebra  Problems and Developments}},
+ booktitle = "Computers in Industry 2 (SCAFI'92)",
+ pages = "117",
+ year = "1995",
+ isbn = "9780471955290",
+ paper = "Wink95.pdf"
+}
+
@book{Wink96,
author = "Winkler, Franz",
title = {{Polynomial Algorithms in Computer Algebra}},
@@ 40219,7 +41500,54 @@ paper = "Brea89.pdf"
The book was originally developed from course material. It can easily
be used as a textbook on the topic. Most subsections contain
 exercises. Solutions of some of the exercises are provided."
+ exercises. Solutions of some of the exercises are provided.",
+ keywords = "axiomref"
+}
+
+@techreport{Wink99,
+ author = "Winkler, Franz",
+ title = {{Advances and Problems in Algebraic Computation}},
+ type = "technical report",
+ number = "9949",
+ year = "1999",
+ institution = "RISC, Linz",
+ abstract =
+ "In the last years there has been dramatic progress in all areas
+ of algebraic computation. Many working mathematiians have access
+ to and actually use algebraic software systems for their research
+ No end of this development is in sight. We report on some active
+ topics in algebraic computation, namely the theory of integration
+ and symbolic solution of systems of differential equations, the
+ solution of systems of algebraic equations, the factorization of
+ polynomials, and the design and analysis of algebraic curves and
+ surfaces.",
+ paper = "Wink99.pdf",
+ keywords = "printed"
+}
+
+@inproceedings{Wink06,
+ author = "Winkler, Franz",
+ title = {{Computer Algebra and Geometry  Some Interactions}},
+ booktitle = "Proc. of Coll. on Constructive Algebra and System
+ Theory (CAST)",
+ year = "2006",
+ publisher = "unknown",
+ isbn = "906984477x",
+ pages = "127138",
+ abstract =
+ "Algebraic curves and surfaces have been studied intensively in
+ algebraic geometry for centuries. Thus, there exists a huge amount
+ of theoretical knowledge about these geometric objects. Recently,
+ algebraic curves and surfaces play an important and ever
+ increasing role in computer aided geometric design, computer
+ vision, computer aided manufacturing, coding theory, and
+ cryptography, just to name a few application areas. Consequently,
+ theoretical results need to be adapted to practical needs. We need
+ efficient algorithms for generating, representing, manipulating,
+ analyzing, rendering algebraic curves and surfaces. Exact computer
+ algebraic methods can be employed effectively for dealing with
+ these geometric problems.",
+ paper = "Wink06.pdf"
}
@misc{Wity85,
@@ 41891,7 +43219,8 @@ paper = "Brea89.pdf"
I hope that it will become clear that many operations that are often
regarded as effective, are in fact not so; while many operations that
might not be regarded as effective in fact are.",
 paper = "Dave81b.pdf"
+ paper = "Dave81b.pdf",
+ keywords = "printed"
}
@misc{Dave87,
@@ 43363,7 +44692,8 @@ paper = "Brea89.pdf"
verification framework, the Maple package DifferenceDifferential
developed at our institute to compute bivariate differencedifferential
polynomials using relative Gr ̈obner bases.",
 paper = "Khan13.pdf"
+ paper = "Khan13.pdf",
+ keywords = "printed"
}
@phdthesis{Khan14,
@@ 45190,11 +46520,16 @@ paper = "Brea89.pdf"
keywords = "axiomref, printed"
}
@misc{SCSCP,
+@article{SCSCP,
author = "The SCSCP development team",
title = {{Symbolic Computation Software Composability Protocol}},
+ journal = "Communications in Computer Algebra",
+ volume = "44",
+ number = "4",
link = "\url{https://gappackages.github.io/scscp/}",
 year = "2017"
+ year = "2010",
+ paper = "SCSCP.pdf",
+ keywords = "printed"
}
@book{Segg93,
@@ 45615,16 +46950,6 @@ paper = "Brea89.pdf"
link = "\url{https://en.wikipedia.org/wiki/Levenshtein\_distance}"
}
@misc{Wink95,
 author = "Winkler, Franz",
 title = {{Computer Algebra  Problems and Developments}},
 year = "1995",
 abstract =
 "Recent developments in computer algebra are discussed using simple
 but illustrative examples",
 paper = "Wink95.pdf"
}

@article{Wosx92,
author = "Wos, Larry",
title = {{The Impossibility of the Automation of Logical Reasoning}},
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index afe2005..036457f 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 12506,6 +12506,206 @@ when shown in factored form.
\subsection{A} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Abadi, Martin}
+\index{Cardelli, Luca}
+\index{Curien, PierreLouis}
+\index{Levy, JeanJacques}
+\begin{chunk}{axiom.bib}
+@inproceedings{Abad90,
+ author = "Abadi, Martin and Cardelli, Luca and Curien, PierreLouis
+ and Levy, JeanJacques",
+ title = {{Explicit Substitutions}},
+ booktitle = "Symp. of Principles of Programming Languages",
+ publisher = "ACM",
+ year = "1990",
+ link = "\url{http://www.hpl.hp.com/techreports/CompaqDEC/SRCRR54.pdf}",
+ abstract =
+ "The $lambda\sigma$calculus is a refinement of the
+ $lambda$calculus where substitutions are manipulated
+ explicitly. The $\lambda\sigma$calculus provides a setting for
+ studying the theory of substitutions, with pleasant mathematical
+ properties. It is also a useful bridge between the classical
+ $\lambda$calculus and concrete implementations.",
+ paper = "Abad90.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Abdali, S. Kamal}
+\begin{chunk}{axiom.bib}
+@book{Abda73,
+ author = "Abdali, S. Kamal",
+ title = {{A Simple LambdaCalculus Model of Programming Languages}},
+ isbn = "9781332196029",
+ publisher = "Forgotten Books",
+ year = "1973",
+ abstract =
+ "We present a simple correspondence between a large subset of
+ ALGOL 60 language and lambdacalculus. With the aid of this
+ correspondence, a program can be translated into a single
+ lambdaexpression. In general, the representation of a program is
+ specified by means of a system of simultaneous conversion
+ relations among the representations of the program
+ constituents. Highlevel programming language features are treated
+ directly, not in terms of the representations of machinelevel
+ operations. The model includes inputoutput in such a way that
+ when the representation of a (convergent) program is applied to
+ the input item representations, the resulting combination reduces
+ to a tuple of the representations of the output items. This model
+ does not introduce any imperative notions into the calculus; the
+ descriptive programming constructs, such as expressions, and the
+ imperative ones, such as assignment and jumps, are translated
+ alike into pure lambda expressions. The applicability of the model
+ to the problems of proving program equivalence and correctness is
+ illustrated by means of simple examples.",
+ paper = "Abda73.pdf"
+}
+
+\end{chunk}
+
+\index{Abdali, S. Kamal}
+\begin{chunk}{axiom.bib}
+@article{Abda74,
+ author = "Abdali, S. Kamal",
+ title = {{A LambdaCalculus Model of Programming Languages 
+ I. Simple Constructs}},
+ journal = "J. of Computer Languages",
+ volume = "1",
+ pages = "287301",
+ year = "1974",
+ abstract =
+ "A simple correspondence is presented between the elementary
+ constructs of programming languages and the lambdacalculus. The
+ correspondence is obtained by using intuitive, functional
+ interpretation of programming language constructs, completely
+ avoiding the notions of machine memory and address. In particular,
+ the concepts of program variable and assignments are accounted for
+ in terms of the concepts of mathematical variable and
+ substitution, respectively. Lambdaexpression representations are
+ given of assignments, conditional and compound statements,
+ inputoutput, and blocks. Algol 60 is used as the illustrative
+ language.",
+ paper = "Abda74.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Abdali, S. Kamal}
+\begin{chunk}{axiom.bib}
+@article{Abda74a,
+ author = "Abdali, S. Kamal",
+ title = {{A LambdaCalculus Model of Programming Languages 
+ II. Jumps and Procedures}},
+ journal = "J. of Computer Languages",
+ volume = "1",
+ pages = "303320",
+ year = "1974",
+ abstract =
+ "The correspondence between programming languages and the
+ lambdacalculus presented in Part I of the paper is extended there
+ to include iteration statements, jumps, and procedures. Programs
+ containing loops are represented by lambdaexpressions whose
+ components are specified recursively by means of systems of
+ simultaneous conversion relations. The representation of
+ callbyname and sideeffects in a program is accomplished without
+ any resort to the concepts of memory andaddress by making use of a
+ number of variables in addition to those declared by the programs;
+ with the aid of these additional variables, the parameter linkage
+ operations can be simulated by pure substitution. The
+ applicability of the model to the problems of proving program
+ correctness and equivalence is demonstrated by means of examples.",
+ paper = "Abda74a.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Abdali, S. Kamal}
+\begin{chunk}{axiom.bib}
+@phdthesis{Abda74b,
+ author = "Abdali, S. Kamal",
+ title = {{A Combinatory Logic Model of Programming Languages}},
+ school = "University of Wisconsin",
+ year = "1974",
+ abstract =
+ "A simple correspondence is presented between a large subset of the
+ ALGOL 60 language and the combinatory logic. With the aid of this
+ correspondence, a program can be translated into a single combinatory
+ object. The combinatory object representing a program is specified,
+ in general, by means of a system of reduction relations among the
+ representations of the program constituents. This object denotes, in
+ terms of the combinatory logic, the function that the program is
+ intended to compute.
+
+ The model has been derived by using intuitive, functional
+ interpretations of the constructs of programming languages, completely
+ avoiding the notions of machine command and address. In particular,
+ the concepts of program variable, assignment, and procedure have been
+ accounted for in terms of the concepts of mathematical variable,
+ substitution, and function, respectively.
+
+ Highlevel programming language features are represented in the
+ combinatory logic directly, not in terms of the representations of
+ machinelevel operations. Inputoutput is treated in such a
+ manner that when the representation of a program is applied to the
+ representations of the input items, the resulting combination reduces
+ to a tuple of the representations of the output items.
+
+ The applicability of the model to the problems of
+ proving program equivalence and correctness is illustrated
+ by means of examples.",
+ paper = "Abda74b.pdf"
+}
+
+\end{chunk}
+
+\index{Abdali, S. Kamal}
+\index{Winkler, Franz}
+\begin{chunk}{axiom.bib}
+@techreport{Abda81,
+ author = "Abdali, S. Kamal and Winkler, Franz",
+ title = {{A LambdaCalculus Model for Generating Verification Conditions}},
+ type = "technical report",
+ institution = "Rensselaer Polytechnic Institute",
+ number = "CS8104",
+ year = "1981",
+ abstract =
+ "A lambdacalculusbased method is developed for the automatic
+ generation of verification conditions. A programming language is
+ specified in which inductive assertions associated with a program
+ are incorporated within the body of the program by means of assert
+ and maintainwhile statements. This programming language includes
+ the following features: assignments, conditionals, loops,
+ compounds, ALGOLtype block structure. A model is developed which
+ consists of rules to translate each statement in this programming
+ language into the lambacalculus. The model is such that the
+ lambdaexpression translation of any program reduces to a list
+ (tuple) of lambdaexpression representations of all verification
+ conditions of the program. A proof of this property is given.",
+ paper = "Abda81.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Abramov, S.A.}
+\begin{chunk}{axiom.bib}
+@article{Abra00,
+ author = "Abramov, S.A.",
+ title = {{A Note on the Number of Division Steps in the Euclidean
+ Algorithm}},
+ journal = "ACM SIGSAM",
+ volume = "34",
+ number = "4",
+ year = "2000",
+ paper = "Abra00.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Abrams, Marshall D.}
\index{Zelkowitz, Marvin V.}
\begin{chunk}{axiom.bib}
@@ 12803,6 +13003,40 @@ when shown in factored form.
\end{chunk}
+\index{Apt, Krysztof R.}
+\index{Bezem, Marc}
+\begin{chunk}{axiom.bib}
+@inbook{Aptx99,
+ author = "Apt, Krysztof R. and Bezem, Marc",
+ title = {{Formulas as Programs}},
+ booktitle = "The Logic Programming Paradigm",
+ year = "1999",
+ publisher = "Springer Berlin Heidelberg",
+ pages = "75107",
+ isbn = "9783642600852",
+ abstract =
+ "We provide here a computational interpretation of firstorder
+ logic based on a constructive interpretation of satisfiability
+ w.r.t. a fixed but arbitrary interpretation. In this approach the
+ formulas themselves are programs. This contrasts with the
+ socalled formulas as types approach in which the proofs of the
+ formulas are typed terms that can be taken as programs. This view
+ of computing is inspired by logic programming and constraint logic
+ programming but differs from them in a number of crucial aspects.
+
+ Formulas as programs is argued to yield a realistic approach to
+ programming that has been realized in the implemented programming
+ language Alma0 Apt, Brunekreef, Partington and Schaerf (1998)
+ that combines the advantages of imperative and logic
+ programming. The work here reported can also be used to reason
+ about the correctness of nonrecursive Alma0 programs that do not
+ include destructive assignment.",
+ paper = "Aptx99.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Aspinall, David}
\index{Hofmann, Martin}
\begin{chunk}{axiom.bib}
@@ 12820,6 +13054,36 @@ when shown in factored form.
\end{chunk}
+\index{Atkey, Robert}
+\begin{chunk}{axiom.bib}
+@misc{Atke18,
+ author = "Atkey, Robert",
+ title = {{Parameterised Notions of Computation}},
+ link = "\url{https://bentnib.org/paramnotionsjfp.pdf}",
+ year = "2018",
+ abstract =
+ "Moggi’s Computational Monads and Power et al ’s equivalent notion of
+ Freyd category have captured a large range of computational effects
+ present in programming languages. Examples include nontermination,
+ nondeterminism, exceptions, continuations, sideeffects and
+ input/output. We present generalisations of both computational monads
+ and Freyd categories, which we call parameterised monads and
+ parameterised Freyd categories, that also capture computational
+ effects with parameters. Examples of such are composable
+ continuations, sideeffects where the type of the state varies and
+ input/output where the range of inputs and outputs varies. By also
+ considering structured parameterisation, we extend the range of
+ effects to cover separated sideeffects and multiple independent
+ streams of I/O. We also present two typed $\lambda$calculi that
+ soundly and completely model our categorical definitions — with and
+ without symmetric monoidal parameterisation — and act as prototypical
+ languages with parameterised effects.",
+ paper = "Atke18.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Avigad, Jeremy}
\begin{chunk}{axiom.bib}
@article{Avig18a,
@@ 12869,6 +13133,64 @@ when shown in factored form.
\end{chunk}
+\index{Bailey, David H.}
+\index{Borwein, Jonathan M.}
+\begin{chunk}{axiom.bib}
+@article{Bail11,
+ author = "Bailey, David H. and Borwein, Jonathan M.",
+ title = {{Highprecision Numerical Integration: Progress and Challenges}},
+ journal = "J. Symbolic Computation",
+ number = "46",
+ pages = "741754",
+ year = "2011",
+ abstract =
+ "One of the most fruitful advances in the field of experimental
+ mathematics has been the development of practical methods for very
+ highprecision numerical integration, a quest initiated by Keith
+ Geddes and other researchers in the 1980s and 1990s.These
+ techniques, when coupled with equally powerful integer relation
+ detection methods, have resulted in the analytic evaluation of many
+ integrals that previously were beyond the realm of symbolic
+ techniques.This paper presents a survey of the current stateoftheart
+ in this area (including results by the present authors and others),
+ mentions some new results, and then sketches what challenges lie
+ ahead.",
+ paper = "Bail11.pdf"
+}
+
+\end{chunk}
+
+\index{Bailey, David H.}
+\index{Borwein, Jonathan M.}
+\index{Kaiser, Alexander D.}
+\begin{chunk}{axiom.bib}
+@article{Bail14,
+ author = "Bailey, David H. and Borwein, Jonathan M. and
+ Kaiser, Alexander D.",
+ title = {{Automated Simplification of Large Symbolic Expressions}},
+ journal = "J. Symbolic Computation",
+ volume = "60",
+ pages = "120136",
+ year = "2014",
+ abstract =
+ "We present a set of algorithms for automated simplification of
+ symbolic constants of the form
+ $\sum_i\alpha_i x_i$ with $\alpha_i$ rational and $x_i$
+ complex. The included algorithms, called SimplifySum and
+ implemented in Mathematica , remove redundant terms, attempt to make
+ terms and the full expression real, and remove terms using repeated
+ application of the multipair PSLQ integer relation detection
+ algorithm. Also included are facilities for making substitutions
+ according to userspecified identities. We illustrate this toolset by
+ giving some realworld examples of its usage, including one, for
+ instance, where the tool reduced a symbolic expression of
+ approximately 100 000 characters in size enough to enable manual
+ manipulation to one with just four simple terms.",
+ paper = "Bail14.pdf"
+}
+
+\end{chunk}
+
\index{Balsters, Herman}
\index{Fokkinga, Maarten M.}
\begin{chunk}{axiom.bib}
@@ 12987,6 +13309,27 @@ when shown in factored form.
\end{chunk}
+\index{Barnett, Michael P.}
+\begin{chunk}{axiom.bib}
+@article{Barn08,
+ author = "Barnett, Michael P.",
+ title = {{Reasoning in Symbolic Computation}},
+ journal = "ACM Communications in Symbolic Algebra",
+ volume = "42",
+ number = "1",
+ year = "2008",
+ abstract =
+ "I discuss notations for some styles of mathematical reasoning that
+ include analogy. These notations extend the conventions of the
+ mathematica package mathscape that I reported recently in the
+ Journal of Symbolic Computation. The paper introduces the reasoning
+ objects that I call 'precursors' and 'consequences lists'.",
+ paper = "Barn08.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Barras, Bruno}
\begin{chunk}{axiom.bib}
@techreport{Barr96a,
@@ 13090,6 +13433,21 @@ when shown in factored form.
\end{chunk}
+\index{Beeson, Michael}
+\begin{chunk}{axiom.bib}
+@article{Bees80a,
+ author = "Beeson, Michael",
+ title = {{Formalizing Constructive Mathematics: Why and How?}},
+ journal = "Lecture Notes in Mathematics",
+ volume = "873",
+ pages = "146190",
+ year = "1980",
+ paper = "Bees80a.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Benini, Marco}
\begin{chunk}{axiom.bib}
@misc{Beni95,
@@ 13253,6 +13611,30 @@ when shown in factored form.
\end{chunk}
+\index{Buchberger, Bruno}
+\begin{chunk}{axiom.bib}
+@article{Buch02,
+ author = "Buchberger, Bruno",
+ title = {{Computer Algebra: The End of Mathematics?}},
+ journal = "ACM SIGSAM",
+ volume = "36",
+ number = "1",
+ year = "2002",
+ abstract =
+ "Mathematical software systems, such as Mathematica, Maple, Derive,
+ and so on, are substantially based on enormous advances in the area of
+ mathematics known as Computer Algebra or Symbolic Mathematics. In
+ fact, everything taught in high school and in the first semesters of a
+ university mathematical education, is available in these systems 'at
+ the touch of the button'. Will mathematics become unnecessary because
+ of this? In the three sections of this essay, I answer this question
+ for nonmathematicians, for mathematicians and for (future) students
+ of mathematics.",
+ paper = "Buch02.pdf"
+}
+
+\end{chunk}
+
\begin{chunk}{axiom.bib}
@misc{Byte79,
author = "Byte Publications",
@@ 13852,6 +14234,18 @@ when shown in factored form.
\index{Daly, Timothy}
\begin{chunk}{axiom.bib}
+@misc{Daly06a,
+ author = "Daly, Timothy",
+ title = {{Literate Programming}},
+ link = "\url{http://lambdatheultimate.org/node/1336}",
+ year = "2006",
+ keywords = "axiomref, TPDref"
+}
+
+\end{chunk}
+
+\index{Daly, Timothy}
+\begin{chunk}{axiom.bib}
@misc{Daly18,
author = "Daly, Timothy",
title = {{Proving Axiom Sane: Survey of CAS and Proof Cooperation}},
@@ 13891,6 +14285,35 @@ when shown in factored form.
\end{chunk}
+\index{Davies, Rowan}
+\index{Pfenning, Frank}
+\begin{chunk}{axiom.bib}
+@article{Davi01,
+ author = "Davies, Rowan and Pfenning, Frank",
+ title = {{A Modal Analysis of Staged Computation}},
+ journal = "J. ACM",
+ volume = "48",
+ number = "3",
+ pages = "555604",
+ year = "2001",
+ abstract =
+ "We show that a type system based on the intuitionistic modal logic S4
+ provides an expressive framework for specifying and analyzing
+ computation stages in the context of typed $\lambda$calculi and
+ functional languages. We directly demonstrate the sense in which our
+ $\lambda_e^{\rightarrow\Box}$calculus captures staging, and also give
+ a conservative embedding of Nielson and Nielson's twolevel functional
+ language in our functional language MiniML${}^\Box$, thus proving that
+ bindingtime correctness is equivalent to modal correctness on this
+ fragment. In addition, MiniML${}^\Box$ can also express immediate
+ evaluation and sharing of code across multiple stages, thus supporting
+ runtime code generation as well as partial evaluation.",
+ paper = "Davi01.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Davis, Jared Curran}
\begin{chunk}{axiom.bib}
@phdthesis{Davi09,
@@ 13950,6 +14373,7 @@ when shown in factored form.
number = "2",
pages = "117183",
year = "2015",
+ link = "\url{https://www.cl.cam.ac.uk/~mom22/jitawa/}",
abstract =
"This paper presents, we believe, the most comprehensive evidence of a
theorem prover’s soundness to date. Our subject is the Milawa theorem
@@ 14025,6 +14449,64 @@ when shown in factored form.
\end{chunk}
+\index{Dershowitz, Nachum}
+\begin{chunk}{axiom.bib}
+@article{Ders87,
+ author = "Dershowitz, Nachum",
+ title = {{Termination of Rewriting}},
+ journal = "J. Symbolic Computation",
+ volume = "3",
+ year = "1987",
+ pages = "69116",
+ abstract =
+ "This survey describes methods for proving that systems of rewrite
+ rules are terminating programs. We illustrate the use in termination
+ proofs of various kinds of orderings on terms, including polynomial
+ interpretations and path orderings. The effect of restrictions, such
+ as linearity, on the form of rules is also considered. In general,
+ however, termination is an undeeidable property of rewrite systems.",
+ paper = "Ders87.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Dick, A.J.J.}
+\begin{chunk}{axiom.bib}
+@techreport{Dick88,
+ author = "Dick, A.J.J.",
+ title = {{Automated Equational Reasoning and the KnuthBendix Algorithm:
+ An Informal Introduction}},
+ year = "1988",
+ type = "technical report",
+ institution = "Rutherford Appelton Laboratory",
+ number = "RAL88043",
+ paper = "Dick88.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Dick, Jeremy}
+\begin{chunk}{axiom.bib}
+@article{Dick91,
+ author = "Dick, Jeremy",
+ title = {{An Introduction to KnuthBendix Completion}},
+ journal = "The Computer Journal",
+ volume = "34",
+ number = "1",
+ year = "1991",
+ abstract =
+ "An informal introduction is given to the underlying concepts of
+ term rewriting. Topics covered are KnuthBendix completion,
+ completion modulo equations, unfailing completion and theorem
+ proving by completion.",
+ paper = "Dick91.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Dijkstra, E.W.}
\begin{chunk}{axiom.bib}
@misc{Dijk71,
@@ 14050,6 +14532,31 @@ when shown in factored form.
\end{chunk}
+\index{Dijkstra, Edsgar W.}
+\begin{chunk}{axiom.bib}
+@article{Dijk75,
+ author = "Dijkstra, Edsgar W.",
+ title = {{Guarded Commands, Nondeterminancy and Formal Derivation
+ of Programs}},
+ journal = "Comm. of the ACM",
+ volume = "18",
+ number = "8",
+ year = "1975",
+ pages = "453457",
+ abstract =
+ "Socalled 'guarded commands' are introduced as a building block
+ for alternative and repetitive constructs that allow
+ nondeterministic program components for which at least the
+ activity evoked, but possibly even the final state, is not
+ necessarily uniquly determined by the initial state. For the
+ formal derivation of programs expressed in terms of these
+ constructs, a calculus will be shown.",
+ paper = "Dijk75.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Dolan, Stephen}
\begin{chunk}{axiom.bib}
@phdthesis{Dola16,
@@ 14269,6 +14776,58 @@ when shown in factored form.
\subsection{E} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{van Emden, M.H.}
+\index{Kowalski, R.A.}
+\begin{chunk}{axiom.bib}
+@article{Emde76,
+ author = "van Emden, M.H. and Kowalski, R.A.",
+ title = {{The Semantics of Predicate Logic as a Programming Language}},
+ journal = "J. Association for Computing Machinery",
+ volume = "23",
+ number = "4",
+ year = "1976",
+ pages = "733742",
+ abstract =
+ "Sentences in firstorder predicate logic can be usefully interpreted
+ as programs In this paper the operational and fixpomt semantics of
+ predicate logic programs are defined, and the connections with the
+ proof theory and model theory of logic are investigated It is
+ concluded that operational semantics is a part of proof theory and
+ that fixpolnt semantics is a special case of modeltheoret:c
+ semantics.",
+ paper = "Emde76.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{England, M.}
+\index{ChebTerrab, E.}
+\index{Bradford, R.}
+\index{Davenport, J.H.}
+\index{Wilson, D.}
+\begin{chunk}{axiom.bib}
+@article{Engl14c,
+ author = "England, M. and ChebTerrab, E. and Bradford, R. and
+ Davenport, J.H. and Wilson, D.",
+ title = {{Branch Cuts in MAPLE 17}},
+ journal = "ACM Comm. in Computer Algebra",
+ volume = "48",
+ number = "1",
+ year = "2014",
+ abstract =
+ "Accurate and comprehensible knowledge about the position of branch
+ cuts is essential for correctly working with multivalued functions,
+ such as the square root and logarithm. We discuss the new tools in
+ Maple 17 for calculating and visualising the branch cuts of such
+ functions, and others built up from them. The cuts are described in an
+ intuitive and accurate form, offering substantial improvement on the
+ descriptions previously available.",
+ paper = "Engl14c.pdf"
+}
+
+\end{chunk}
+
\index{Esparza, Javier}
\begin{chunk}{axiom.bib}
@book{Espa17,
@@ 14282,6 +14841,37 @@ when shown in factored form.
\end{chunk}
+\index{Essex, Christopher}
+\index{Davison, Matt}
+\index{Schulzky, Christian}
+\begin{chunk}{axiom.bib}
+@article{Esse00,
+ author = "Essex, Christopher and Davison, Matt and Schulzky, Christian",
+ title = {{Numerical Monsters}},
+ journal = "ACM SIGSAM",
+ volume = "34",
+ number = "4",
+ year = "2000",
+ abstract =
+ "When the results of certain computer calculations are shown to be not
+ simply incorrect but dramatically incorrect, we have a powerful reason
+ to be cautious about all computerbased calculations. In this paper we
+ present a 'Rogue's Gallery' of simple calculations whose correct
+ solutions are obvious to humans but whose numerical solutions are
+ incorrect in pathological ways. We call these calculations, which can
+ be guaranteed to wreak numerical mayhem across both software
+ packages and hardware platforms, 'Numerical Monsters'. Our monsters
+ can be used to provide deep insights into how computer calculations
+ fail, and we use t h e m to engender appreciation for the subject of
+ numerical analysis in our students. Although these monsters are based
+ on wellunderstood numerical pathologies, even experienced numerical
+ analysts will find surprises in their behaviour and ,can use the
+ lessons they bring to become even better masters of their tools.",
+ paper = "Esse00.pdf"
+}
+
+\end{chunk}
+
\subsection{F} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Farmer, William M.}
@@ 14512,6 +15102,45 @@ when shown in factored form.
\end{chunk}
+\index{Fateman, Richard}
+\begin{chunk}{axiom.bib}
+@article{Fate14a,
+ author = "Fateman, Richard",
+ title = {{Algorithm Differentiation in Lisp: ADIL}},
+ journal = "ACM Comm. in Computer Algebra",
+ volume = "48",
+ number = "3",
+ year = "2014",
+ abstract =
+ "Algorithm differentiation (AD) is a technique used to transform a
+ program $F$ computing a numerical function of one argument $F(x)$ into
+ another program $G(p)$ that returns a pair,
+ $\langle F (p), F^\prime(p)\rangle$ where by $F^\prime(p)$
+ we mean the derivative of $F$ with respect to its argument $x$,
+ evaluated at $x = p$. That is, we have a program AD that takes as input
+ a program, and returns another: $G := AD(F)$. Over the years AD
+ programs have been developed to allow $F$ to be expressed in some
+ specialized variant of a popular programming language L (FORTRAN, C,
+ Matlab, Python) and where $G$ is delivered in that language $L$ or some
+ other. Alternatively, executing $F(p)$ is some environment will deliver
+ $\langle F^\prime(p), F(p)\rangle$ directly. AD tools have also
+ been incorporated in computer algebra systems (CAS) such as
+ Maple. A CAS is hardly necessary for the task of writing the AD
+ program, since the main requirement is a set of tools for
+ manipulation of an internal (typically tree) form of a program.
+ In Lisp, a normal program is already in this form and so the AD
+ program in Lisp (ADIL), the target $F$ and the product $G$ can
+ all be expressed compactly in Lisp. In spite of the brevity and
+ extensibility of the ADIL program, we can provide
+ features which are unsupported in other AD programs. In particular,
+ recursive functions are easily accommodated. Our perspective here is
+ to point out that for scientists who write programs in Lisp or any
+ language that can be converted to Lisp, AD is easily at hand.",
+ paper = "Fate14a.pdf"
+}
+
+\end{chunk}
+
\index{Feferman, Solomon}
\begin{chunk}{axiom.bib}
@misc{Fefe95,
@@ 14886,6 +15515,20 @@ when shown in factored form.
\end{chunk}
+\index{Glymour, Clark}
+\index{Serafin, Luke}
+\begin{chunk}{axiom.bib}
+@misc{Glym15,
+ author = "Glymour, Clark and Serafin, Luke",
+ title = {{Mathematical Metaphysics}},
+ link = "\url{http://shelf1.library.cmu.edu/HSS/2015/a1626190.pdf}",
+ year = "2015",
+ paper = "Glym15.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Gonthier, Georges}
\begin{chunk}{axiom.bib}
@article{Gont09a,
@@ 14951,6 +15594,21 @@ when shown in factored form.
\end{chunk}
+\index{Goodman, Nicolas D.}
+\begin{chunk}{axiom.bib}
+@article{Good80,
+ author = "Goodman, Nicolas D.",
+ title = {{Reflections on Bishop's Philosophy of Mathematics}},
+ journal = "Lecture Notes in Mathematics",
+ volume = "873",
+ pages = "135145",
+ year = "1980",
+ paper = "Good80.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Gordon, Michael J.}
\index{Milner, Arthur j.}
\index{Wadsworth, Christopher P.}
@@ 15316,6 +15974,25 @@ when shown in factored form.
\subsection{H} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Hamada, Tatsuyoshi}
+\begin{chunk}{axiom.bib}
+@article{Hama14,
+ author = "Hamada, Tatsuyoshi",
+ title = {{MathLibre: Personalizable Computer Environment for
+ Mathematical Research}},
+ volume = "48",
+ number = "3",
+ year = "2014",
+ abstract =
+ "MathLibre is a project to archive free mathematical software and free
+ mathematical documents and offer them on Live Linux system. MathLibre
+ Project is the direct descendant of KNOPPIX/Math Project. It provides
+ a desktop for mathematicians that can be set up easily and quickly.",
+ paper = "Hama14.pdf"
+}
+
+\end{chunk}
+
\index{Hamming, Richard}
\begin{chunk}{axiom.bib}
@misc{Hamm95,
@@ 15531,6 +16208,88 @@ when shown in factored form.
\subsection{J} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Jenks, Richard D.}
+\begin{chunk}{axiom.bib}
+@article{Jenk11,
+ author = "Jenks, Richard D.",
+ title = {{The 2011 Richard D. Jenks Memorial Prize}},
+ journal = "ACM Communications in Computer Algebra",
+ volume = "45",
+ number = "4",
+ year = "2011",
+ abstract =
+ "The 2011 Richard D. Jenks Memorial Prize for Excellence in
+ Software Engineering Applied to Computer Algebra was presented by
+ members of the Prize Selection Committee and its chair, Erich
+ Kaltofen, at ISSAC and SNC in San Jose, CA, on June 9, 2011 to the
+ Maple Project at the University of Waterloo.",
+ paper = "Jenk11.pdf",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
+\index{Jenks, Richard D.}
+\begin{chunk}{axiom.bib}
+@article{Jenk13,
+ author = "Jenks, Richard D.",
+ title = {{The 2013 Richard D. Jenks Memorial Prize}},
+ journal = "ACM Communications in Computer Algebra",
+ volume = "47",
+ number = "4",
+ year = "2013",
+ abstract =
+ "The 2013 Richard D. Jenks Memorial Prize for Excellence in
+ Software Engineering Applied to Computer Algebra was announced by
+ members of the Prize Selection Committee, Mark Giesbrecht
+ representing its chair Erich Kaltofen, at ISSAC in Boston, MA, on
+ June 28, 2013 to have been awared to Professor William Arthur
+ Stein of the Sage Project at the University of Washington.",
+ paper = "Jenk13.pdf",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
+\index{Jenks, Richard D.}
+\begin{chunk}{axiom.bib}
+@article{Jenk15,
+ author = "Jenks, Richard D.",
+ title = {{The 2015 Richard D. Jenks Memorial Prize}},
+ journal = "ACM Communications in Computer Algebra",
+ volume = "49",
+ number = "4",
+ year = "2015",
+ abstract =
+ "The 2015 Richard D. Jenks Memorial Prize was awarded on October
+ 30, 2015 at the Fields Institute in Toronto during the Major
+ Thematic Program on Computer Algebra to Professor Victor Shoup for
+ NTL: A Library for doing Number Theory.",
+ paper = "Jenk15.pdf",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
+\index{Jenks, Richard D.}
+\begin{chunk}{axiom.bib}
+@article{Jenk17,
+ author = "Jenks, Richard D.",
+ title = {{The 2017 Richard D. Jenks Memorial Prize}},
+ journal = "ACM Communications in Computer Algebra",
+ volume = "51",
+ number = "4",
+ year = "2017",
+ abstract =
+ "The 2017 Richard D. Jenks Memorial Prize for Excellence in
+ Software Engineering Applied to Computer Algebra has been awarded
+ to Stephen Wolfram for WolframAlpha and Mathematica.",
+ paper = "Jenk17.pdf",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
\index{Johnson, C.W.}
\begin{chunk}{axiom.bib}
@article{John96,
@@ 15683,6 +16442,20 @@ when shown in factored form.
\end{chunk}
+\index{Kant, Immanuel}
+\begin{chunk}{axiom.bib}
+@book{Kant98,
+ author = "Kant, Immanuel",
+ title = {{The Critique of Pure Reason}},
+ publisher = "Cambridge University Press",
+ year = "1998",
+ isbn = "0521354021",
+ link = "\url{http://strangebeautiful.com/othertexts/kantfirstcritiquecambridge.pdf}",
+ paper = "Kant98.pdf"
+}
+
+\end{chunk}
+
\index{Keimel, Klaus}
\index{Plotkin, Gordon D.}
\begin{chunk}{axiom.bib}
@@ 15802,6 +16575,24 @@ when shown in factored form.
\end{chunk}
+\index{Knuth, Donald E.}
+\index{Bendix, Peter B.}
+\begin{chunk}
+@incollection{Knut70,
+ author = "Knuth, Donald E. and Bendix, Peter B.",
+ title = {{Simple Word Problems in Unversal Algebras}},
+ booktitle = "Computational Problems in Abstract Algebra",
+ editor = "Leech, John",
+ publisher = "Pergamon Press",
+ isbn = "080129757",
+ year = "1970",
+ pages = "263298",
+ paper = "Knut70.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Kohlhase, Michael}
\index{De Feo, Luca}
\index{Muller, Dennis}
@@ 15884,6 +16675,32 @@ when shown in factored form.
\end{chunk}
+\index{Krall, Andreas}
+\begin{chunk}{axiom.bib}
+@misc{Kralxx,
+ author = "Krall, Andreas",
+ title = {{Implementation Techniques for Prolog}},
+ link = "\url{https://pdfs.semanticscholar.org/fdbf/aa46bf6ab2148595f638fe9afe97033583ee.pdf}",
+ year = "unknown",
+ abstract =
+ "This paper is a short survey about currently used implementation
+ techniques for Prolog. It gives an introduction to unification and
+ resolution in Prolog and presents the memory model and a basic
+ execution model. These models are expanded to the Vienna Abstract
+ Machine (VAM) with its two versions, the VAM${}_{2p}$ and the
+ VAM${}_{1p}$, and the most famous abstract machine, the Warren
+ Abstract Machine (WAM). The continuation passing style model of
+ Prolog, binary Prolog, leands to the BinWAM. Abstract
+ interpretation can be applied to gather information about a
+ program. This information is used in the generation of very
+ specialized machine code and in optimizations like clause indexing
+ and instruction scheduling on each kind of abstract machine.",
+ paper = "Kralxx.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Kranz, David}
\index{Kelsey, Richard}
\index{Rees, Jonathan}
@@ 15993,6 +16810,70 @@ when shown in factored form.
\end{chunk}
+\index{Lamport, Leslie}
+\begin{chunk}{axiom.bib}
+@misc{Lamp03,
+ author = "Lamport, Leslie",
+ title = {{The Future of Computing: Logic or Biology}},
+ link =
+ "\url{https://lamport.azurewebsites.net/pubs/futureofcomputing.pdf}",
+ year = "2003",
+ paper = "Lamp03.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Lazard, Daniel}
+\begin{chunk}{axiom.bib}
+@article{Laza01,
+ author = "Lazard, Daniel",
+ title = {{Solving Systems of Algebraic Equations}},
+ journal = "ACM SIGSAM Bulletin",
+ volume = "35",
+ number = "3",
+ year = "2001",
+ abstract =
+ "Let $f_1,\ldots,f_k$ be $k$ multivariate polynomials which have
+ a finite number of common zeros in the algebraic closure of the ground
+ field, counting the common zeros at infinity. An algorithm is
+ given and proved which reduces the computations of these zeros to
+ the resolution of a single univariate equation whose degree is the
+ number of common zeros. This algorithm gives the whole algebraic
+ and geometric structure of the set of zeros (multiplicities,
+ conjugate zeros,...). When all the polynomials have the same degree,
+ the complexity of this algorithm is polynomial relative to the generic
+ number of solutions.",
+ paper = "Laza01.pdf"
+}
+
+\end{chunk}
+
+\index{Leech, John}
+\begin{chunk}{axiom.bib}
+@book{Leec70,
+ author = "Leech, John",
+ title = {{Computational Problems in Abstract Algebra}},
+ publisher = "Pergamon Press",
+ year = "1970",
+ isbn = "080129757",
+ paper = "Leec70.pdf"
+}
+
+\end{chunk}
+
+\index{LeGuin, Ursula K.}
+\begin{chunk}{axiom.bib}
+@book{Legu76,
+ author = "LeGuin, Ursula K.",
+ title = {{The Left Hand of Darkness}},
+ publisher = "Penguin Random House",
+ year = "1976",
+ isbn = "9781101665398"
+}
+
+\end{chunk}
+
\index{Leroy, Xavier}
\begin{chunk}{axiom.bib}
@techreport{Lero90,
@@ 16249,6 +17130,18 @@ when shown in factored form.
\end{chunk}
+\index{Mazur, Barry}
+\begin{chunk}{axiom.bib}
+@misc{Mazu07,
+ author = "Mazur, Barry",
+ title = {{When is One Thing Equal to Some Other Thing?}},
+ link = "\url{http://www.math.harvard.edu/~mazur/preprints/when_is_one.pdf}",
+ year = "2007",
+ paper = "Mazu07.pdf"
+}
+
+\end{chunk}
+
\index{McCarthy, John}
\begin{chunk}{axiom.bib}
@article{Mcca60,
@@ 16438,6 +17331,18 @@ when shown in factored form.
\end{chunk}
+\index{Prengel, Alex}
+\begin{chunk}{axiom.bib}
+@misc{Pren16,
+ author = "Prengel, Alex",
+ title = {{MIT axiommath\_v8.14}},
+ link = "\url{http://web.mit.edu/axiommath_v8.14/}",
+ year = "2016",
+ keywords = "axiomref, TPDref"
+}
+
+\end{chunk}
+
\index{Mitchell, John}
\begin{chunk}{axiom.bib}
@inproceedings{Mitc84,
@@ 16826,6 +17731,7 @@ when shown in factored form.
volume = "6898",
pages = "265280",
year = "2011",
+ link = "\url{https://www.cl.cam.ac.uk/~mom22/jitawa/}",
abstract =
"Theorem provers, such as ACL2, HOL, Isabelle and Coq, rely on the
correctness of runtime systems for programming languages like ML,
@@ 16861,6 +17767,7 @@ when shown in factored form.
volume = "7406",
pages = "412417",
year = "2012",
+ link = "\url{https://www.cl.cam.ac.uk/~mom22/jitawa/}",
abstract =
"This paper presents a method which simplifies verification of deeply
embedded functional programs. We present a technique by which
@@ 17027,6 +17934,45 @@ when shown in factored form.
\end{chunk}
+\index{Oles, Frank Joseph}
+\begin{chunk}{axiom.bib}
+@phdthesis{Oles82,
+ author = "Oles, Frank Joseph",
+ title = {{A CategoryTheoretic Approach to the Semantics of
+ Programming Languages}},
+ school = "Syracuse University",
+ year = "1982",
+ abstract =
+ "Here we create a framework for handling the semantics of fully
+ typed programming languages with imperative features, higherorder
+ ALGOLlike procedures, block structure, and implicit
+ conversions. Our approach involves introduction of a new family of
+ programming languages, the {\sl coercive typed $\lambda$calculi},
+ denoted by $L$ in the body of the dissertation. By appropriately
+ choosing the linguistic constants (i.e. generators) of $L$, we can
+ view phrases of variants of ALGOL as syntactically sugared phrases
+ of $L$.
+
+ This dissertation breaks into three parts. In the first part,
+ consisting of the first chapter, we supply basic definitions and
+ motivate the idea that functor categories arise naturally in the
+ explanation of block structure and stack discipline. The second
+ part, consisting of the next three chapters, is dedicated to the
+ general theory of the semantics of the coercive typed
+ $\lambda$calculus; the interplay between posets, algebras, and
+ Cartesian closed categories is particularly intense here. The
+ remaining four chapters make up the final part, in which we apply
+ the general theory to give both direct and continuation semantics
+ for desugared variants of ALGOL. To do so, it is necessary to show
+ certain functor categories are Cartesian closed and to describe a
+ category $\Sigma$ of store shapes. An interesting novelty in the
+ presentation of continuation semantics is the view that commands
+ form a procedural, rather than a primitive, phrase type.",
+ paper = "Oles82.pdf"
+}
+
+\end{chunk}
+
\index{Oury, Nicolas}
\index{Swierstra, Wouter}
\begin{chunk}{axiom.bib}
@@ 17218,6 +18164,33 @@ when shown in factored form.
\end{chunk}
\index{Pfenning, Frank}
+\index{Davies, Rowan}
+\begin{chunk}{axiom.bib}
+@article{Pfen01,
+ author = "Pfenning, Frank and Davies, Rowan",
+ title = {{A Judgemental Reconstruction of Modal Logic}},
+ journal = "Mathematical Structures in Computer Science",
+ volume = "11",
+ pages = "511540",
+ year = "2001",
+ abstract =
+ "We reconsider the foundations of modal logic, following MartinLof's
+ methodology of distinguishing judgments from propositions. We give
+ constructive meaning explanations for necessity and possibility which
+ yields a simple and uniform system of natural deduction for
+ intuitionistic modal logic which does not exhibit anomalies found in
+ other proposals. We also give a new presentation of lax logic and nd
+ that the lax modality is already expressible using possibility and
+ necessity. Through a computational interpretation of proofs in modal
+ logic we further obtain a new formulation of Moggi's monadic
+ metalanguage.",
+ paper = "Pfen01.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Pfenning, Frank}
\begin{chunk}{axiom.bib}
@misc{Pfen04,
author = "Pfenning, Frank",
@@ 17564,6 +18537,24 @@ when shown in factored form.
\end{chunk}
+\index{Reynolds, John C.}
+\begin{chunk}{axiom.bib}
+@article{Reyn93,
+ author = "Reynolds, John C.",
+ title = {{The Discoveries of Continuations}},
+ journal = "Lisp and Symbolic Computation",
+ volume = "6",
+ pages = "233248",
+ year = "1993",
+ abstract =
+ "We give a brief account of the discoveries of continuations and
+ related concepts.",
+ paper = "Reyn93.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Robinson, Alan}
\index{Voronkov, Andrei}
\begin{chunk}{axiom.bib}
@@ 17577,6 +18568,33 @@ when shown in factored form.
\end{chunk}
+\index{Roche, Daniel S.}
+\begin{chunk}{axiom.bib}
+@article{Roch11,
+ author = "Roche, Daniel S.",
+ title = {{Chunky and EqualSpaced Polynomial Multiplication}},
+ journal = "J. Symbolic Computation",
+ volume = "46",
+ pages = "791806",
+ year = "2011",
+ abstract =
+ "Finding the product of two polynomials is an essential and basic
+ problem in computer algebra. While most previous results have
+ focused on the worstcase complexity, we instead employ the
+ technique of adaptive analysis to give an improvement in many
+ ‘‘easy’’ cases. We present two adaptive measures and methods
+ for polynomial multiplication, and also show how to effectively
+ combine them to gain both advantages. One useful feature of these
+ algorithms is that they essentially provide a gradient between
+ existing ‘‘sparse’’ and ‘‘dense’’ methods. We prove that these
+ approaches provide significant improvements in many cases but
+ in the worst case are still comparable to the fastest existing
+ algorithms.",
+ paper = "Roch11.pdf"
+}
+
+\end{chunk}
+
\index{Roorda, JanWillem}
\begin{chunk}{axiom.bib}
@phdthesis{Roor00,
@@ 17613,6 +18631,19 @@ when shown in factored form.
\end{chunk}
+\index{Rosenkranz, Markus}
+\begin{chunk}{axiom.bib}
+@book{Rose07,
+ author = "Rosenkranz, Markus",
+ title = {{Gr\"obner Bases in Symbolic Analysis}},
+ publisher = "Walter de Gruyter, Berlin Germany",
+ year = "2007",
+ isbn = "978311.0193237",
+ keywords = "axiomref, TPDref"
+}
+
+\end{chunk}
+
\index{Roy, Peter Van}
\index{Haridi, Seif}
\begin{chunk}{axiom.bib}
@@ 17742,6 +18773,54 @@ when shown in factored form.
\end{chunk}
+\index{Schonhage, A.}
+\begin{chunk}{axiom.bib}
+@article{Scho88,
+ author = "Schonhage, A.",
+ title = {{Probabilistic Computation of Integer Polynomial GCDs}},
+ journal = "J. of Algorithms",
+ volume = "9",
+ pages = "365371",
+ year = "1988",
+ abstract =
+ "We describe a probabilistic algorithm for the computation of the
+ gcd of two univariate integer polynomials of degrees $\le n$ with
+ their $l^1$norms being bounded by $2^h$ and estimate its expected
+ running time by a worstcase bound of
+ $O(n(n+h)^{l+\epsilon(l)})$.",
+ paper = "Scho88.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Scott, Dana S.}
+\begin{chunk}{axiom.bib}
+@article{Scot93,
+ author = "Scott, Dana S.",
+ title = {{A TypeTheoretical Alternative to ISWIM, CUCH, OWHY}},
+ journal = "Theoretical Computer Science",
+ volume = 121,
+ number = "12",
+ year = "1993",
+ pages = "411440",
+ abstract =
+ "The paper (first written in 1969 and circulated privately) concerns
+ the definition, axiomatization, and applications of the hereditarily
+ monotone and continuous functionals generated from the integers and
+ the Booleans (plus “undefined” elements). The system is formulated as
+ a typed system of combinators (or as a typed λcalculus) with a
+ recursion operator (the least fixedpoint operator), and its proof
+ rules are contrasted to a certain extent with those of the untyped
+ λcalculus. For publication (1993), a new preface has been added, and
+ many bibliographical references and comments in footnotes have been
+ appended.",
+ paper = "Scot93.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Scott, Dana S.}
\index{Strachey, C.}
\begin{chunk}{axiom.bib}
@@ 17775,6 +18854,25 @@ when shown in factored form.
\end{chunk}
+\index{Sedjelmaci, Sidi M.}
+\begin{chunk}{axiom.bib}
+@article{Sedj13,
+ author = "Sedjelmaci, Sidi M.",
+ title = {{Fast Parallel GCD Algorithm of Many Integers}},
+ journal = "ACM Comm in Computer Algebra",
+ volume = "47",
+ number = "3",
+ year = "2013",
+ abstract =
+ "We present a new parallel algorithm which computes the GCD of $n$
+ integers of $O(n)$ bits in $O(n/log~n)$ time with
+ $O(n^{2+\epsilon})$ processors, for any $\epsilon > 0$ on CRCW
+ PRAM model.",
+ paper = "Sedj13.pdf"
+}
+
+\end{chunk}
+
\index{Shieber, Stuart M.}
\index{Schabes, Yves}
\index{Pereira, Fernando C.N.}
@@ 17804,6 +18902,18 @@ when shown in factored form.
\end{chunk}
+\index{Shankar, N.}
+\begin{chunk}{axiom.bib}
+@book{Shan94,
+ author = "Shankar, N.",
+ title = {{Metamathematics, Machines, and Godel's Proof}},
+ publisher = "Cambridge University Press",
+ year = "1994",
+ isbn = "0521585333"
+}
+
+\end{chunk}
+
\index{Shields, Mark}
\index{Jones, Simon Peyton}
\begin{chunk}{axiom.bib}
@@ 17843,18 +18953,6 @@ when shown in factored form.
\end{chunk}
\index{Shankar, N.}
\begin{chunk}{axiom.bib}
@book{Shan94,
 author = "Shankar, N.",
 title = {{Metamathematics, Machines, and Godel's Proof}},
 publisher = "Cambridge University Press",
 year = "1994",
 isbn = "0521585333"
}

\end{chunk}

\index{Shoenfield, Joseph R.}
\begin{chunk}{axiom.bib}
@book{Shoe67,
@@ 17867,6 +18965,55 @@ when shown in factored form.
\end{chunk}
+\index{Shulman, Michael}
+\begin{chunk}{axiom.bib}
+@misc{Shul18,
+ author = "Shulman, Michael",
+ title = {{Linear Logic for Constructive Mathematics}},
+ link = "\url{https://arxiv.org/pdf/1805.07518.pdf}",
+ year = "2018",
+ abstract =
+ "We show that numerous distinctive concepts of constructive
+ mathematics arise automatically from an interpretation of 'linear
+ higherorder logic' into intuitionistic higherorder logic via a Chu
+ construction. This includes apartness relations, complemented
+ subsets, antisubgroups and antiideals, strict and nonstrict order
+ pairs, cutvalued metrics, and apartness spaces. We also explain the
+ constructive bifurcation of classical concept s using the choice
+ between multiplicative and additive linear connectives. Linear logic
+ thus systematically 'constructivizes' classical definitions and deals
+ automatically with the resulting bookkeeping, and could potentially
+ be used directly as a basis for constructive mathematics in place
+ of intuitionistic logic.",
+ paper = "Shul18.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Smith, A.}
+\begin{chunk}{axiom.bib}
+@techreport{Smit90,
+ author = "Smith, A.",
+ title = {{The KnuthBendix Completion Algorithm and its Specification in Z}},
+ type = "technical report",
+ institution = "Ministry of Defence, RSRE Malvern WORCS",
+ year = "1990",
+ number = "RSRE Memorandum 4323",
+ abstract =
+ "Proving that something is a consequence of a set of axioms can be
+ very difficult. The KnuthBendix completion algorithm attempts to
+ automate this process when the axioms are equations. The algorithm
+ is bound up in the area of term rewriting, and so this memorandum
+ contains an introduction to the tehory of term rewriting, followed
+ by an overview of the algorithm. Finally a formal specification of
+ the algorithm is given using the language Z.",
+ paper = "Smit90.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Smith, Peter}
\begin{chunk}{axiom.bib}
@misc{Smit15,
@@ 17903,6 +19050,41 @@ when shown in factored form.
\end{chunk}
+\index{Sorenson, Jonathan}
+\begin{chunk}{axiom.bib}
+@article{Sore94,
+ author = "Sorenson, Jonathan",
+ title = {{Two Fast GCD Algorithms}},
+ journal = "Journal of Algorithms",
+ volume = "16",
+ pages = "110144",
+ year = "1994",
+ abstract =
+ "We present two new algorithms for computing geatest common
+ divisors: the right and leftshift $k$ary GCD algorithms. These
+ algorithms are generalizations of the binary and leftshift binary
+ algorithms. Interestingly, both new algorithms have sequential
+ versions that are practical and efficient and parallel versions
+ that rival the best previous parallel GCD algorithms. We show that
+ sequential versions of both algorithms take $O(n^2/log~n)$ bit
+ operations in the worst case to compute the GCD of two nbit
+ integers. This compares favorably to the Euclidean and moth
+ precision versions of these GCD algorithms, and we found that both
+ $k$ary algorithms are faster than the Euclidean and binary
+ algorithms on inputs of 100 to 1000 decimal digits in length. We
+ show that parallel versions of both algorithms match the
+ complexity of the best previous parallel GCD algorithm due to Chor
+ and Goldreich. Specifically, if $log~n\le k \le 2^n$ and $k$ is a
+ power of two, then both algorithms run in $O(n/log~n+log^2~n)$
+ time using a number of processors bounded by a polynomial in $n$
+ and $k$ on a common CRCW PRAM. We also discuss extended versions
+ of both algorithms.",
+ paper = "Sore94.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Steele, Guy Lewis}
\begin{chunk}{axiom.bib}
@techreport{Stee78,
@@ 17971,8 +19153,8 @@ when shown in factored form.
number = "AI Memo No. 453",
year = "1978",
abstract =
 "We examine the effes of various language design decisions on the
 programming styles available to a user of the language, with
+ "We examine the effects of various language design decisions on
+ the programming styles available to a user of the language, with
particular emphasis on the ability to incrementatlly construct
modular systems. At each step we exhibit an interactive
metacircular interpreter for the language under
@@ 17997,6 +19179,76 @@ when shown in factored form.
\end{chunk}
+
+\index{Stoutemyer, David R.}
+\begin{chunk}{axiom.bib}
+@article{Stou11,
+ author = "Stoutemyer, David R.",
+ title = {{Ways to Implement Computer Algebra Compactly}},
+ journal = "ACM Comm. in Computer Algebra",
+ volume = "45",
+ number = "4",
+ year = "2011",
+ abstract =
+ "Computer algebra had to be implemented compactly to fit on early
+ personal computers and handheld calculators. Compact implementation
+ is still important for portable handheld devices. Also, compact
+ implementation increases comprehensibility while decreasing develop
+ ment and maintenance time and cost, regardless of the platform. This
+ article describes several ways to achieve compact implementations,
+ including:
+ \begin{itemize}
+ \item Exploit evaluation followed by interpolation to avoid
+ implementing a parser, such as in PicoMath
+ \item Use contiguous storage as an expression stack to avoid garbage
+ collection and pointerspace overhead, such as in Calculus Demon
+ and TIMathEngine
+ \item Use various techniques for saving code space for linkedstorage
+ representation of expressions and functions, such as muMath and Derive
+ \end{itemize}",
+ paper = "Stou11.pdf",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
+\index{Stoutemyer, David R.}
+\begin{chunk}{axiom.bib}
+@article{Stou11a,
+ author = "Stoutemyer, David R.",
+ title = {{Ten Commandments for Good Default Expression Simplification}},
+ journal = "J. Symbolic Computation",
+ volume = "46",
+ pages = "859887",
+ year = "2011",
+ abstract =
+ "This article provides goals for the design and improvement of default
+ computer algebra expression simplification. These goals can also help
+ users recognize and partially circumvent some limitations of their
+ current computer algebra systems. Although motivated by computer
+ algebra, many of the goals are also applicable to manual
+ simplification, indicating what transformations are necessary and
+ sufficient for good simplification when no particular canonical result
+ form is required.
+
+ After motivating the ten goals, the article then explains how the
+ Altran partially factored form for rational expressions was extended
+ for Derive and for the computer algebra in Texas Instruments products
+ to help fulfill these goals. In contrast to the distributed Altran
+ representation, this recursive partially factored semifraction form:
+ \begin{itemize}
+ \item does not unnecessarily force common denominators
+ \item discovers and preserves significantly more factors
+ \item can represent general expressions
+ \item can produce an entire spectrum from fully factored over a
+ common denominator through complete multivariate partial fractions,
+ including a dense subset of all intermediate forms.
+ \end{itemize}",
+ paper = "Stou11a.pdf"
+}
+
+\end{chunk}
+
\index{Stoutemyer, David R.}
\begin{chunk}{axiom.bib}
@article{Stou12,
@@ 18043,6 +19295,53 @@ when shown in factored form.
\end{chunk}
+\index{Stoutemyer, David R.}
+\begin{chunk}{axiom.bib}
+@article{Stou13,
+ author = "Stoutemyer, David R.",
+ title = {{A Computer Algebra User Interface Manifesto}},
+ journal = "ACM Communications in Computer Algebra",
+ volume = "47",
+ number = "4",
+ year = "2013",
+ abstract =
+ "Many computer algebra systems have more than 1000 builtin functions,
+ making expertise difficult. Using mock dialog boxes, this article
+ describes a proposed interactive generalpurpose wizard for organizing
+ optional transformations and allowing easy fine grain control over the
+ form of the result – even by amateurs. This wizard integrates ideas
+ including:
+ \begin{itemize}
+ \item flexible subexpression selection;
+ \item complete control over the ordering of variables and
+ commutative operands, with wellchosen defaults;
+ \item interleaving the choice of successively less main
+ variables with applicable function choices to provide detailed
+ control without incurring a combinatorial number of applicable
+ alternatives at any one level;
+ \item quick applicability tests to reduce the listing of
+ inapplicable transformations;
+ \item using an organizing principle to order the alternatives
+ in a helpful manner;
+ \item labeling quicklycomputed alternatives in dialog boxes
+ with a preview of their results, using ellipsis elisions if
+ necessary or helpful;
+ \item allowing the user to retreat from a sequence of choices
+ to explore other branches of the tree of alternatives – or to
+ return quickly to branches already visited;
+ \item allowing the user to accumulate more than one of the
+ alternative forms;
+ \item integrating direct manipulation into the wizard; and
+ \item supporting not only the usual inputresult pair mode, but
+ also the useful alternative derivational and in situ replacement
+ modes in a unified window.
+ \end{itemize}",
+ paper = "Stou13.pdf",
+ kryeotfd = "printed"
+}p
+
+\end{chunk}
+
\index{Stuckey, Peter J.}
\index{Sulzmann, Martin}
\begin{chunk}{axiom.bib}
@@ 18165,6 +19464,21 @@ when shown in factored form.
\end{chunk}
+\index{Tarski, Alfred}
+\begin{chunk}{axiom.bib}
+@article{Tars69,
+ author = "Tarski, Alfred",
+ title = {{Truth and Proof}},
+ journal = "Scientific American",
+ volume = "1969",
+ pages = "6377",
+ year = "1969",
+ paper = "Tars69.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{TobinHochstadt, Sam}
\index{Felleisen, Matthias}
\begin{chunk}{axiom.bib}
@@ 18432,6 +19746,36 @@ when shown in factored form.
\end{chunk}
+\index{Weber, Kenneth}
+\index{Trevisan, Vilmar}
+\index{Martins, Luiz Felipe}
+\begin{chunk}{axiom.bib}
+@article{Webe05a,
+ author = "Weber, Kenneth and Trevisan, Vilmar and Martins, Luiz Felipe",
+ title = {{A Modular Integer GCD Algorithm}},
+ journal = "J. of Algorithms",
+ volume = "54",
+ year = "2005",
+ pages = "152167",
+ abstract =
+ "This paper describes the first algorithm to compute the greatest
+ common divisor (GCD) of two $n$bit integers using a modular
+ representation for intermediate values $U$, $V$ and also for the
+ result. It is based on a reduction step, similar to one used in
+ the accelerated algorithm when $U$ and $V$ are close to the same
+ size, that replaces $U$ by $(UbV)/p$, where $p$ is one of the
+ prime moduli and $b$ is the unique integer in the interval
+ $(p/2,p/2)$ such that $b\equiv UV^{1} (mod~p)$. When the
+ algorithm is executed on a bit common CRCW PRAM with
+ $O(n~log~n~log~log~log~n)$ processors, it takes $(O(n)$ time in
+ the worst case. A heuristic model of the average case yields
+ $O(n/log~n)$ time on the same number of processors.",
+ paper = "Webe05a.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Wehr, Stefan}
\begin{chunk}{axiom.bib}
@phdthesis{Wehr05,
@@ 18823,7 +20167,44 @@ when shown in factored form.
\end{chunk}
\section{Proving Axiom Correct  Coercion in CASProof Systesms} %
+\index{Zengler, Christoph}
+\index{Kubler, Andreas}
+\index{Kuchlin, Wolfgang}
+\begin{chunk}{axiom.bib}
+@article{Zeng11,
+ author = "Zengler, Christoph and Kubler, Andreas and Kuchlin, Wolfgang",
+ title = {{New Approaches to Boolean Quantifier Elimination}},
+ journal = "ACM Comm. in Computer Algebra",
+ volume = "45",
+ number = "2",
+ year = "2011",
+ abstract =
+ "We present four different approaches for existential Boolean
+ quantifier elimination, based on model enumeration, resolution,
+ knowledge compilation with projection, and substitution. We point out
+ possible applications in the area of verification and we present
+ preliminary benchmark results of the different approaches.",
+ paper = "Zeng11.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Zhang, Ting}
+\begin{chunk}{axiom.bib}
+@misc{Zhan02,
+ author = "Zhang, Ting",
+ title = {{A Survey of Quantifier Elimination: Syntactic and Semantic
+ Approaches}},
+ year = "2002",
+ link = "\url{http://theory.stanford.edu/~tingz/talks/qe.ps}",
+ paper = "Zhan02.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\section{Proving Axiom Sane  Coercion in CASProof Systesms} %
\index{Sozeau, Matthieu}
\begin{chunk}{axiom.bib}
@@ 28950,11 +30331,15 @@ AddisonWesly, New York, 3rd edition 1993
\end{chunk}
\index{Lichtblau, Daniel}
\begin{chunk}{ignore}
\bibitem[Lichtblau 11]{Lich11} Lichtblau, Daniel
 title = {{Symbolic definite (and indefinite) integration: methods and
 open issues}},
ACM Comm. in Computer Algebra Issue 175, Vol 45, No.1 (2011)
+\begin{chunk}{axiom.bib}
+@article{Lich11,
+ author = "Lichtblau, Daniel",
+ title = {{Symbolic Definite (and Indefinite) Integration: Methods and
+ Open Issues}},
+ journal = "ACM Comm. in Computer Algebra",
+ volume = "45",
+ number = "1",
+ year = "2011",
link = "\url{http://www.sigsam.org/bulletin/articles/175/issue175.pdf}",
abstract = "
The computation of definite integrals presents one with a variety of
@@ 28967,6 +30352,7 @@ ACM Comm. in Computer Algebra Issue 175, Vol 45, No.1 (2011)
ways. Herein we discuss these various issues and illustrate
with examples.",
paper = "Lich11.pdf"
+}
\end{chunk}
@@ 34366,6 +35752,33 @@ Proc ISSAC 97 pp172175 (1997)
\end{chunk}
+\index{Huang, Zongyan}
+\index{England, Matthew}
+\index{Wilson, David}
+\index{Davenport, James H.}
+\index{Paulson, Lawrence C.}
+\begin{chunk}{axiom.bib}
+@article{Huan14,
+ author = "Huang, Zongyan and England, Matthew and Wilson, David and
+ Davenport, James H. and Paulson, Lawrence C.",
+ title = {{A Comparison of Three Heuristics to Choose the Variable
+ Ordering for Cylindrical Algebraic Decomposition}},
+ journal = "ACM Comm. in Computer Algebra",
+ volume = "48",
+ number = "3",
+ year = "2014",
+ abstraact =
+ "Cylindrical algebraic decomposition (CAD) is a key tool for problems
+ in real algebraic geometry and beyond. When using CAD there is often a
+ choice over the variable ordering to use, with some problems
+ infeasible in one ordering but simple in another. Here we discuss a
+ recent experiment comparing three heuristics for making this choice on
+ thousands of examples.",
+ paper = "Huan14.pdf"
+}
+
+\end{chunk}
+
\subsection{J} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Jovanovic, Dejan}
@@ 35854,6 +37267,42 @@ Proc ISSAC 97 pp172175 (1997)
\section{To Be Classified} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Bozman, Gerald}
+\index{Buco, William}
+\index{Daly, Timothy}
+\index{Tetzlaff, William}
+\begin{chunk}{axiom.bib}
+@article{Bozm84,
+ author = "Bozman, Gerald and Buco, William and Daly, Timothy and
+ Tetzlaff, William",
+ title = {{Analysis of Free Storage Algorithms  Revisited}},
+ journal = "IBM Systems Journal",
+ volume = "23",
+ number = "1",
+ year = "1984",
+ abstract =
+ "Most research in freestorage management has centered around
+ strategies that search a linked list and strategies that partition
+ storage into predetermined sizes. Such algorithms are analyzed in
+ terms of CPU efficiency and storage efficiency. The subject of this
+ study is the freestorage management in the Virtual Machine/System
+ Product (VM/SP) system control program. As a part of this study,
+ simulations were done of established, and proposed, dynamic storage
+ algorithms for the VM/SP operating system. Empirical evidence is given
+ that simplifying statistical assumptions about the distribution of
+ interarrival times and holding times has high predictive
+ ability. Algorithms such as firstfit, modified firstfit, and
+ bestfit are found to be CPUinefficient. Buddy systems are found to
+ be very fast but suffer from a high degree of internal
+ fragmentation. A form of extended subpooling is shown to be as fast as
+ buddy systems with improved storage efficiency. This algorithm was
+ implemented for VM/SP, and then measured. Results for this algorithm
+ are given for several production VM/SP systems.",
+ paper = "Bozm84.pdf"
+}
+
+\end{chunk}
+
\index{Calmet, J.}
\index{Campbell, J.A.}
\begin{chunk}{axiom.bib}
@@ 42048,11 +43497,14 @@ Coding Theory and Applications Proceedings. SpringerVerlag, Berlin, Germany
\end{chunk}
\index{Daly, Timothy}
\begin{chunk}{ignore}
\bibitem[Daly 03]{Dal03} Daly, Timothy
 title = {{The Axiom Wiki Website}},
 link = "\url{http://axiom.axiomdeveloper.org}",
+\begin{chunk}{axiom.bib}}
+@misc{Daly03,
+ author = "Daly, Timothy",
+ title = {{Axiom Website: http://axiomdeveloper.org}},
+ link = "\url{http://axiomdeveloper.org}",
keywords = "axiomref",
+ year = "2003"
+}
\end{chunk}
@@ 48753,7 +50205,7 @@ Draft September 5, 1988
covered in the survey, but different in many ways as well. Axiom,
Maxima, and SAGE, are the largest of the generalpurpose opensource
CASs.",
 keywords = "axiomref",
+ keywords = "axiomref, TPDref",
beebe = "Joyner:2008:OSC"
}
@@ 48882,6 +50334,42 @@ SIGSAM Communications in Computer Algebra, 157 2006
\end{chunk}
+\index{KandriRody, Abdelilah}
+\index{Kapur, Deepak}
+\index{Winkler, Franz}
+\begin{chunk}{axiom.bib}
+@inproceedings{Kand89,
+ author = "KandriRody, Abdelilah and Kapur, Deepak and Winkler, Franz",
+ title = {{KnuthBendix Procedure and Buchberger Algorithm  A Synthesis}},
+ booktitle = "ISSAC'89",
+ publisher = "ACM Press",
+ pages = "5567",
+ year = "1989",
+ isbn = "0897913256",
+ abstract =
+ "The KnuthBendix procedure for the completion of a rewrite rule
+ system and the Buchberger algorithm for computing a Groebner basis
+ of a polynomial ideal are very similar in two respects: they both
+ start wtih an arbitrary specification of an algebraic structure
+ (axioms for an equational theory and a basis for a polynomial
+ ideal, respectively) which is transformed to a very special
+ specification of this algebraic structure (a complete rewrite rule
+ system and a Groebner basis of the polynomial ideal, respectively).
+ This special specification allows to decide many problems concerning
+ the given algebraic structure. Moreover, both algorithms achieve
+ their goals by employing the same basic concepts: formation of
+ critical pairs and completion.
+
+ Although the two methods are obviously related, the exact nature
+ of this relation remains to be clarified. Based on previous work
+ we show how the KnuthBendix procedure and the Buchberger algorithm
+ can be seen as special cases of a more general completion procedure.",
+ paper = "Kand89.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Kanigel, Robert}
\begin{chunk}{axiom.bib}
@misc{Kani16,
@@ 52501,7 +53989,7 @@ interactive computing, Brunel University, Uxbridge, England, 47 September
This exhibit includes a laptop computer running a recent version
of Axiom, Internet access (if available) to the Axiom Wiki website[4],
and CDs containing Axiom software for free distribution[5].",
 keywords = "axiomref",
+ keywords = "axiomref, TPDref",
beebe = "Page:2007:AOS"
}
@@ 52707,8 +54195,8 @@ Computers and Mathematics November 1993, Vol 40, Number 9 pp12031210
\begin{chunk}{axiom.bib}
@InProceedings{Prit06,
author = "Pritchard, F. Leon and Sit, William Y.",
 title = {{On initial value problems for ordinary differentialalgebraic
 equations}},
+ title = {{On Initial Value Problems for Ordinary DifferentialAlgebraic
+ Equations}},
booktitle = "Radon Series on Computational and Applied Mathematics",
year = "2006",
pages = "283340",
@@ 52732,7 +54220,7 @@ Computers and Mathematics November 1993, Vol 40, Number 9 pp12031210
algebraic index of the system, defined as the number of steps taken
by the process to stabilize. Over and underdetermined systems are
also accommodated in their framework.",
 keywords = "axiomref"
+ keywords = "axiomref, TPDref"
}
\end{chunk}
@@ 55104,30 +56592,6 @@ IBM Manual, March 1988
\end{chunk}
\index{Sutor, Robert S.}
\begin{chunk}{axiom.bib}
 author = "R. D. Jenks R. S. Sutor and S. M. Watt",
 title = {{Scratchpad II: An abstract Datatype system for
 mathematical computation}},
 pages = "1237",
 year = "1988"
}
\end{chunk}

\begin{chunk}{Sutor:1988:SIA}
@InProceedings{Sutor:1988:SIA,
 author = "R. D. Jenks R. S. Sutor and S. M. Watt",
 title = {{Scratchpad II: An abstract Datatype system for
 mathematical computation}},
 crossref = "Janssen:1988:TCA",
 pages = "12??",
 year = "1988",
 bibsource = "/usr/local/src/bib/bibliography/Theory/Comp.Alg.1.bib;
 http://www.math.utah.edu/pub/tex/bib/axiom.bib",
}

\end{chunk}

\begin{chunk}{axiom.bib}
@misc{Swmath,
author = "Unknown",
@@ 56629,6 +58093,41 @@ LCCN QA76.7.S54 v22:7 SIGPLAN Notices, vol 22, no 7 (July 1987)
\index{Winkler, Franz}
\begin{chunk}{axiom.bib}
+@inproceedings{Wink85,
+ author = "Winkler, Franz",
+ title = {{Reducing the Complexity of the KnuthBendix Completion
+ Algorithm: A ``Unification'' of Different Approaches}},
+ booktitle = "European Conference on Computer Algebra (EUROCAL 85)",
+ pages = "378389",
+ publisher = "Springer",
+ year = "1985",
+ isbn = "9783540159834",
+ abstract =
+ "The KnuthBendix completion procedure for rewrite rule systems is
+ of wide applicability in symbolic and algebraic computation.
+ Attempts to reduce the complexity of this completion algorithm are
+ reported in the literature. Already in their seminal 1967 paper
+ D.E. Knuth and P.B. Bendix have suggested to keep all the rules
+ iterreduced during the execution of the algorithm. G. Huet has
+ presented a version of the completion algorithm in which every
+ rewrite rule is kept in reduced form with respect to all the other
+ rules in the system. Borrowing an idea of Buchberger's for the
+ completion of bases of polynomial ideals the author has proposed
+ in 1983 a criterion for detecting ``unnecessary'' critical
+ pairs. If a critical pair is recognized as unnecessary then one
+ need not apply the costly process of computing normal forms to
+ it. It has been unclear whether these approaches can be
+ combined. We demonstrate that it is possible to keep all the
+ rewrite rules interreduced and still use a criterion for
+ eliminating unnecessary critical pairs.",
+ paper = "Wink85.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Winkler, Franz}
+\begin{chunk}{axiom.bib}
@misc{Wink89,
author = "Winkler, Franz",
title = {{Equational Theorem Proving and Rewrite Rule Systems}},
@@ 56663,7 +58162,40 @@ LCCN QA76.7.S54 v22:7 SIGPLAN Notices, vol 22, no 7 (July 1987)
We show how rewrite systems can be used for proving theorems in
equational and inductive theories, and how an equational specification
of a problem can be turned into a rewrite program.",
 paper = "Wink89.pdf"
+ paper = "Wink89.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Winkler, Franz}
+\begin{chunk}{axiom.bib}
+@inbook{Wink90,
+ author = "Winkler, Franz",
+ title = {{Solution of Equations I: Polynomial Ideals and Grobner Bases}},
+ booktitle = "Computers in Mathematics",
+ year = "1990",
+ publisher = "Marcel Dekker, Inc",
+ pages = "383407",
+ isbn = "0824783417",
+ paper = "Wink90.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Winkler, Franz}
+\begin{chunk}{axiom.bib}
+@misc{Wink93a,
+ author = "Winkler, Franz",
+ title = {{Computer Algebra}},
+ booktitle = "Concise Encyclopedia of Computer Science",
+ year = "1993",
+ publisher = "Wiley",
+ isbn = "0470090952",
+ pages = "227231",
+ paper = "Wink93a.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 56675,7 +58207,8 @@ LCCN QA76.7.S54 v22:7 SIGPLAN Notices, vol 22, no 7 (July 1987)
title = {{Algebraic Computation in Geometry}},
year = "1993",
journal = "IMACS Symposium SC1993",
 link = "\url{http://www.risc.jku.at/publications/download/risc_3777/paper_35.pdf}",
+ link =
+ "\url{http://www.risc.jku.at/publications/download/risc_3777/paper_35.pdf}",
abstract =
"Computation with algebraic curves and surfaces are very well suited
for being treated with computer algebra. Many aspects of computer
@@ 56693,6 +58226,20 @@ LCCN QA76.7.S54 v22:7 SIGPLAN Notices, vol 22, no 7 (July 1987)
\index{Winkler, Franz}
\begin{chunk}{axiom.bib}
+@inproceedings{Wink95,
+ author = "Winkler, Franz",
+ title = {{Computer Algebra  Problems and Developments}},
+ booktitle = "Computers in Industry 2 (SCAFI'92)",
+ pages = "117",
+ year = "1995",
+ isbn = "9780471955290",
+ paper = "Wink95.pdf"
+}
+
+\end{chunk}
+
+\index{Winkler, Franz}
+\begin{chunk}{axiom.bib}
@book{Wink96,
author = "Winkler, Franz",
title = {{Polynomial Algorithms in Computer Algebra}},
@@ 56724,7 +58271,62 @@ LCCN QA76.7.S54 v22:7 SIGPLAN Notices, vol 22, no 7 (July 1987)
The book was originally developed from course material. It can easily
be used as a textbook on the topic. Most subsections contain
 exercises. Solutions of some of the exercises are provided."
+ exercises. Solutions of some of the exercises are provided.",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
+\index{Winkler, Franz}
+\begin{chunk}{axiom.bib}
+@techreport{Wink99,
+ author = "Winkler, Franz",
+ title = {{Advances and Problems in Algebraic Computation}},
+ type = "technical report",
+ number = "9949",
+ year = "1999",
+ institution = "RISC, Linz",
+ abstract =
+ "In the last years there has been dramatic progress in all areas
+ of algebraic computation. Many working mathematiians have access
+ to and actually use algebraic software systems for their research
+ No end of this development is in sight. We report on some active
+ topics in algebraic computation, namely the theory of integration
+ and symbolic solution of systems of differential equations, the
+ solution of systems of algebraic equations, the factorization of
+ polynomials, and the design and analysis of algebraic curves and
+ surfaces.",
+ paper = "Wink99.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Winkler, Franz}
+\begin{chunk}{axiom.bib}
+@inproceedings{Wink06,
+ author = "Winkler, Franz",
+ title = {{Computer Algebra and Geometry  Some Interactions}},
+ booktitle = "Proc. of Coll. on Constructive Algebra and System
+ Theory (CAST)",
+ year = "2006",
+ publisher = "unknown",
+ isbn = "906984477x",
+ pages = "127138",
+ abstract =
+ "Algebraic curves and surfaces have been studied intensively in
+ algebraic geometry for centuries. Thus, there exists a huge amount
+ of theoretical knowledge about these geometric objects. Recently,
+ algebraic curves and surfaces play an important and ever
+ increasing role in computer aided geometric design, computer
+ vision, computer aided manufacturing, coding theory, and
+ cryptography, just to name a few application areas. Consequently,
+ theoretical results need to be adapted to practical needs. We need
+ efficient algorithms for generating, representing, manipulating,
+ analyzing, rendering algebraic curves and surfaces. Exact computer
+ algebraic methods can be employed effectively for dealing with
+ these geometric problems.",
+ paper = "Wink06.pdf"
}
\end{chunk}
@@ 59453,7 +61055,8 @@ Princeton University Press. (1963)
I hope that it will become clear that many operations that are often
regarded as effective, are in fact not so; while many operations that
might not be regarded as effective in fact are.",
 paper = "Dave81b.pdf"
+ paper = "Dave81b.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 62187,7 +63790,8 @@ Springer Verlag Heidelberg, 1989, ISBN 0387969802
verification framework, the Maple package DifferenceDifferential
developed at our institute to compute bivariate differencedifferential
polynomials using relative Gr ̈obner bases.",
 paper = "Khan13.pdf"
+ paper = "Khan13.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 65315,11 +66919,16 @@ Software Practice and Experience. 6(1) (1976)
\end{chunk}
\begin{chunk}{axiom.bib}
@misc{SCSCP,
+@article{SCSCP,
author = "The SCSCP development team",
title = {{Symbolic Computation Software Composability Protocol}},
+ journal = "Communications in Computer Algebra",
+ volume = "44",
+ number = "4",
link = "\url{https://gappackages.github.io/scscp/}",
 year = "2017"
+ year = "2010",
+ paper = "SCSCP.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 66190,20 +67799,6 @@ Linear Algebra and Appl. 28 285303. 1979
\end{chunk}
\index{Winkler, Franz}
\begin{chunk}{axiom.bib}
@misc{Wink95,
 author = "Winkler, Franz",
 title = {{Computer Algebra  Problems and Developments}},
 year = "1995",
 abstract =
 "Recent developments in computer algebra are discussed using simple
 but illustrative examples",
 paper = "Wink95.pdf"
}

\end{chunk}

\index{Wisbauer, R.}
\begin{chunk}{ignore}
\bibitem[Wisbauer 91]{Wis91} Wisbauer, R.
diff git a/changelog b/changelog
index c14ed1e..cdb997f 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20180811 tpd src/axiomwebsite/patches.html 20180811.01.tpd.patch
+20180811 tpd books/bookvolbib add references
20180717 tpd src/axiomwebsite/patches.html 20180717.01.tpd.patch
20180717 tpd src/axiomwebsite/documentation.html redirect downloads to github
20180714 tpd src/axiomwebsite/patches.html 20180714.01.tpd.patch
diff git a/patch b/patch
index ba04cd1..e9e6b12 100644
 a/patch
+++ b/patch
@@ 63,3 +63,1533 @@ Goal: Proving Axiom Sane
}
\end{chunk}
+
+\index{KandriRody, Abdelilah}
+\index{Kapur, Deepak}
+\index{Winkler, Franz}
+\begin{chunk}{axiom.bib}
+@inproceedings{Kand89,
+ author = "KandriRody, Abdelilah and Kapur, Deepak and Winkler, Franz",
+ title = {{KnuthBendix Procedure and Buchberger Algorithm  A Synthesis}},
+ booktitle = "ISSAC'89",
+ publisher = "ACM Press",
+ pages = 5567",
+ year = "1989",
+ isbn = "0897913256",
+ abstract =
+ "The KnuthBendix procedure for the completion of a rewrite rule
+ system and the Buchberger algorithm for computing a Groebner basis
+ of a polynomial ideal are very similar in two respects: they both
+ start wtih an arbitrary specification of an algebraic structure
+ (axioms for an equational theory and a basis for a polynomial
+ ideal, respectively) which is transformed to a very special
+ specification of this algebraic structure (a complete rewrite rule
+ system and a Groebner basis of the polynomial ideal, respectively).
+ This special specification allows to decide many problems concerning
+ the given algebraic structure. Moreover, both algorithms achieve
+ their goals by employing the same basic concepts: formation of
+ critical pairs and completion.
+
+ Although the two methods are obviously related, the exact nature
+ of this relation remains to be clarified. Based on previous work
+ we show how the KnuthBendix procedure and the Buchberger algorithm
+ can be seen as special cases of a more general completion procedure.",
+ paper = "Kand89.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Winkler, Franz}
+\begin{chunk}{axiom.bib}
+@misc{Wink92,
+ author = "Winkler, Franz",
+ title = {{Computer Algebra}},
+ booktitle = "Encyclopedia of Physical Science and Technology",
+ volume = "4",
+ year = "1992",
+ publisher = "Academic Press",
+ paper = "Wink92.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Winkler, Franz}
+begin{chunk}{axiom.bib}
+@inproceedings{Wink95,
+ author = "Winkler, Franz",
+ title = {{Computer Algebra  Problems and Developments}},
+ booktitle = "Computers in Industry 2 (SCAFI'92)",
+ pages = "117",
+ year = "1995",
+ isbn = "9780471955290",
+ paper = "Wink95.pdf"
+}
+
+\end{chunk}
+
+\index{Winkler, Franz}
+\begin{chunk}{axiom.bib}
+@techreport{Wink99,
+ author = "Winkler, Franz",
+ title = {{Advances and Problems in Algebraic Computation}},
+ type = "technical report",
+ number = "9949",
+ year = "1999",
+ institution = "RISC, Linz",
+ abstract =
+ "In the last years there has been dramatic progress in all areas
+ of algebraic computation. Many working mathematiians have access
+ to and actually use algebraic software systems for their research
+ No end of this development is in sight. We report on some active
+ topics in algebraic computation, namely the theory of integration
+ and symbolic solution of systems of differential equations, the
+ solution of systems of algebraic equations, the factorization of
+ polynomials, and the design and analysis of algebraic curves and
+ surfaces.",
+ paper = "Wink99.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Winkler, Franz}
+\begin{chunk}{axiom.bib}
+@inproceedings{Wink06,
+ author = "Winkler, Franz",
+ title = {{Computer Algebra and Geometry  Some Interactions}},
+ booktitle = "Proc. of Coll. on Constructive Algebra and System
+ Theory (CAST)",
+ year = "2006",
+ publisher = "unknown",
+ isbn = "906984477x",
+ pages = "127138",
+ abstract =
+ "Algebraic curves and surfaces have been studied intensively in
+ algebraic geometry for centuries. Thus, there exists a huge amount
+ of theoretical knowledge about these geometric objects. Recently,
+ algebraic curves and surfaces play an important and ever
+ increasing role in computer aided geometric design, computer
+ vision, computer aided manufacturing, coding theory, and
+ cryptography, just to name a few application areas. Consequently,
+ theoretical results need to be adapted to practical needs. We need
+ efficient algorithms for generating, representing, manipulating,
+ analyzing, rendering algebraic curves and surfaces. Exact computer
+ algebraic methods can be employed effectively for dealing with
+ these geometric problems.",
+ paper = "Wink06.pdf"
+}
+
+\end{chunk}
+
+\index{Davies, Rowan}
+\index{Pfenning, Frank}
+\begin{chunk}{axiom.bib}
+@article{Davi01,
+ author = "Davies, Rowan and Pfenning, Frank",
+ title = {{A Modal Analysis of Staged Computation}},
+ journal = "J. ACM",
+ volume = "48",
+ number = "3",
+ pages = "555604",
+ year = "2001",
+ abstract =
+ "We show that a type system based on the intuitionistic modal logic S4
+ provides an expressive framework for specifying and analyzing
+ computation stages in the context of typed $\lambda$calculi and
+ functional languages. We directly demonstrate the sense in which our
+ $\lambda_e^{\rightarrow\box}$calculus captures staging, and also give
+ a conservative embedding of Nielson and Nielson's twolevel functional
+ language in our functional language MiniML${}^\box$, thus proving that
+ bindingtime correctness is equivalent to modal correctness on this
+ fragment. In addition, MiniML${}^\box$ can also express immediate
+ evaluation and sharing of code across multiple stages, thus supporting
+ runtime code generation as well as partial evaluation.",
+ paper = "Davi01.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Pfenning, Frank}
+\index{Davies, Rowan}
+\begin{chunk}{axiom.bib}
+@article{Pfen01,
+ author = "Pfenning, Frank and Davies, Rowan",
+ title = {{A Judgemental Reconstruction of Modal Logic}},
+ journal = "Mathematical Structures in Computer Science",
+ volume = "11",
+ pages = "511540",
+ year = "2001",
+ abstract =
+ "We reconsider the foundations of modal logic, following MartinLof's
+ methodology of distinguishing judgments from propositions. We give
+ constructive meaning explanations for necessity and possibility which
+ yields a simple and uniform system of natural deduction for
+ intuitionistic modal logic which does not exhibit anomalies found in
+ other proposals. We also give a new presentation of lax logic and nd
+ that the lax modality is already expressible using possibility and
+ necessity. Through a computational interpretation of proofs in modal
+ logic we further obtain a new formulation of Moggi's monadic
+ metalanguage.",
+ paper = "Pfen01.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Lamport, Leslie}
+\begin{chunk}{axiom.bib}
+@misc{Lamp03,
+ author = "Lamport, Leslie",
+ title = {{The Future of Computing: Logic or Biology}},
+ link =
+ "\url{https://lamport.azurewebsites.net/pubs/futureofcomputing.pdf}",
+ year = "2003",
+ paper = "Lamp03.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Glymour, Clark}
+\index{Serafin, Luke}
+\begin{chunk}{axiom.bib}
+@misc{Glym15,
+ author = "Glymour, Clark and Serafin, Luke",
+ title = {{Mathematical Metaphysics}},
+ link = "\url{http://shelf1.library.cmu.edu/HSS/2015/a1626190.pdf}",
+ year = "2015",
+ paper = "Glym15.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Reynolds, John C.}
+\begin{chunk}{axiom.bib}
+@article{Reyn93,
+ author = "Reynolds, John C.",
+ title = {{The Discoveries of Continuations}},
+ journal = "Lisp and Symbolic Computation",
+ volume = "6",
+ pages = "233248",
+ year = "1993",
+ abstract =
+ "We give a brief account of the discoveries of continuations and
+ related concepts.",
+ paper = "Reyn93.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Oles, Frank Joseph}
+\begin{chunk}{axiom.bib}
+@phdthesis{Oles82,
+ author = "Oles, Frank Joseph",
+ title = {{A CategoryTheoretic Approach to the Semantics of
+ Programming Languages}},
+ school = "Syracuse University",
+ year = "1982",
+ abstract =
+ "Here we create a framework for handling the semantics of fully
+ typed programming languages with imperative features, higherorder
+ ALGOLlike procedures, block structure, and implicit
+ conversions. Our approach involves introduction of a new family of
+ programming languages, the {\sl coercive typed $\lambda$calculi},
+ denoted by $L$ in the body of the dissertation. By appropriately
+ choosing the linguistic constants (i.e. generators) of $L$, we can
+ view phrases of variants of ALGOL as syntactically sugared phrases
+ of $L$.
+
+ This dissertation breaks into three parts. In the first part,
+ consisting of the first chapter, we supply basic definitions and
+ motivate the idea that functor categories arise naturally in the
+ explanation of block structure and stack discipline. The second
+ part, consisting of the next three chapters, is dedicated to the
+ general theory of the semantics of the coercive typed
+ $\lambda$calculus; the interplay between posets, algebras, and
+ Cartesian closed categories is particularly intense here. The
+ remaining four chapters make up the final part, in which we apply
+ the general theory to give both direct and continuation semantics
+ for desugared variants of ALGOL. To do so, it is necessary to show
+ certain functor categories are Cartesian closed and to describe a
+ category $\Sigma$ of store shapes. An interesting novelty in the
+ presentation of continuation semantics is the view that commands
+ form a procedural, rather than a primitive, phrase type.",
+ paper = "Oles82.pdf"
+}
+
+\end{chunk}
+
+\index{Abdali, S. Kamal}
+\index{Winkler, Franz}
+\begin{chunk}{axiom.bib}
+@techreport{Abda81,
+ author = "Abdali, S. Kamal and Winkler, Franz",
+ title = {{A LambdaCalculus Model for Generating Verification Conditions}},
+ type = "technical report",
+ institution = "Rensselaer Polytechnic Institute",
+ number = "CS8104",
+ year = "1981",
+ abstract =
+ "A lambdacalculusbased method is developed for the automatic
+ generation of verification conditions. A programming language is
+ specified in which inductive assertions associated with a program
+ are incorporated within the body of the program by means of assert
+ and maintainwhile statements. This programming language includes
+ the following features: assignments, conditionals, loops,
+ compounds, ALGOLtype block structure. A model is developed which
+ consists of rules to translate each statement in this programming
+ language into the lambacalculus. The model is such that the
+ lambdaexpression translation of any program reduces to a list
+ (tuple) of lambdaexpression representations of all verification
+ conditions of the program. A proof of this property is given.",
+ paper = "Abda81.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Abdali, S. Kamal}
+\begin{chunk}{axiom.bib}
+@book{Abda73,
+ author = "Abdali, S. Kamal",
+ title = {{A Simple LambdaCalculus Model of Programming Languages}},
+ isbn = "9781332196029",
+ publisher = "Forgotten Books",
+ year = "1973",
+ abstract =
+ "We present a simple correspondence between a large subset of
+ ALGOL 60 language and lambdacalculus. With the aid of this
+ correspondence, a program can be translated into a single
+ lambdaexpression. In general, the representation of a program is
+ specified by means of a system of simultaneous conversion
+ relations among the representations of the program
+ constituents. Highlevel programming language features are treated
+ directly, not in terms of the representations of machinelevel
+ operations. The model includes inputoutput in such a way that
+ when the representation of a (convergent) program is applied to
+ the input item representations, the resulting combination reduces
+ to a tuple of the representations of the output items. This model
+ does not introduce any imperative notions into the calculus; the
+ descriptive programming constructs, such as expressions, and the
+ imperative ones, such as assignment and jumps, are translated
+ alike into pure lambda expressions. The applicability of the model
+ to the problems of proving program equivalence and correctness is
+ illustrated by means of simple examples."
+ paper = "Abda73.pdf"
+}
+
+\end{chunk}
+
+\index{Abdali, S. Kamal}
+\begin{chunk}{axiom.bib}
+@article{Abda74,
+ author = "Abdali, S. Kamal",
+ title = {{A LambdaCalculus Model of Programming Languages 
+ I. Simple Constructs}},
+ journal = "J. of Computer Languages",
+ volume = "1",
+ pages = "287301",
+ year = "1974",
+ abstract =
+ "A simple correspondence is presented between the elementary
+ constructs of programming languages and the lambdacalculus. The
+ correspondence is obtained by using intuitive, functional
+ interpretation of programming language constructs, completely
+ avoiding the notions of machine memory and address. In particular,
+ the concepts of program variable and assignments are accounted for
+ in terms of the concepts of mathematical variable and
+ substitution, respectively. Lambdaexpression representations are
+ given of assignments, conditional and compound statements,
+ inputoutput, and blocks. Algol 60 is used as the illustrative
+ language.",
+ paper = "Abda74.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Abdali, S. Kamal}
+\begin{chunk}{axiom.bib}
+@article{Abda74a,
+ author = "Abdali, S. Kamal",
+ title = {{A LambdaCalculus Model of Programming Languages 
+ II. Jumps and Procedures}},
+ journal = "J. of Computer Languages",
+ volume = "1",
+ pages = "303320",
+ year = "1974",
+ abstract =
+ "The correspondence between programming languages and the
+ lambdacalculus presented in Part I of the paper is extended there
+ to include iteration statements, jumps, and procedures. Programs
+ containing loops are represented by lambdaexpressions whose
+ components are specified recursively by means of systems of
+ simultaneous conversion relations. The representation of
+ callbyname and sideeffects in a program is accomplished without
+ any resort to the concepts of memory andaddress by making use of a
+ number of variables in addition to those declared by the programs;
+ with the aid of these additional variables, the parameter linkage
+ operations can be simulated by pure substitution. The
+ applicability of the model to the problems of proving program
+ correctness and equivalence is demonstrated by means of examples.",
+ paper = "Abda74a.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Abdali, S. Kamal}
+\begin{chunk}{axiom.bib}
+@phdthesis{Abda74b,
+ author = "Abdali, S. Kamal",
+ title = {{A Combinatory Logic Model of Programming Languages}},
+ school = "University of Wisconsin",
+ year = "1974",
+ abstract =
+ "A simple correspondence is presented between a large subset of the
+ ALGOL 60 language and the combinatory logic. With the aid of this
+ correspondence, a program can be translated into a single combinatory
+ object. The combinatory object representing a program is specified,
+ in general, by means of a system of reduction relations among the
+ representations of the program constituents. This object denotes, in
+ terms of the combinatory logic, the function that the program is
+ intended to compute.
+
+ The model has been derived by using intuitive, functional
+ interpretations of the constructs of programming languages, completely
+ avoiding the notions of machine command and address. In particular,
+ the concepts of program variable, assignment, and procedure have been
+ accounted for in terms of the concepts of mathematical variable,
+ substitution, and function, respectively.
+
+ Highlevel programming language features are represented in the
+ combinatory logic directly, not in terms of the representations of
+ machinelevel operations. Inputoutput is treated in such a
+ manner that when the representation of a program is applied to the
+ representations of the input items, the resulting combination reduces
+ to a tuple of the representations of the output items.
+
+ The applicability of the model to the problems of
+ proving program equivalence and correctness is illustrated
+ by means of examples.",
+ paper = "Abda74b.pdf"
+}
+
+\end{chunk}
+
+\index{Krall, Andreas}
+\begin{chunk}{axiom.bib}
+@misc{Kralxx,
+ author = "Krall, Andreas",
+ title = {{Implementation Techniques for Prolog}},
+ link = "\url{https://pdfs.semanticscholar.org/fdbf/aa46bf6ab2148595f638fe9afe97033583ee.pdf}",
+ year = "unknown",
+ abstract =
+ "This paper is a short survey about currently used implementation
+ techniques for Prolog. It gives an introduction to unification and
+ resolution in Prolog and presents the memory model and a basic
+ execution model. These models are expanded to the Vienna Abstract
+ Machine (VAM) with its two versions, the VAM${}_{2p}$ and the
+ VAM${}_{1p}$, and the most famous abstract machine, the Warren
+ Abstract Machine (WAM). The continuation passing style model of
+ Prolog, binary Prolog, leands to the BinWAM. Abstract
+ interpretation can be applied to gather information about a
+ program. This information is used in the generation of very
+ specialized machine code and in optimizations like clause indexing
+ and instruction scheduling on each kind of abstract machine.",
+ paper = "Kralxx.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Abadi, Martin}
+\index{Cardelli, Luca}
+\index{Curien, PierreLouis}
+\index{Levy, JeanJacques}
+\begin{chunk}{axiom.bib}
+@inproceedings{Abad90,
+ author = "Abadi, Martin and Cardelli, Luca and Curien, PierreLouis
+ and Levy, JeanJacques",
+ title = {{Explicit Substitutions}},
+ booktitle = "Symp. of Principles of Programming Languages",
+ publisher = "ACM",
+ year = "1990",
+ link = "\url{http://www.hpl.hp.com/techreports/CompaqDEC/SRCRR54.pdf}",
+ abstract =
+ "The $lambda\sigma$calculus is a refinement of the
+ $lambda$calculus where substitutions are manipulated
+ explicitly. The $\lambda\sigma$calculus provides a setting for
+ studying the theory of substitutions, with pleasant mathematical
+ properties. It is also a useful bridge between the classical
+ $\lambda$calculus and concrete implementations.",
+ paper = "Abad90.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Beeson, Michael}
+\begin{chunk}{axiom.bib}
+@article{Bees80a,
+ author = "Beeson, Michael",
+ title = {{Formalizing Constructive Mathematics: Why and How?}},
+ journal = "Lecture Notes in Mathematics",
+ volume = "873",
+ pages = "146190",
+ year = "1980",
+ paper = "Bees80a.pdf"
+}
+
+\end{chunk}
+
+\index{Goodman, Nicolas D.}
+\begin{chunk}{axiom.bib}
+@article{Good80,
+ author = "Goodman, Nicolas D.",
+ title = {{Reflections on Bishop's Philosophy of Mathematics}},
+ journal = "Lecture Notes in Mathematics",
+ volume = "873",
+ pages = "135145",
+ year = "1980",
+ paper = "Good80.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Rosenkranz, Markus}
+\begin{chunk}{axiom.bib}
+@book{Rose07,
+ author = "Rosenkranz, Markus",
+ title = {{Gr\"obner Bases in Symbolic Analysis}},
+ publisher = "Walter de Gruyter, Berlin Germany",
+ year = "2007",
+ isbn = "978311.0193237",
+ keywords = "axiomref, TPDref"
+}
+
+\end{chunk}
+
+\index{Daly, Timothy}
+\begin{chunk}{axiom.bib}
+@misc{Daly06,
+ author = "Daly, Timothy",
+ title = {{Literate Programming}},
+ link = "\url{http://lambdatheultimate.org/node/1336}",
+ year = "2006",
+ keywords = "axiomref, TPDref"
+}
+
+\end{chunk}
+
+\index{Prengel, Alex}
+\begin{chunk}{axiom.bib}
+@misc{Pren16,
+ author = "Prengel, Alex",
+ title = {{MIT axiommath_v8.14}},
+ link = "\url{http://web.mit.edu/axiommath_v8.14/}",
+ year = "2016",
+ keywords = "axiomref, TPDref"
+}
+
+\end{chunk}
+
+\index{Jenks, Richard D.}
+\begin{chunk}{axiom.bib}
+@article{Jenk11,
+ author = "Jenks, Richard D.",
+ title = {{The 2011 Richard D. Jenks Memorial Prize}},
+ journal = "ACM Communications in Computer Algebra",
+ volume = "45",
+ number = "4",
+ year = "2011",
+ abstract =
+ "The 2011 Richard D. Jenks Memorial Prize for Excellence in
+ Software Engineering Applied to Computer Algebra was presented by
+ members of the Prize Selection Committee and its chair, Erich
+ Kaltofen, at ISSAC and SNC in San Jose, CA, on June 9, 2011 to the
+ Maple Project at the University of Waterloo.",
+ paper = "Jenk11.pdf",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
+\index{Jenks, Richard D.}
+\begin{chunk}{axiom.bib}
+@article{Jenk13,
+ author = "Jenks, Richard D.",
+ title = {{The 2013 Richard D. Jenks Memorial Prize}},
+ journal = "ACM Communications in Computer Algebra",
+ volume = "47",
+ number = "4",
+ year = "2013",
+ abstract =
+ "The 2013 Richard D. Jenks Memorial Prize for Excellence in
+ Software Engineering Applied to Computer Algebra was announced by
+ members of the Prize Selection Committee, Mark Giesbrecht
+ representing its chair Erich Kaltofen, at ISSAC in Boston, MA, on
+ June 28, 2013 to have been awared to Professor William Arthur
+ Stein of the Sage Project at the University of Washington.",
+ paper = "Jenk13.pdf",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
+\index{Jenks, Richard D.}
+\begin{chunk}{axiom.bib}
+@article{Jenk15,
+ author = "Jenks, Richard D.",
+ title = {{The 2015 Richard D. Jenks Memorial Prize}},
+ journal = "ACM Communications in Computer Algebra",
+ volume = "49",
+ number = "4",
+ year = "2015",
+ abstract =
+ "The 2015 Richard D. Jenks Memorial Prize was awarded on October
+ 30, 2015 at the Fields Institute in Toronto during the Major
+ Thematic Program on Computer Algebra to Professor Victor Shoup for
+ NTL: A Library for doing Number Theory.",
+ paper = "Jenk15.pdf",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
+\index{Jenks, Richard D.}
+\begin{chunk}{axiom.bib}
+@article{Jenk17,
+ author = "Jenks, Richard D.",
+ title = {{The 2017 Richard D. Jenks Memorial Prize}},
+ journal = "ACM Communications in Computer Algebra",
+ volume = "51",
+ number = "4",
+ year = "2017",
+ abstract =
+ "The 2017 Richard D. Jenks Memorial Prize for Excellence in
+ Software Engineering Applied to Computer Algebra has been awarded
+ to Stephen Wolfram for WolframAlpha and Mathematica.",
+ paper = "Jenk17.pdf",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
+\index{Lazard, Daniel}
+\begin{chunk}{axiom.bib}
+@article{Laza01,
+ author = "Lazard, Daniel",
+ title = {{Solving Systems of Algebraic Equations}},
+ journal = "ACM SIGSAM Bulletin",
+ volume = "35",
+ number = "3",
+ year = "2001",
+ abstract =
+ "Let $f_1,\ldots,f_k$ be $k$ k multivariate polynomials which have
+ a finite number of common zeros in the algebraic closure of the ground
+ field, counting the common zeros at infinity. An algorithm is
+ given and proved which reduces the computations of these zeros to
+ the resolution of a single univariate equation whose degree is the
+ number of common zeros. This algorithm gives the whole algebraic
+ and geometric structure of the set of zeros (multiplicities,
+ conjugate zeros,...). When all the polynomials have the same degree,
+ the complexity of this algorithm is polynomial relative to the generic
+ number of solutions.",
+ paper = "Laza01.pdf"
+}
+
+\end{chunk}
+
+\index{Abramov, S.A.}
+\begin{chunk}{axiom.bib}
+@article{Abra00,
+ author = "Abramov, S.A.",
+ title = {{A Note on the Number of Division Steps in the Euclidean
+ Algorithm}},
+ journal = "ACM SIGSAM",
+ volume = "34",
+ number = "4",
+ year = "2000",
+ paper = "Abra00.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Essex, Christopher}
+\index{Davison, Matt}
+\index{Schulzky, Christian}
+\begin{chunk}{axiom.bib}
+@article{Esse00,
+ author = "Essex, Christopher and Davison, Matt and Schulzky, Christian",
+ title = {{Numerical Monsters}},
+ journal = "ACM SIGSAM",
+ volume = "34",
+ number = "4",
+ year = "2000",
+ abstract =
+ "When the results of certain computer calculations are shown to be not
+ simply incorrect but dramatically incorrect, we have a powerful reason
+ to be cautious about all computerbased calculations. In this paper we
+ present a 'Rogue's Gallery' of simple calculations whose correct
+ solutions are obvious to humans but whose numerical solutions are
+ incorrect in pathological ways. We call these calculations, which can
+ be guaranteed to wreak numerical mayhem across both software
+ packages and hardware platforms, 'Numerical Monsters'. Our monsters
+ can be used to provide deep insights into how computer calculations
+ fail, and we use t h e m to engender appreciation for the subject of
+ numerical analysis in our students. Although these monsters are based
+ on wellunderstood numerical pathologies, even experienced numerical
+ analysts will find surprises in their behaviour and ,can use the
+ lessons they bring to become even better masters of their tools.",
+ paper = "Esse00.pdf"
+}
+
+\end{chunk}
+
+\index{Buchberger, Bruno}
+\begin{chunk}{axiom.bib}
+@article{Buch02,
+ author = "Buchberger, Bruno",
+ title = {{Computer Algebra: The End of Mathematics?}},
+ journal = "ACM SIGSAM",
+ volume = "36",
+ number = "1",
+ year = "2002",
+ abstract =
+ "Mathematical software systems, such as Mathematica, Maple, Derive,
+ and so on, are substantially based on enormous advances in the area of
+ mathematics known as Computer Algebra or Symbolic Mathematics. In
+ fact, everything taught in high school and in the first semesters of a
+ university mathematical education, is available in these systems 'at
+ the touch of the button'. Will mathematics become unnecessary because
+ of this? In the three sections of this essay, I answer this question
+ for nonmathematicians, for mathematicians and for (future) students
+ of mathematics.",
+ paper = "Buch02.pdf"
+}
+
+\end{chunk}
+
+\index{Barnett, Michael P.}
+\begin{chunk}{axiom.bib}
+@article{Barn08,
+ author = "Barnett, Michael P.",
+ title = {{Reasoning in Symbolic Computation}},
+ journal = "ACM Communications in Symbolic Algebra",
+ volume = "42",
+ number = "1",
+ year = "2008",
+ abstract =
+ "I discuss notations for some styles of mathematical reasoning that
+ include analogy. These notations extend the conventions of the
+ mathematica package mathscape that I reported recently in the
+ Journal of Symbolic Computation. The paper introduces the reasoning
+ objects that I call 'precursors' and 'consequences lists'.",
+ paper = "Barn08.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Lichtblau, Daniel}
+\begin{chunk}{axiom.bib}
+@article{Lich11,
+ author = "Lichtblau, Daniel",
+ title = {{Symbolic Definite (and Indefinite) Integration: Methods and
+ Open Issues}},
+ journal = "ACM Comm. in Computer Algebra",
+ volume = "45",
+ number = "1",
+ year = "2011",
+ link = "\url{http://www.sigsam.org/bulletin/articles/175/issue175.pdf}",
+ abstract = "
+ The computation of definite integrals presents one with a variety of
+ choices. There are various methods such as NewtonLeibniz or Slater's
+ convolution method. There are questions such as whether to split or
+ merge sums, how to search for singularities on the path of
+ integration, when to issue conditional results, how to assess
+ (possibly conditional) convergence, and more. These various
+ considerations moreover interact with one another in a multitude of
+ ways. Herein we discuss these various issues and illustrate
+ with examples.",
+ paper = "Lich11.pdf"
+}
+
+\end{chunk}
+
+\index{Zengler, Christoph}
+\index{Kubler, Andreas}
+\index{Kuchlin, Wolfgang}
+\begin{chunk}{axiom.bib}
+@article{Zeng11,
+ author = "Zengler, Christoph and Kubler, Andreas and Kuchlin, Wolfgang",
+ title = {{New Approaches to Boolean Quantifier Elimination}},
+ journal = "ACM Comm. in Computer Algebra",
+ volume = "45",
+ number = "2",
+ year = "2011",
+ abstract =
+ "We present four different approaches for existential Boolean
+ quantifier elimination, based on model enumeration, resolution,
+ knowledge compilation with projection, and substitution. We point out
+ possible applications in the area of verification and we present
+ preliminary benchmark results of the different approaches.",
+ paper = "Zeng11.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Stoutemyer, David R.}
+\begin{chunk}{axiom.bib}
+@article{Stou11,
+ author = "Stoutemyer, David R.",
+ title = {{Ways to Implement Computer Algebra Compactly}},
+ journal = "ACM Comm. in Computer Algebra",
+ volume = "45",
+ number = "4",
+ year = "2011",
+ abstract =
+ "Computer algebra had to be implemented compactly to fit on early
+ personal computers and handheld calculators. Compact implementation
+ is still important for portable handheld devices. Also, compact
+ implementation increases comprehensibility while decreasing develop
+ ment and maintenance time and cost, regardless of the platform. This
+ article describes several ways to achieve compact implementations,
+ including:
+ \begin{itemize}
+ \item Exploit evaluation followed by interpolation to avoid
+ implementing a parser, such as in PicoMath
+ \item Use contiguous storage as an expression stack to avoid garbage
+ collection and pointerspace overhead, such as in Calculus Demon
+ and TIMathEngine
+ \item Use various techniques for saving code space for linkedstorage
+ representation of expressions and functions, such as muMath and Derive
+ \end{itemize}",
+ paper = "Stou11.pdf",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
+\index{Roche, Daniel S.}
+\begin{chunk}{axiom.bib}
+@article{Roch11,
+ author = "Roche, Daniel S.",
+ title = {{Chunky and EqualSpaced Polynomial Multiplication}},
+ journal = "J. Symbolic Computation",
+ volume = "46",
+ pages = "791806",
+ year = "2011",
+ abstract =
+ "Finding the product of two polynomials is an essential and basic
+ problem in computer algebra. While most previous results have
+ focused on the worstcase complexity, we instead employ the
+ technique of adaptive analysis to give an improvement in many
+ ‘‘easy’’ cases. We present two adaptive measures and methods
+ for polynomial multiplication, and also show how to effectively
+ combine them to gain both advantages. One useful feature of these
+ algorithms is that they essentially provide a gradient between
+ existing ‘‘sparse’’ and ‘‘dense’’ methods. We prove that these
+ approaches provide significant improvements in many cases but
+ in the worst case are still comparable to the fastest existing
+ algorithms.",
+ paper = "Roch11.pdf"
+}
+
+\end{chunk}
+
+\index{Bailey, David H.}
+\index{Borwein, Jonathan M.}
+\index{Kaiser, Alexander D.}
+\begin{chunk}{axiom.bib}
+@article{Bail14,
+ author = "Bailey, David H. and Borwein, Jonathan M. and
+ Kaiser, Alexander D.",
+ title = {{Automated Simplification of Large Symbolic Expressions}},
+ journal = "J. Symbolic Computation",
+ volume = "60",
+ pages = "120136",
+ year = "2014",
+ abstract =
+ "We present a set of algorithms for automated simplification of
+ symbolic constants of the form
+ $\sum_i\alpha_i x_i$ with $\alpha_i$ rational and $x_i$
+ complex. The included algorithms, called SimplifySum and
+ implemented in Mathematica , remove redundant terms, attempt to make
+ terms and the full expression real, and remove terms using repeated
+ application of the multipair PSLQ integer relation detection
+ algorithm. Also included are facilities for making substitutions
+ according to userspecified identities. We illustrate this toolset by
+ giving some realworld examples of its usage, including one, for
+ instance, where the tool reduced a symbolic expression of
+ approximately 100 000 characters in size enough to enable manual
+ manipulation to one with just four simple terms.",
+ paper = "Bail14.pdf"
+}
+
+\end{chunk}
+
+\index{Bailey, David H.}
+\index{Borwein, Jonathan M.}
+\begin{chunk}{axiom.bib}
+@article{Bail11,
+ author = "Bailey, David H. and Borwein, Jonathan M.",
+ title = {{Highprecision Numerical Integration: Progress and Challenges}},
+ journal = "J. Symbolic Computation",
+ number = "46",
+ pages = "741754",
+ year = "2011",
+ abstract =
+ "One of the most fruitful advances in the field of experimental
+ mathematics has been the development of practical methods for very
+ highprecision numerical integration, a quest initiated by Keith
+ Geddes and other researchers in the 1980s and 1990s.These
+ techniques, when coupled with equally powerful integer relation
+ detection methods, have resulted in the analytic evaluation of many
+ integrals that previously were beyond the realm of symbolic
+ techniques.This paper presents a survey of the current stateoftheart
+ in this area (including results by the present authors and others),
+ mentions some new results, and then sketches what challenges lie
+ ahead.",
+ paper = "Bail11.pdf"
+}
+
+\end{chunk}
+
+\index{Huang, Zongyan}
+\index{England, Matthew}
+\index{Wilson, David}
+\index{Davenport, James H.}
+\index{Paulson, Lawrence C.}
+\begin{chunk}{axiom.bib}
+@article{Huan14,
+ author = "Huang, Zongyan and England, Matthew and Wilson, David and
+ Davenport, James H. and Paulson, Lawrence C.",
+ title = {{A Comparison of Three Heuristics to Choose the Variable
+ Ordering for Cylindrical Algebraic Decomposition}},
+ journal = "ACM Comm. in Computer Algebra",
+ volume = "48",
+ number = "3",
+ year = "2014",
+ abstraact =
+ "Cylindrical algebraic decomposition (CAD) is a key tool for problems
+ in real algebraic geometry and beyond. When using CAD there is often a
+ choice over the variable ordering to use, with some problems
+ infeasible in one ordering but simple in another. Here we discuss a
+ recent experiment comparing three heuristics for making this choice on
+ thousands of examples.",
+ paper = "Huan14.pdf"
+}
+
+\end{chunk}
+
+\index{Hamada, Tatsuyoshi}
+\begin{chunk}{axiom.bib}
+@article{Hama14,
+ author = "Hamada, Tatsuyoshi",
+ title = {{MathLibre: Personalizable Computer Environment for
+ Mathematical Research}},
+ volume = "48",
+ number = "3",
+ year = "2014",
+ abstract =
+ "MathLibre is a project to archive free mathematical software and free
+ mathematical documents and offer them on Live Linux system. MathLibre
+ Project is the direct descendant of KNOPPIX/Math Project. It provides
+ a desktop for mathematicians that can be set up easily and quickly.",
+ paper = "Hama14.pdf"
+}
+
+\end{chunk}
+
+\index{Fateman, Richard}
+\begin{chunk}{axiom.bib}
+@article{Fate14a,
+ author = "Fateman, Richard",
+ title = {{Algorithm Differentiation in Lisp: ADIL}},
+ journal = "ACM Comm. in Computer Algebra",
+ volume = "48",
+ number = "3",
+ year = "2014",
+ abstract =
+ "Algorithm differentiation (AD) is a technique used to transform a
+ program $F$ computing a numerical function of one argument $F(x)$ into
+ another program $G(p)$ that returns a pair,
+ $\langle F (p), F^\prime(p)\rangle$ where by $F^\prime(p)$
+ we mean the derivative of $F$ with respect to its argument $x$,
+ evaluated at $x = p$. That is, we have a program AD that takes as input
+ a program, and returns another: $G := AD(F)$. Over the years AD
+ programs have been developed to allow $F$ to be expressed in some
+ specialized variant of a popular programming language L (FORTRAN, C,
+ Matlab, Python) and where $G$ is delivered in that language $L$ or some
+ other. Alternatively, executing $F(p)$ is some environment will deliver
+ $\langle F^\prime(p), F(p)\rangle$ directly. AD tools have also
+ been incorporated in computer algebra systems (CAS) such as
+ Maple. A CAS is hardly necessary for the task of writing the AD
+ program, since the main requirement is a set of tools for
+ manipulation of an internal (typically tree) form of a program.
+ In Lisp, a normal program is already in this form and so the AD
+ program in Lisp (ADIL), the target $F$ and the product $G$ can
+ all be expressed compactly in Lisp. In spite of the brevity and
+ extensibility of the ADIL program, we can provide
+ features which are unsupported in other AD programs. In particular,
+ recursive functions are easily accommodated. Our perspective here is
+ to point out that for scientists who write programs in Lisp or any
+ language that can be converted to Lisp, AD is easily at hand.",
+ paper = "Fate14a.pdf"
+}
+
+\end{chunk}
+
+\index{England, M.}
+\index{ChebTerrab, E.}
+\index{Bradford, R.}
+\index{Davenport, J.H.}
+\index{Wilson, D.}
+\begin{chunk}{axiom.bib}
+@article{Engl14c,
+ author = "England, M. and ChebTerrab, E. and Bradford, R. and
+ Davenport, J.H. and Wilson, D.",
+ title = {{Branch Cuts in MAPLE 17}},
+ journal = "ACM Comm. in Computer Algebra",
+ volume = "48",
+ number = "1",
+ year = "2014",
+ abstract =
+ "Accurate and comprehensible knowledge about the position of branch
+ cuts is essential for correctly working with multivalued functions,
+ such as the square root and logarithm. We discuss the new tools in
+ Maple 17 for calculating and visualising the branch cuts of such
+ functions, and others built up from them. The cuts are described in an
+ intuitive and accurate form, offering substantial improvement on the
+ descriptions previously available.",
+ paper = "Engl14c.pdf"
+}
+
+\end{chunk}
+
+\index{Stoutemyer, David R.}
+\begin{chunk}{axiom.bib}
+@article{Stou13,
+ author = "Stoutemyer, David R.",
+ title = {{A Computer Algebra User Interface Manifesto}},
+ journal = "ACM Communications in Computer Algebra",
+ volume = "47",
+ number = "4",
+ year = "2013",
+ abstract =
+ "Many computer algebra systems have more than 1000 builtin functions,
+ making expertise difficult. Using mock dialog boxes, this article
+ describes a proposed interactive generalpurpose wizard for organizing
+ optional transformations and allowing easy fine grain control over the
+ form of the result – even by amateurs. This wizard integrates ideas
+ including:
+ \begin{itemize}
+ \item flexible subexpression selection;
+ \item complete control over the ordering of variables and
+ commutative operands, with wellchosen defaults;
+ \item interleaving the choice of successively less main
+ variables with applicable function choices to provide detailed
+ control without incurring a combinatorial number of applicable
+ alternatives at any one level;
+ \item quick applicability tests to reduce the listing of
+ inapplicable transformations;
+ \item using an organizing principle to order the alternatives
+ in a helpful manner;
+ \item labeling quicklycomputed alternatives in dialog boxes
+ with a preview of their results, using ellipsis elisions if
+ necessary or helpful;
+ \item allowing the user to retreat from a sequence of choices
+ to explore other branches of the tree of alternatives – or to
+ return quickly to branches already visited;
+ \item allowing the user to accumulate more than one of the
+ alternative forms;
+ \item integrating direct manipulation into the wizard; and
+ \item supporting not only the usual inputresult pair mode, but
+ also the useful alternative derivational and in situ replacement
+ modes in a unified window.
+ \end{itemize}",
+ paper = "Stou13.pdf",
+ kryeotfd = "printed"
+}p
+
+\end{chunk}
+
+\index{Sorenson, Jonathan}
+\begin{chunk}{axiom.bib}
+@article{Sore94,
+ author = "Sorenson, Jonathan",
+ title = {{Two Fast GCD Algorithms}},
+ journal = "Journal of Algorithms",
+ volume = "16",
+ pages = "110144",
+ year = "1994",
+ abstract =
+ "We present two new algorithms for computing geatest common
+ divisors: the right and leftshift $k$ary GCD algorithms. These
+ algorithms are generalizations of the binary and leftshift binary
+ algorithms. Interestingly, both new algorithms have sequential
+ versions that are practical and efficient and parallel versions
+ that rival the best previous parallel GCD algorithms. We show that
+ sequential versions of both algorithms take $O(n^2/log~n)$ bit
+ operations in the worst case to compute the GCD of two nbit
+ integers. This compares favorably to the Euclidean and moth
+ precision versions of these GCD algorithms, and we found that both
+ $k$ary algorithms are faster than the Euclidean and binary
+ algorithms on inputs of 100 to 1000 decimal digits in length. We
+ show that parallel versions of both algorithms match the
+ complexity of the best previous parallel GCD algorithm due to Chor
+ and Goldreich. Specifically, if $log~n\le k \le 2^n$ and $k$ is a
+ power of two, then both algorithms run in $O(n/log~n+log^2~n)$
+ time using a number of processors bounded by a polynomial in $n$
+ and $k$ on a common CRCW PRAM. We also discuss extended versions
+ of both algorithms.",
+ paper = "Sore94.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Weber, Kenneth}
+\index{Trevisan, Vilmar}
+\index{Martins, Luiz Felipe}
+\begin{chunk}{axiom.bib}
+@article{Webe05a,
+ author = "Weber, Kenneth and Trevisan, Vilmar and Martins, Luiz Felipe",
+ title = {{A Modular Integer GCD Algorithm}},
+ journal = "J. of Algorithms",
+ volume = "54",
+ year = "2005",
+ pages = "152167",
+ abstract =
+ "This paper describes the first algorithm to compute the greatest
+ common divisor (GCD) of two $n$bit integers using a modular
+ representation for intermediate values $U$, $V$ and also for the
+ result. It is based on a reduction step, similar to one used in
+ the accelerated algorithm when $U$ and $V$ are close to the same
+ size, that replaces $U$ by $(UbV)/p$, where $p$ is one of the
+ prime moduli and $b$ is the unique integer in the interval
+ $(p/2,p/2)$ such that $b\equiv UV^{1} (mod~p)$. When the
+ algorithm is executed on a bit common CRCW PRAM with
+ $O(n~log~n~log~log~log~n)$ processors, it takes $(O(n)$ time in
+ the worst case. A heuristic model of the average case yields
+ $O(n/log~n)$ time on the same number of processors.",
+ paper = "Webe05a.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Schonhage, A.}
+\begin{chunk}{axiom.bib}
+@article{Scho88,
+ author = "Schonhage, A.",
+ title = {{Probabilistic Computation of Integer Polynomial GCDs}},
+ journal = "J. of Algorithms",
+ volume = "9",
+ pages = "365371",
+ year = "1988",
+ abstract =
+ "We describe a probabilistic algorithm for the computation of the
+ gcd of two univariate integer polynomials of degrees $\le n$ with
+ their $l^1$norms being bounded by $2^h$ and estimate its expected
+ running time by a worstcase bound of
+ $O(n(n+h)^{l+\epsilon(l)})$.",
+ paper = "Scho88.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{LeGuin, Ursula K.}
+\begin{chunk}{axiom.bib}
+@book{Legu76,
+ author = "LeGuin, Ursula K.",
+ title = {{The Left Hand of Darkness}},
+ publisher = "Penguin Random House",
+ year = "1976",
+ isbn = "9781101665398"
+}
+
+\end{chunk}
+
+\index{Shulman, Michael}
+\begin{chunk}{axiom.bib}
+@misc{Shul18,
+ author = "Shulman, Michael",
+ title = {{Linear Logic for Constructive Mathematics}},
+ link = "\url{https://arxiv.org/pdf/1805.07518.pdf}",
+ year = "2018",
+ abstract =
+ "We show that numerous distinctive concepts of constructive
+ mathematics arise automatically from an interpretation of 'linear
+ higherorder logic' into intuitionistic higherorder logic via a Chu
+ construction. This includes apartness relations, complemented
+ subsets, antisubgroups and antiideals, strict and nonstrict order
+ pairs, cutvalued metrics, and apartness spaces. We also explain the
+ constructive bifurcation of classical concept s using the choice
+ between multiplicative and additive linear connectives. Linear logic
+ thus systematically 'constructivizes' classical definitions and deals
+ automatically with the resulting bookkeeping, and could potentially
+ be used directly as a basis for constructive mathematics in place
+ of intuitionistic logic.",
+ paper = "Shul18.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Khan, Muhammad Taimoor}
+\begin{chunk}{axiom.bib}
+@techreport{Khan13,
+ author = "Khan, Muhammad Taimoor",
+ title = {{On the Formal Verification of Maple Programs}},
+ year = "2013",
+ type = "technical report",
+ number = "1307",
+ institution = "RISC Linz",
+ abstract =
+ "In this paper, we present an examplebased demonstration of our
+ recent results on the formal verification of programs written in the
+ computer algebra language (Mini)Maple (a slightly modified subset of
+ Maple). The main goal of this work is to develop a verification
+ framework for behavioral analysis of MiniMaple programs. For
+ verification, we translate an annotated MiniMaple program into the
+ language Why3ML of the intermediate verification tool Why3 developed
+ at LRI, France. We generate verification conditions by the
+ corresponding component of Why3 and later prove the correctness of
+ these conditions by various supported by the Why3 backend automatic
+ and interactive theorem provers. We have used the verification
+ framework to verify some parts of the main test example of our
+ verification framework, the Maple package DifferenceDifferential
+ developed at our institute to compute bivariate differencedifferential
+ polynomials using relative Gr ̈obner bases.",
+ paper = "Khan13.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Daly, Timothy}
+\begin{chunk}{axiom.bib}}
+@misc{Daly03,
+ author = "Daly, Timothy",
+ title = {{Axiom Website: http://axiomdeveloper.org}},
+ link = "\url{http://axiomdeveloper.org}",
+ keywords = "axiomref",
+ year = "2003"
+}
+
+\end{chunk}
+
+\index{Dijkstra, Edsgar W.}
+\begin{chunk}{axiom.bib}
+@article{Dijk75,
+ author = "Dijkstra, Edsgar W.",
+ title = {{Guarded Commands, Nondeterminancy and Formal Derivation
+ of Programs}},
+ journal = "Comm. of the ACM",
+ volume = "18",
+ number = "8",
+ year = "1975",
+ pages = "453457",
+ abstract =
+ "Socalled 'guarded commands' are introduced as a building block
+ for alternative and repetitive constructs that allow
+ nondeterministic program components for which at least the
+ activity evoked, but possibly even the final state, is not
+ necessarily uniquly determined by the initial state. For the
+ formal derivation of programs expressed in terms of these
+ constructs, a calculus will be shown.",
+ paper = "Dijk75.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{van Emden, M.H.}
+\index{Kowalski, R.A.}
+\begin{chunk}{axiom.bib}
+@article{Emde76,
+ author = "van Emden, M.H. and Kowalski, R.A.",
+ title = {{The Semantics of Predicate Logic as a Programming Language}},
+ journal = "J. Association for Computing Machinery",
+ volume = "23",
+ number = "4",
+ year = "1976",
+ pages = "733742",
+ abstract =
+ "Sentences in firstorder predicate logic can be usefully interpreted
+ as programs In this paper the operational and fixpomt semantics of
+ predicate logic programs are defined, and the connections with the
+ proof theory and model theory of logic are investigated It is
+ concluded that operational semantics is a part of proof theory and
+ that fixpolnt semantics is a special case of modeltheoret:c
+ semantics.",
+ paper = "Emde76.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Tarski, Alfred}
+\begin{chunk}{axiom.bib}
+@article{Tars69,
+ author = "Tarski, Alfred",
+ title = {{Truth and Proof}},
+ journal = "Scientific American",
+ volume = "1969",
+ pages = "6377",
+ year = "1969",
+ paper = "Tars69.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Apt, Krysztof R.}
+\index{Bezem, Marc}
+\begin{chunk}{axiom.bib}
+@inbook{Aptx99,
+ author = "Apt, Krysztof R. and Bezem, Marc",
+ title = {{Formulas as Programs}},
+ booktitle = "The Logic Programming Paradigm",
+ year = "1999",
+ publisher = "Springer Berlin Heidelberg",
+ pages = "75107",
+ isbn = "9783642600852",
+ abstract =
+ "We provide here a computational interpretation of firstorder
+ logic based on a constructive interpretation of satisfiability
+ w.r.t. a fixed but arbitrary interpretation. In this approach the
+ formulas themselves are programs. This contrasts with the
+ socalled formulas as types approach in which the proofs of the
+ formulas are typed terms that can be taken as programs. This view
+ of computing is inspired by logic programming and constraint logic
+ programming but differs from them in a number of crucial aspects.
+
+ Formulas as programs is argued to yield a realistic approach to
+ programming that has been realized in the implemented programming
+ language Alma0 Apt, Brunekreef, Partington and Schaerf (1998)
+ that combines the advantages of imperative and logic
+ programming. The work here reported can also be used to reason
+ about the correctness of nonrecursive Alma0 programs that do not
+ include destructive assignment.",
+ paper = "Aptx99.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Mazur, Barry}
+\begin{chunk}{axiom.bib}
+@misc{Mazu07,
+ author = "Mazur, Barry",
+ title = {{When is One Thing Equal to Some Other Thing?}},
+ link = "\url{http://www.math.harvard.edu/~mazur/preprints/when_is_one.pdf}",
+ year = "2007",
+ paper = "Mazu07.pdf"
+}
+
+\end{chunk}
+
+\index{Kant, Immanuel}
+\begin{chunk}{axiom.bib}
+@book{Kant98,
+ author = "Kant, Immanuel",
+ title = {{The Critique of Pure Reason}},
+ publisher = "Cambridge University Press",
+ year = "1998",
+ isbn = "0521354021",
+ link = "\url{http://strangebeautiful.com/othertexts/kantfirstcritiquecambridge.pdf}",
+ paper = "Kant98.pdf"
+}
+
+\end{chunk}
+
+\index{Smith, A.}
+\begin{chunk}{axiom.bib}
+@techreport{Smit90,
+ author = "Smith, A.",
+ title = {{The KnuthBendix Completion Algorithm and its Specification in Z}},
+ type = "technical report",
+ institution = "Ministry of Defence, RSRE Malvern WORCS",
+ year = "1990",
+ number = "RSRE Memorandum 4323",
+ abstract =
+ "Proving that something is a consequence of a set of axioms can be
+ very difficult. The KnuthBendix completion algorithm attempts to
+ automate this process when the axioms are equations. The algorithm
+ is bound up in the area of term rewriting, and so this memorandum
+ contains an introduction to the tehory of term rewriting, followed
+ by an overview of the algorithm. Finally a formal specification of
+ the algorithm is given using the language Z.",
+ paper = "Smit90.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Dick, A.J.J.}
+\begin{chunk}{axiom.bib}
+@techreport{Dick88,
+ author = "Dick, A.J.J.",
+ title = {{Automated Equational Reasoning and the KnuthBendix Algorithm:
+ An Informal Introduction}},
+ year = "1988",
+ type = "technical report",
+ institution = "Rutherford Appelton Laboratory",
+ number = "RAL88043",
+ paper = "Dick88.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Dick, Jeremy}
+\begin{chunk}{axiom.bib}
+@article{Dick91,
+ author = "Dick, Jeremy",
+ title = {{An Introduction to KnuthBendix Completion}},
+ journal = "The Computer Journal",
+ volume = "34",
+ number = "1",
+ year = "1991",
+ abstract =
+ "An informal introduction is given to the underlying concepts of
+ term rewriting. Topics covered are KnuthBendix completion,
+ completion modulo equations, unfailing completion and theorem
+ proving by completion.",
+ paper = "Dick91.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Knuth, Donald E.}
+\index{Bendix, Peter B.}
+\begin{chunk}
+\incollection{Knut70,
+ author = "Knuth, Donald E. and Bendix, Peter B.",
+ title = {{Simple Word Problems in Unversal Algebras}},
+ booktitle = "Computational Problems in Abstract Algebra",
+ editor = "Leech, John",
+ publisher = "Pergamon Press",
+ isbn = "080129757",
+ year = "1970",
+ pages = "263298",
+ paper = "Knut70.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Leech, John}
+\begin{chunk}{axiom.bib}
+@book{Leec70,
+ author = "Leech, John",
+ title = {{Computational Problems in Abstract Algebra}},
+ publisher = "Pergamon Press",
+ year = "1970",
+ isbn = "080129757",
+ paper = "Leec70.pdf"
+}
+
+\end{chunk}
+
+\index{Dershowitz, Nachum}
+\begin{chunk}{axiom.bib}
+@article{Ders87,
+ author = "Dershowitz, Nachum",
+ title = {{Termination of Rewriting}},
+ journal = "J. Symbolic Computation",
+ volume = "3",
+ year = "1987",
+ pages = "69116",
+ abstract =
+ "This survey describes methods for proving that systems of rewrite
+ rules are terminating programs. We illustrate the use in termination
+ proofs of various kinds of orderings on terms, including polynomial
+ interpretations and path orderings. The effect of restrictions, such
+ as linearity, on the form of rules is also considered. In general,
+ however, termination is an undeeidable property of rewrite systems.",
+ paper = "Ders87.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Atkey, Robert}
+\begin{chunk}{axiom.bib}
+@misc{Atke18,
+ author = "Atkey, Robert",
+ title = {{Parameterised Notions of Computation}},
+ link = "\url{https://bentnib.org/paramnotionsjfp.pdf}",
+ year = "2018",
+ abstract =
+ "Moggi’s Computational Monads and Power et al ’s equivalent notion of
+ Freyd category have captured a large range of computational effects
+ present in programming languages. Examples include nontermination,
+ nondeterminism, exceptions, continuations, sideeffects and
+ input/output. We present generalisations of both computational monads
+ and Freyd categories, which we call parameterised monads and
+ parameterised Freyd categories, that also capture computational
+ effects with parameters. Examples of such are composable
+ continuations, sideeffects where the type of the state varies and
+ input/output where the range of inputs and outputs varies. By also
+ considering structured parameterisation, we extend the range of
+ effects to cover separated sideeffects and multiple independent
+ streams of I/O. We also present two typed $\lambda$calculi that
+ soundly and completely model our categorical definitions — with and
+ without symmetric monoidal parameterisation — and act as prototypical
+ languages with parameterised effects.",
+ paper = "Atke18.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Bozman, Gerald}
+\index{Buco, William}
+\index{Daly, Timothy}
+\index{Tetzlaff, William}
+\begin{chunk}{axiom.bib}
+@article{Bozm84,
+ author = "Bozman, Gerald and Buco, William and Daly, Timothy and
+ Tetzlaff, William",
+ title = {{Analysis of Free Storage Algorithms  Revisited}},
+ journal = "IBM Systems Journal",
+ volume = "23",
+ number = "1",
+ year = "1984",
+ abstract =
+ "Most research in freestorage management has centered around
+ strategies that search a linked list and strategies that partition
+ storage into predetermined sizes. Such algorithms are analyzed in
+ terms of CPU efficiency and storage efficiency. The subject of this
+ study is the freestorage management in the Virtual Machine/System
+ Product (VM/SP) system control program. As a part of this study,
+ simulations were done of established, and proposed, dynamic storage
+ algorithms for the VM/SP operating system. Empirical evidence is given
+ that simplifying statistical assumptions about the distribution of
+ interarrival times and holding times has high predictive
+ ability. Algorithms such as firstfit, modified firstfit, and
+ bestfit are found to be CPUinefficient. Buddy systems are found to
+ be very fast but suffer from a high degree of internal
+ fragmentation. A form of extended subpooling is shown to be as fast as
+ buddy systems with improved storage efficiency. This algorithm was
+ implemented for VM/SP, and then measured. Results for this algorithm
+ are given for several production VM/SP systems.",
+ paper = "Bozm84.pdf"
+}
+
+\end{chunk}
\ No newline at end of file
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 68c02b4..a794758 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5964,6 +5964,8 @@ books/bookheader.tex fix typo
src/axiomwebsite/currentstate.html fix last update
20180717.01.tpd.patch
src/axiomwebsite/documentation.html redirect downloads to github
+20180811.01.tpd.patch
+books/bookvolbib add references

1.9.1