From 7d704eb3ac515a3f8281c1fb34c6ee3cf9141d34 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Sat, 2 Dec 2017 09:25:40 0500
Subject: [PATCH] books/bookvolbib add references
MIMEVersion: 1.0
ContentType: text/plain; charset=UTF8
ContentTransferEncoding: 8bit
Goal: Proving Axiom Correct
\index{Maurer, D.}
\begin{chunk}{axiom.bib}
@article{Maur73,
author = "Maurer, D.",
title = {{Applications of Symbolic Mathematical Manipulation to
Algorithmic Verification (Abstract)},
journal = "SIGSAM Bulletin",
volume = "26",
year = "1973",
pages = "4"
}
\end{chunk}
\index{Waldinger, R.J.}
\index{Levitt, K.N.}
\begin{chunk}{axiom.bib}
@article{Wald74,
author = "Waldinger, R.J. and Levitt, K.N.",
title = {{Reasoning about Programs}},
journal = "Artificial Intelligence",
volume = "5",
number = "3",
year = "1974",
pages = "235316",
abstract =
"This paper describes a theorem prover that embodies knowledge about
programming constructs, such as numbers, arrays, lists, and
expressions. The program can reason about these concepts and is used
as part of a program verification system that uses the FloydNaur
explication of program semantics. It is implemented in the qa4
language; the qa4 system allows many pieces of strategic knowledge,
each expressed as a small program, to be coordinated so that a program
stands forward when it is relevant to the problem at hand. The
language allows clear, concise representation of this sort of
knowledge. The qa4 system also has special facilities for dealing with
commutative functions, ordering relations, and equivalence relations;
these features are heavily used in this deductive system. The program
interrogates the user and asks his advice in the course of a
proof. Verifications have been found for Hoare's FIND program, a
realnumber division algorithm, and some sort programs, as well as for
many simpler algorithms. Additional theorems have been proved about a
pattern matcher and a version of Robinson's unification algorithm. The
appendix contains a complete, annotated listing of the deductive
system and annotated traces of several of the deductions performed by
the system.",
paper = "Wald74.pdf"
}
\end{chunk}
\index{Floyd, W.}
\begin{chunk}{axiom.bib}
@incollection{Floy86,
author = "Floyd, W.",
title = {{Toward Interactive Design of Correct Programs}},
booktitle = "Reading in Artificial Intelligence and Software Engeering",
pages = "331334",
year = "1986",
isbn = "0934613125"
}
\end{chunk}
\index{Milner, R.}
\begin{chunk}{axiom.bib}
@article{Miln84,
author = "Milner, R.",
title = {{The Use of Machines to Assist in Rigorous Proof}},
journal = "Philosophical Transactions of the Royal Society",
volume = "312",
pages = "411422",
number = "1522",
year = "1984",
abstract =
"A methodology for computer assisted proof is presented with an
example. A central ingredient in the method is the presentation of
tactics (or strategies) in an algorithmic metalanguage. Further, the
same language is also used to express combinators, by which simple
elementary tactics  which often correspond to the inference rules of
the logic employed  are combined into more complex tactics, which may
even be strategies complete for a class of problems. However, the
emphasis is not upon completeness but upon providing a metalogical
framework within which a user may express his insight into proof
methods and may delegate routine (but errorprone) work to the
computer. This method of tactic composition is presented at the start
of the paper in the form of an elementary theory of goalseeking. A
second ingredient of the methodology is the stratification of
machineassisted proof by an ancestry graph of applied theories, and
the example illustrates this stratification. In the final section,
some recent developments and applications of the method are cited.",
paper = "Miln84.pdf"
}
\end{chunk}
\index{Giunchiglia, Fausto}
\index{Pecchiari, Paolo}
\index{Talcott, Carolyn}
\begin{chunk}{axiom.bib}
@techreport{Giun94,
author = "Giunchiglia, Fausto and Pecchiari, Paolo and Talcott, Carolyn",
title = {{Reasoning Theories  Towards an Architecture for Open
Mechanized Reasoning}},
year = "1994",
institution = "Stanford University",
abstract =
"Our ultimate goal is to provide a framework and a methodology which
will allow users, and not only system developers, to construct complex
reasoning systems by composing existing modules, or to add new modules
to existing systems, in a "plug and play" manner. These modules and
systems might be based on different logics; have different domain
models; use different vocabularies and data structures; use different
reasoning strategies; and have different interaction
capabilities. This paper makes two main contributions towards our
goal. First, it proposes a general architecture for a class of
reasoning systems called Open Mechanized Reasoning Systems (OMRSs). An
OMRS has three components: a reasoning theory component which is the
counterpart of the logical notion of formal system, a control
component which consists of a set of inference strategies, and an
interaction component which provides an OMRS with the capability of
interacting with other systems, including OMRSs and hum...",
paper = "Giun94.pdf"
}
\end{chunk}
\index{Carette, Jacques}
\index{Farmer, William M.}
\index{Wajs, Jeremie}
\begin{chunk}{axiom.bib}
@misc{Care11b,
author = "Carette, Jacques and Farmer, William M. and Wajs, Jeremie",
title = {{Trustable Communication Between Mathematics Systems}},
year = "2011",
link = "\url{https://pdfs.semanticscholar.org/0d0b/206edf7ef1c01d7bfa1284c85b469b2fbd29.pdf}",
abstract =
"This paper presents a rigorous, unified framework for facilitating
communication between mathematics systems. A mathematics system is
given one or more interfaces which offer deductive and computational
services to other mathematics systems. To achieve communication
between systems, a client interface is linked to a server interface by
an asymmetric connection consisting of a pair of translations.
Answers to requests are trustable in the sense that they are correct
provided a small set of prescribed conditions are satisfied. The
frame work is robust with respect to interface extension and can
process requests for abstract services, where the server interface is
not fully specified.",
paper = "Care11b.pdf"
}
\end{chunk}
\index{Carlisle, David}
\index{Ion, Patrick}
\index{Miner, Robert}
\begin{chunk}{axiom.bib}
@misc{Carl14,
author = "Carlisle, David and Ion, Patrick and Miner, Robert",
title = {{Mathematical Markup Language}},
year = "2014",
link = "\url{https://www.w3.org/TR/MathML3/}"
}
\end{chunk}
\index{Buswell, S.}
\index{Caprotti, O.}
\index{Carlisle, D.P.}
\index{Dewar, M.C.}
\index{Gaetano, M.}
\index{Kohlhase, M.}
\begin{chunk}{axiom.bib}
@misc{Busw04,
author = "Buswell, S. and Caprotti, O. and Carlisle, D.P. and Dewar, M.C.
and Gaetano, M. and Kohlhase, M.",
title = {{The OpenMath Standard}},
year = "2004",
link = "\url{https://www.openmath.org/standard/om2020040630/omstd20.pdf}",
paper = "Busw04.pdf"
}
\end{chunk}
\index{Armando, Alessandro}
\index{Zini, Daniele}
\begin{chunk}{axiom.bib}
@misc{Arma00,
author = "Armando, Alessandro and Zini, Daniele",
title = {{Towards Interoperable Mechanized Reasoning Systems:
The Logic Broker Architecture}},
year = "2000",
abstract =
"There is a growing interest in the integration of mechanized
reasoning systems such as automated theorem provers, computer algebra
systems, and model checkers. Stateoftheart reasoning systems are
the result of many manyears of careful development and engineering,
and usually they provide a high degree of sophistication in their
respective domain. Yet they often perform poorly when applied outside
the domain they have been designed for. The problem of integrating
mechanized reasoning systems is therefore being perceived as an
important issue in automated reasoning. In this paper we present
the Logic Broker Architecture, a framework which provides the needed
infrastructure for making mechanized reasoning systems interoperate.
The architecture provides location transparency, a way to forward
requests for logical services to appropriate reasoning systems via a
simple registration/subscription mechanism, and a translation
mechanism which ensures the transparent and provably sound exchange of
logical services.",
paper = "Arma00.pdf"
}
\end{chunk}
\index{Lester, D.R.}
\begin{chunk}{axiom.bib}
@inproceedings{Lest01,
author = "Lester, D.R.",
title = {{Effective Continued Fractions}},
booktitle = "15th IEEE Symp. on Computer Arithmetic",
publisher = "IEEE Computer Society Press",
year = "2001",
pages = "163170",
abstract =
"Only the leading seven terms of a continued fraction are needed to
perform online arithmetic, provided the continued fractions are of
the correct form. This forms the basis of a proof that there is an
effective representation of the computable reals as continued
fractions: we also demonstrate that the basic arithmetic operations
are computable using this representation.",
paper = "Lest01.pdf"
}
\end{chunk}
\index{Vuillemin, J.}
\begin{chunk}{axiom.bib}
@techreport{Vuil87,
author = "Vuillemin, J.",
title = {{Exact Real Computer Arithmetic with Continued Fractions}},
institution = "Institut National de Recherche en Informatique et en
Automatique",
year = "1987",
number = "760",
abstract =
"We discuss a representation of the {\sl computable real numbers} by
continued fractions. This deals with the subtle points of undecidable
and integer division, as well as representing the infinite
$\infty=1/0$ and undefined $\bot=0/0$ numbers. Two general algorithms
for performing arithmetic operations are introduced. The
{\sl algebraic algorithm}, which computes sums and products of
continued fractions as a special case, basically operates in a
positional manner, producing one term of output for each term of
input. The {\sl transcendental algorithm} uses a general formula of
Gauss to compute the continued fractions of exponentials, logarithms,
trigonometric functions, as well as a wide class of special
functions. This work has been implemented in Le\_Lisp and the
performance of these algorithms appears to be quite good; however, no
competing system has been available for comparison",
paper = "Vuil87.pdf"
}
\end{chunk}
\index{Zinn, Claus}
\begin{chunk}{axiom.bib}
@phdthesis{Zinn04,
author = "Zinn, Claus",
title = {{Understanding Informal Mathematical Discourse}},
school = "Universitat Erlangen Nurnberg",
year = "2004",
abstract =
"Automated reasoning is one of the most established disciplines in
informatics and artificial intelligence, and formal methods become
increasingly employed in practical applications. However, for the most
part, such applications seem to be limited to informaticsspecific
areas (e.g., the verification of correctness properties of software
and hardware specifications) and areas close to informatics such as
computational linguistics (e.g., the computation of consistence and
informativeness properties of semantic representations). Naturally,
there is also a potential for practical applications in the the area
of mathematics: the generation of proofs for mathematically
interesting and motivated theorems and, quite associated, the
computersupported formalisation of (parts of elementary)
mathematics. It is a matter of fact, however, that mathematicians
rarely use computersupport for the construction and verification of
proofs. This is mainly caused by the “unnaturalness” of the language
and the reasoning that such proof engines support.
In the past, researchers in the area of automated reasoning have
focused their work on formalisms and algorithms that allow the
construction and verification of proofs that are written in a
formallogical language and that only use a limited number of
inference rules. For the computer scientist, such formal proofs have
the advantage of a simple and ambiguousfree syntax, which can thus be
easily processed. Moreover, the limited number of inference rules has
a direct impact on the complexity of the search space that needs to be
conquered during the process of constructing proofs. The verification
of given formal proofs is greatly facilitated by the complete
explicitness of their logical argumentation where no reasoning step is
left out. For mathematicians, however, such formal proofs are usually
hard to understand. For them, they are written in an unfamiliar and
artificial language and much too detailed. Moreover, the sheer number
of inference steps, while logically relevant, describe only trivial
mathematical details and make it difficult to follow a proof’s main
underlying argumentation line. In practise, thus, mathematicians use
proof generation engines rather seldom, if at all. The same is true
with regard to proof verification tools. The amount of work that is
required to verify a mathematical proof with such tools is
considerable, if not prohibitive. Since proof verification systems
only accept formal proofs as input, the mathematician’s first task is
to manually translate the mathematical proof into the formal language
that is accepted by the verifier. This in turn includes the
translation of the proof’s underlying mathematical argumentation into
inference rules that are supported by the proof engine. Such
translations and refinements are usually very time consuming, tedious,
and prone to error themselves. Hence, how the proof verifier then
judges the result of proof translation and proof refinement is only
of limited relevance to the original mathematical proof. From the
mathematician’s point of view, there is thus a need for a proof
verification system that is capable of processing mathematical proofs
automatically, at least with regard to translating the mathematicians’
expert language into the system’s artificial formal language. Such a
system would have an enormous potential in the community of
mathematics, and this potential has been recognised early. In the
beginning of the 1960s, John McCarthy, one of the pioneers of
artificial intelligence, remarked that ``[c]hecking mathematical proofs
is potentially one of the most interesting and useful applications of
automatic computers'' [111]. More than forty years thereafter, a tool
that supports mathematicians with the verification of mathematical
proofs is more science fiction than reality. Its realisation is
associated with research questions within the disciplines of automated
reasoning and computational linguistics that are still only partially
answered.
This thesis aims at contributing towards the realisation of a
verifier for mathematical proofs. It attempts to provide a general
framework as well as an implementation for such a proof
engine. The dissertation’s objects of study are short and simple
proofs that were taken from textbooks on elementary number
theory. Fig. 1 depicts a proof of the mathematical truth that
every positive integer greater than 1 can be represented as a
product of one or more primes. The proof consists of only a few
lines and little mathematical knowledge is necessary to follow the
proof author’s argumentation. It is this kind of short proof that
we attempt to check automatically.",
paper = "Zinn04.pdf"
}
\end{chunk}
\index{Trybulec, Andrzej}
\begin{chunk}{axiom.bib}
@misc{Tryb02,
author = "Trybulec, Andrzej",
title = {{Towards Practical Formalizaiton of Mathematics}},
comment = "abstract",
link =
"\url{http://www.macs.hw.ac.uk/~fairouz/forest//events/automath2002/abstracts/Andrzej.abst.html}",
abstract =
"In sixties the opinion that mathematics cannot be practically
formalized was well established. So the main achievement of de Bruijn,
among many others, is the decision that the problem must be reconsider
and probably positively solved. And I believe that 1967 will be
treated by future historians of mathematics as a turning point.
It is not easy to say precisely what we learnt in the meantime, if we
learnt anything at all. I believe that the most important results are:
\begin{enumerate}
\item we need experiments with much more advanced mathematics than
already done
\item a system for practical formalization of mathematics probably will
not be a simple system based on small number of primitive notions
\item integration with a computer algebra systems may be necessary or at
least a feasible system must have bigger computational power.
\end{enumerate}
Still we should me more concerned with the original ideas of de
Bruijn, the most important that eventually we have to be able to
formalize new mathematical results, published in mathematical
newspapers in this century."
}
\end{chunk}
\index{Hayes, Patrick J.}
\begin{chunk}{axiom.bib}
@inproceedings{Haye74,
author = "Hayes, Patrick J.",
title = {{Some Problems and Nonproblems in Representation Theory}},
booktitle = "AI and Simulation of Behaviour Conference",
year = "1974",
pages = "6379"
}
\end{chunk}
\index{de Bruijn, N.G.}
\begin{chunk}{axiom.bib}
@incollection{Brui94a,
author = "de Bruijn, N.G.",
title = {{The Mathematical Vernacular, a Language for Mathematics
with Typed Sets}},
booktitle = "Selected Papers on Automath",
pages = "865935",
year = "1994",
publisher = "NorthHolland",
link = "\url{https://pure.tue.nl/ws/files/2073504/610209.pdf}",
paper = "Brui94a.pdf"
}
\end{chunk}
\index{Elbers, Hugo Johannes}
\begin{chunk}{axiom.bib}
@phdthesis{Elbe98,
author = "Elbers, Hugo Johannes",
title = {{Connecting Informal and Formal Mathematics}},
year = "1998",
school = "Technische Universiteit Eindhoven",
paper = "Elbe98.pdf"
}
\end{chunk}
\index{Bundy, Alan}
\begin{chunk}{axiom.bib}
@incollection{Bund91,
author = "Bundy, Alan",
title = {{A Science of Reasoning (Extended Abstract)}},
booktitle = "Computational Logic: Essays in Honor of Alan
Robinson",
year = "1991",
publisher = "MIT Press",
abstract =
"How can we understand reasoning in general and mathematical proofs
in particular? It is argued that a highlevel understanding of proofs
is needed to complement the lowlevel understanding provided by
Logic. A role for computation is proposed to provide this highlevel
understanding, namely by the association of proof plans with
proofs. Criteria are given for assessing the association of a proof
plan with a proof.",
paper = "Bund91.pdf"
}
\end{chunk}
\index{Daly, Timothy}
\index{Botch, Mark}
\begin{chunk}{axiom.bib}
@misc{Daly17,
author = "Daly, Timothy and Botch, Mark",
title = {{Axiom Developer Website}},
link = "\url{http://axiomdeveloper.org}",
year = "2017"
}
\end{chunk}
\index{SpectorZabusky, Antal}
\index{Breitner, Joachim}
\index{Rizkallah, Christine}
\index{Weirich, Stephanie}
\begin{chunk}{axiom.bib}
@inproceedings{Spec18,
author = "SpectorZabusky, Antal and Breitner, Joachim and
Rizkallah, Christine and Weirich, Stephanie",
title = {{Total Haskell is Reasonable Coq}},
booktitle = "ACM SIGPLAN Int. Conf. on Certified Programs and
Proofs",
publisher = "ACM",
year = "2018",
abstract =
"We would like to use the Coq proof assistant to mechanically
verify properites of Haskell programs. To that end, we present a
tool, named {\tt hstocoq}, that translates total Haskell
programs into Coq programs via a shallow embedding. We apply our
tool in three case studies  a lawful {\tt Monad} instance,
``Hutton's razor'', and an existing data structure library  and
prove their correctness. These examples show that this approach is
viable: both that {\tt hstocoq} applies to existing Haskell
code, and that the output it produces is amenable to
verification.",
paper = "Spec18.pdf"
}
\end{chunk}

books/axiom.bib  386 +++++++++++++++++++++++++
books/bookvolbib.pamphlet  477 +++++++++++++++++++++++++++++++
changelog  2 +
patch  604 +++++++++++++++++++++++++++++
src/axiomwebsite/patches.html  2 +
5 files changed, 1273 insertions(+), 198 deletions()
diff git a/books/axiom.bib b/books/axiom.bib
index 25177fa..7c9c749 100644
 a/books/axiom.bib
+++ b/books/axiom.bib
@@ 1,3 +1,10 @@
+@misc{Daly17,
+ author = "Daly, Timothy and Botch, Mark",
+ title = {{Axiom Developer Website}},
+ link = "\url{http://axiomdeveloper.org}",
+ year = "2017"
+}
+
@book{Book00,
author = "Axiom Authors",
title = {{Volume 0: Axiom Jenks and Sutor}},
@@ 7509,10 +7516,11 @@ paper = "Brea89.pdf"
paper = "Bees92.pdf"
}
@misc{Beesxx,
+@misc{Bees98,
author = "Beeson, Michael",
title = {{Automatic Generation of EpsilonDelta Proofs of Continuity}},
link = "\url{http://www.michaelbeeson.com/research/papers/aisc.pdf}",
+ year = "1998",
abstract =
"As part of a project on automatic generation of proofs involving both
logic and computation, we have automated the production of some proofs
@@ 7526,7 +7534,7 @@ paper = "Brea89.pdf"
for intermixing logical deduction steps with computational steps and
with inequality reasoning. Problems discussed here as examples involve
the continuity and uniform continuity of various specific functions.",
 paper = "Beesxx.pdf"
+ paper = "Bees98.pdf"
}
@article{Benk03,
@@ 8033,8 +8041,8 @@ paper = "Brea89.pdf"
paper = "Broy88.pdf"
}
\article{Brui68,
 author = "de Bruijn, N.G."
+@article{Brui68,
+ author = "de Bruijn, N.G.",
title = {{The Mathematical Language Automath, its Usage, and Some of
its Extensions}},
journal = "Lecture Notes in Mathematics",
@@ 8403,6 +8411,26 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@misc{Care11b,
+ author = "Carette, Jacques and Farmer, William M. and Wajs, Jeremie",
+ title = {{Trustable Communication Between Mathematics Systems}},
+ year = "2011",
+ link = "\url{https://pdfs.semanticscholar.org/0d0b/206edf7ef1c01d7bfa1284c85b469b2fbd29.pdf}",
+ abstract =
+ "This paper presents a rigorous, unified framework for facilitating
+ communication between mathematics systems. A mathematics system is
+ given one or more interfaces which offer deductive and computational
+ services to other mathematics systems. To achieve communication
+ between systems, a client interface is linked to a server interface by
+ an asymmetric connection consisting of a pair of translations.
+ Answers to requests are trustable in the sense that they are correct
+ provided a small set of prescribed conditions are satisfied. The
+ frame work is robust with respect to interface extension and can
+ process requests for abstract services, where the server interface is
+ not fully specified.",
+ paper = "Care11b.pdf"
+}
+
@article{Chli10,
author = "Chlipala, Adam",
title = {{An Introduction to Programming and Proving with Dependent Types
@@ 9227,6 +9255,15 @@ paper = "Brea89.pdf"
isbn = "9781461275152"
}
+@incollection{Floy86,
+ author = "Floyd, W.",
+ title = {{Toward Interactive Design of Correct Programs}},
+ booktitle = "Reading in Artificial Intelligence and Software Engeering",
+ pages = "331334",
+ year = "1986",
+ isbn = "0934613125"
+}
+
@article{Frad08,
author = "Frade, Maria Joao",
title = {{Calculus of Inductive Construction. Software Formal Verification}},
@@ 9407,7 +9444,8 @@ paper = "Brea89.pdf"
type = "technical report",
number = "940915",
instituion = "IRST Trento Italy",
 year = "1994"
+ year = "1994",
+ paper = "Giun94.pdf"
}
@article{Gogu82,
@@ 9873,7 +9911,7 @@ paper = "Brea89.pdf"
abstract =
"This paper describes an implementation within Nuprl of mechanisms
that support the use of Nuprl's type theory as a language for
 constructing theoremprovind procedures. The main componenet of the
+ constructing theoremproving procedures. The main component of the
implementation is a large library of definitions, theorems and
proofs. This library may be regarded as the beginning of a book of
formal mathematics; it contains the formal development and explanation
@@ 10653,6 +10691,16 @@ paper = "Brea89.pdf"
adaptability."
}
+@article{Maur73,
+ author = "Maurer, D.",
+ title = {{Applications of Symbolic Mathematical Manipulation to
+ Algorithmic Verification (Abstract)}},
+ journal = "SIGSAM Bulletin",
+ volume = "26",
+ year = "1973",
+ pages = "4"
+}
+
@inproceedings{Mcal96,
author = "McAllester, D. and Arkondas, K.",
title = {{Walther Recursion}},
@@ 10989,6 +11037,34 @@ paper = "Brea89.pdf"
paper = "Miln78.pdf"
}
+@article{Miln84,
+ author = "Milner, R.",
+ title = {{The Use of Machines to Assist in Rigorous Proof}},
+ journal = "Philosophical Transactions of the Royal Society",
+ volume = "312",
+ pages = "411422",
+ number = "1522",
+ year = "1984",
+ abstract =
+ "A methodology for computer assisted proof is presented with an
+ example. A central ingredient in the method is the presentation of
+ tactics (or strategies) in an algorithmic metalanguage. Further, the
+ same language is also used to express combinators, by which simple
+ elementary tactics  which often correspond to the inference rules of
+ the logic employed  are combined into more complex tactics, which may
+ even be strategies complete for a class of problems. However, the
+ emphasis is not upon completeness but upon providing a metalogical
+ framework within which a user may express his insight into proof
+ methods and may delegate routine (but errorprone) work to the
+ computer. This method of tactic composition is presented at the start
+ of the paper in the form of an elementary theory of goalseeking. A
+ second ingredient of the methodology is the stratification of
+ machineassisted proof by an ancestry graph of applied theories, and
+ the example illustrates this stratification. In the final section,
+ some recent developments and applications of the method are cited.",
+ paper = "Miln84.pdf"
+}
+
@misc{Mohr14,
author = "MohringPaulin, Christine",
title = {{Introduction to the Calculus of Inductive Constructions}},
@@ 11922,6 +11998,28 @@ paper = "Brea89.pdf"
paper = "Soze12.pdf"
}
+@inproceedings{Spec18,
+ author = "SpectorZabusky, Antal and Breitner, Joachim and
+ Rizkallah, Christine and Weirich, Stephanie",
+ title = {{Total Haskell is Reasonable Coq}},
+ booktitle = "ACM SIGPLAN Int. Conf. on Certified Programs and
+ Proofs",
+ publisher = "ACM",
+ year = "2018",
+ abstract =
+ "We would like to use the Coq proof assistant to mechanically
+ verify properites of Haskell programs. To that end, we present a
+ tool, named {\tt hstocoq}, that translates total Haskell
+ programs into Coq programs via a shallow embedding. We apply our
+ tool in three case studies  a lawful {\tt Monad} instance,
+ ``Hutton's razor'', and an existing data structure library  and
+ prove their correctness. These examples show that this approach is
+ viable: both that {\tt hstocoq} applies to existing Haskell
+ code, and that the output it produces is amenable to
+ verification.",
+ paper = "Spec18.pdf"
+}
+
@misc{Stac17a,
author = "cstheory.stackexchange.com",
title = {{Why does Coq have Prop?}},
@@ 12115,6 +12213,38 @@ paper = "Brea89.pdf"
paper = "Wadl14.pdf"
}
+@article{Wald74,
+ author = "Waldinger, R.J. and Levitt, K.N.",
+ title = {{Reasoning about Programs}},
+ journal = "Artificial Intelligence",
+ volume = "5",
+ number = "3",
+ year = "1974",
+ pages = "235316",
+ abstract =
+ "This paper describes a theorem prover that embodies knowledge about
+ programming constructs, such as numbers, arrays, lists, and
+ expressions. The program can reason about these concepts and is used
+ as part of a program verification system that uses the FloydNaur
+ explication of program semantics. It is implemented in the qa4
+ language; the qa4 system allows many pieces of strategic knowledge,
+ each expressed as a small program, to be coordinated so that a program
+ stands forward when it is relevant to the problem at hand. The
+ language allows clear, concise representation of this sort of
+ knowledge. The qa4 system also has special facilities for dealing with
+ commutative functions, ordering relations, and equivalence relations;
+ these features are heavily used in this deductive system. The program
+ interrogates the user and asks his advice in the course of a
+ proof. Verifications have been found for Hoare's FIND program, a
+ realnumber division algorithm, and some sort programs, as well as for
+ many simpler algorithms. Additional theorems have been proved about a
+ pattern matcher and a version of Robinson's unification algorithm. The
+ appendix contains a complete, annotated listing of the deductive
+ system and annotated traces of several of the deductions performed by
+ the system.",
+ paper = "Wald74.pdf"
+}
+
@misc{Wals92,
author = "Walsh, Toby and Nunes, Alex and Bundy, Alan",
title = {{The Use of Proof Plans to Sum Series}},
@@ 31744,6 +31874,31 @@ paper = "Brea89.pdf"
isbn = "0486445186"
}
+@misc{Arma00,
+ author = "Armando, Alessandro and Zini, Daniele",
+ title = {{Towards Interoperable Mechanized Reasoning Systems:
+ The Logic Broker Architecture}},
+ year = "2000",
+ abstract =
+ "There is a growing interest in the integration of mechanized
+ reasoning systems such as automated theorem provers, computer algebra
+ systems, and model checkers. Stateoftheart reasoning systems are
+ the result of many manyears of careful development and engineering,
+ and usually they provide a high degree of sophistication in their
+ respective domain. Yet they often perform poorly when applied outside
+ the domain they have been designed for. The problem of integrating
+ mechanized reasoning systems is therefore being perceived as an
+ important issue in automated reasoning. In this paper we present
+ the Logic Broker Architecture, a framework which provides the needed
+ infrastructure for making mechanized reasoning systems interoperate.
+ The architecture provides location transparency, a way to forward
+ requests for logical services to appropriate reasoning systems via a
+ simple registration/subscription mechanism, and a translation
+ mechanism which ensures the transparent and provably sound exchange of
+ logical services.",
+ paper = "Arma00.pdf"
+}
+
@article{Aste02,
author = "Astesiano, Egidio and Bidoit, Michel and Kirchner, Helene and
KriegBruckner, Bernd and Mosses, Peter D. and Sannella, Donald
@@ 32233,7 +32388,7 @@ paper = "Brea89.pdf"
address = "INRIA Sophia Antipolis",
link =
"\url{http://wwwsop.inria.fr/cafe/Manuel.Bronstein/publications/issac98.pdf}",
 paper = "Bro98b.pdf"
+
}
@article{Brui94,
@@ 32261,6 +32416,18 @@ paper = "Brea89.pdf"
paper = "Brui94.pdf"
}
+@incollection{Brui94a,
+ author = "de Bruijn, N.G.",
+ title = {{The Mathematical Vernacular, a Language for Mathematics
+ with Typed Sets}},
+ booktitle = "Selected Papers on Automath",
+ pages = "865935",
+ year = "1994",
+ publisher = "NorthHolland",
+ link = "\url{https://pure.tue.nl/ws/files/2073504/610209.pdf}",
+ paper = "Brui94a.pdf"
+}
+
@article{Buch87,
author = "Buchberger, Bruno",
title = {{Applications of Gr\"obner Bases in NonLinear
@@ 32364,6 +32531,24 @@ paper = "Brea89.pdf"
paper = "Buch14.pdf"
}
+@incollection{Bund91,
+ author = "Bundy, Alan",
+ title = {{A Science of Reasoning (Extended Abstract)}},
+ booktitle = "Computational Logic: Essays in Honor of Alan
+ Robinson",
+ year = "1991",
+ publisher = "MIT Press",
+ abstract =
+ "How can we understand reasoning in general and mathematical proofs
+ in particular? It is argued that a highlevel understanding of proofs
+ is needed to complement the lowlevel understanding provided by
+ Logic. A role for computation is proposed to provide this highlevel
+ understanding, namely by the association of proof plans with
+ proofs. Criteria are given for assessing the association of a proof
+ plan with a proof.",
+ paper = "Bund91.pdf"
+}
+
@article{Burg74,
author = "William H. Burge",
title = {{Stream Processing Functions}},
@@ 32399,6 +32584,15 @@ paper = "Brea89.pdf"
paper = "Burs77.pdf"
}
+@misc{Busw04,
+ author = "Buswell, S. and Caprotti, O. and Carlisle, D.P. and Dewar, M.C.
+ and Gaetano, M. and Kohlhase, M.",
+ title = {{The OpenMath Standard}},
+ year = "2004",
+ link = "\url{https://www.openmath.org/standard/om2020040630/omstd20.pdf}",
+ paper = "Busw04.pdf"
+}
+
@inproceedings{Butl96,
author = "Butler, Greg",
title = {{Software Architectures for Computer Algebra: A Case Study}},
@@ 32464,6 +32658,13 @@ paper = "Brea89.pdf"
pages = "95101",
}
+@misc{Carl14,
+ author = "Carlisle, David and Ion, Patrick and Miner, Robert",
+ title = {{Mathematical Markup Language}},
+ year = "2014",
+ link = "\url{https://www.w3.org/TR/MathML3/}"
+}
+
@book{Char92,
author = "Char, B.W. and Geddes, K.O. and Gonnet, G.H. and Leong, B.L.
and Monagan, M.B. and Watt, S.M.",
@@ 32919,6 +33120,14 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@phdthesis{Elbe98,
+ author = "Elbers, Hugo Johannes",
+ title = {{Connecting Informal and Formal Mathematics}},
+ year = "1998",
+ school = "Technische Universiteit Eindhoven",
+ paper = "Elbe98.pdf"
+}
+
@inproceedings{Enge65,
author = "Engelman, C.",
title = {{A Program for OnLine Assistance in Symbolic Computation}},
@@ 33371,6 +33580,14 @@ paper = "Brea89.pdf"
paper = "Haya05.pdf"
}
+@inproceedings{Haye74,
+ author = "Hayes, Patrick J.",
+ title = {{Some Problems and Nonproblems in Representation Theory}},
+ booktitle = "AI and Simulation of Behaviour Conference",
+ year = "1974",
+ pages = "6379"
+}
+
@misc{Hear87,
author = "Hearn, Anthony",
title = {{REDUCE User's Manual}},
@@ 34140,6 +34357,23 @@ paper = "Brea89.pdf"
paper = "Lehn10.pdf"
}
+@inproceedings{Lest01,
+ author = "Lester, D.R.",
+ title = {{Effective Continued Fractions}},
+ booktitle = "15th IEEE Symp. on Computer Arithmetic",
+ publisher = "IEEE Computer Society Press",
+ year = "2001",
+ pages = "163170",
+ abstract =
+ "Only the leading seven terms of a continued fraction are needed to
+ perform online arithmetic, provided the continued fractions are of
+ the correct form. This forms the basis of a proof that there is an
+ effective representation of the computable reals as continued
+ fractions: we also demonstrate that the basic arithmetic operations
+ are computable using this representation.",
+ paper = "Lest01.pdf"
+}
+
@misc{Leve80,
author = "Levenworth, B.",
title = {{ADAPT Reference Manual}},
@@ 35443,6 +35677,36 @@ paper = "Brea89.pdf"
paper = "Thur94.pdf"
}
+@misc{Tryb02,
+ author = "Trybulec, Andrzej",
+ title = {{Towards Practical Formalizaiton of Mathematics}},
+ comment = "abstract",
+ link =
+ "\url{http://www.macs.hw.ac.uk/~fairouz/forest//events/automath2002/abstracts/Andrzej.abst.html}",
+ abstract =
+ "In sixties the opinion that mathematics cannot be practically
+ formalized was well established. So the main achievement of de Bruijn,
+ among many others, is the decision that the problem must be reconsider
+ and probably positively solved. And I believe that 1967 will be
+ treated by future historians of mathematics as a turning point.
+
+ It is not easy to say precisely what we learnt in the meantime, if we
+ learnt anything at all. I believe that the most important results are:
+ \begin{enumerate}
+ \item we need experiments with much more advanced mathematics than
+ already done
+ \item a system for practical formalization of mathematics probably will
+ not be a simple system based on small number of primitive notions
+ \item integration with a computer algebra systems may be necessary or at
+ least a feasible system must have bigger computational power.
+ \end{enumerate}
+
+ Still we should me more concerned with the original ideas of de
+ Bruijn, the most important that eventually we have to be able to
+ formalize new mathematical results, published in mathematical
+ newspapers in this century."
+}
+
@InProceedings{Mart99,
author = "Martin, Ursula",
title = {{Computers, reasoning and mathematical practice}},
@@ 35497,6 +35761,31 @@ paper = "Brea89.pdf"
\newline\refto{package PAFF PackageForAlgebraicFunctionField}"
}
+@techreport{Vuil87,
+ author = "Vuillemin, J.",
+ title = {{Exact Real Computer Arithmetic with Continued Fractions}},
+ institution = "Institut National de Recherche en Informatique et en
+ Automatique",
+ year = "1987",
+ number = "760",
+ abstract =
+ "We discuss a representation of the {\sl computable real numbers} by
+ continued fractions. This deals with the subtle points of undecidable
+ and integer division, as well as representing the infinite
+ $\infty=1/0$ and undefined $\bot=0/0$ numbers. Two general algorithms
+ for performing arithmetic operations are introduced. The
+ {\sl algebraic algorithm}, which computes sums and products of
+ continued fractions as a special case, basically operates in a
+ positional manner, producing one term of output for each term of
+ input. The {\sl transcendental algorithm} uses a general formula of
+ Gauss to compute the continued fractions of exponentials, logarithms,
+ trigonometric functions, as well as a wide class of special
+ functions. This work has been implemented in Le\_Lisp and the
+ performance of these algorithms appears to be quite good; however, no
+ competing system has been available for comparison",
+ paper = "Vuil87.pdf"
+}
+
@book{Walk78,
author = "Walker, Robert J.",
title = {{Algebraic Curves}},
@@ 35643,6 +35932,89 @@ paper = "Brea89.pdf"
link = "\url{http://www.cis.upenn.edu/~stevez/vellvm}"
}
+@phdthesis{Zinn04,
+ author = "Zinn, Claus",
+ title = {{Understanding Informal Mathematical Discourse}},
+ school = "Universitat Erlangen Nurnberg",
+ year = "2004",
+ abstract =
+ "Automated reasoning is one of the most established disciplines in
+ informatics and artificial intelligence, and formal methods become
+ increasingly employed in practical applications. However, for the most
+ part, such applications seem to be limited to informaticsspecific
+ areas (e.g., the verification of correctness properties of software
+ and hardware specifications) and areas close to informatics such as
+ computational linguistics (e.g., the computation of consistence and
+ informativeness properties of semantic representations). Naturally,
+ there is also a potential for practical applications in the the area
+ of mathematics: the generation of proofs for mathematically
+ interesting and motivated theorems and, quite associated, the
+ computersupported formalisation of (parts of elementary)
+ mathematics. It is a matter of fact, however, that mathematicians
+ rarely use computersupport for the construction and verification of
+ proofs. This is mainly caused by the “unnaturalness” of the language
+ and the reasoning that such proof engines support.
+
+ In the past, researchers in the area of automated reasoning have
+ focused their work on formalisms and algorithms that allow the
+ construction and verification of proofs that are written in a
+ formallogical language and that only use a limited number of
+ inference rules. For the computer scientist, such formal proofs have
+ the advantage of a simple and ambiguousfree syntax, which can thus be
+ easily processed. Moreover, the limited number of inference rules has
+ a direct impact on the complexity of the search space that needs to be
+ conquered during the process of constructing proofs. The verification
+ of given formal proofs is greatly facilitated by the complete
+ explicitness of their logical argumentation where no reasoning step is
+ left out. For mathematicians, however, such formal proofs are usually
+ hard to understand. For them, they are written in an unfamiliar and
+ artificial language and much too detailed. Moreover, the sheer number
+ of inference steps, while logically relevant, describe only trivial
+ mathematical details and make it difficult to follow a proof’s main
+ underlying argumentation line. In practise, thus, mathematicians use
+ proof generation engines rather seldom, if at all. The same is true
+ with regard to proof verification tools. The amount of work that is
+ required to verify a mathematical proof with such tools is
+ considerable, if not prohibitive. Since proof verification systems
+ only accept formal proofs as input, the mathematician’s first task is
+ to manually translate the mathematical proof into the formal language
+ that is accepted by the verifier. This in turn includes the
+ translation of the proof’s underlying mathematical argumentation into
+ inference rules that are supported by the proof engine. Such
+ translations and refinements are usually very time consuming, tedious,
+ and prone to error themselves. Hence, how the proof verifier then
+ judges the result of proof translation and proof refinement is only
+ of limited relevance to the original mathematical proof. From the
+ mathematician’s point of view, there is thus a need for a proof
+ verification system that is capable of processing mathematical proofs
+ automatically, at least with regard to translating the mathematicians’
+ expert language into the system’s artificial formal language. Such a
+ system would have an enormous potential in the community of
+ mathematics, and this potential has been recognised early. In the
+ beginning of the 1960s, John McCarthy, one of the pioneers of
+ artificial intelligence, remarked that ``[c]hecking mathematical proofs
+ is potentially one of the most interesting and useful applications of
+ automatic computers'' [111]. More than forty years thereafter, a tool
+ that supports mathematicians with the verification of mathematical
+ proofs is more science fiction than reality. Its realisation is
+ associated with research questions within the disciplines of automated
+ reasoning and computational linguistics that are still only partially
+ answered.
+
+ This thesis aims at contributing towards the realisation of a
+ verifier for mathematical proofs. It attempts to provide a general
+ framework as well as an implementation for such a proof
+ engine. The dissertation’s objects of study are short and simple
+ proofs that were taken from textbooks on elementary number
+ theory. Fig. 1 depicts a proof of the mathematical truth that
+ every positive integer greater than 1 can be represented as a
+ product of one or more primes. The proof consists of only a few
+ lines and little mathematical knowledge is necessary to follow the
+ proof author’s argumentation. It is this kind of short proof that
+ we attempt to check automatically.",
+ paper = "Zinn04.pdf"
+}
+
@misc{OCon08,
author = "O'Connor, Christine",
title = {{Christine Jeanne O'Connor Obituary}},
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 6585628..987e071 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 26,6 +26,18 @@ paragraph for those unfamiliar with the terms.
\section{Axiom Literate Sources}
+\index{Daly, Timothy}
+\index{Botch, Mark}
+\begin{chunk}{axiom.bib}
+@misc{Daly17,
+ author = "Daly, Timothy and Botch, Mark",
+ title = {{Axiom Developer Website}},
+ link = "\url{http://axiomdeveloper.org}",
+ year = "2017"
+}
+
+\end{chunk}
+
\index{Axiom Authors}
\begin{chunk}{axiom.bib}
@book{Book00,
@@ 10205,10 +10217,11 @@ when shown in factored form.
\index{Beeson, Michael}
\begin{chunk}{axiom.bib}
@misc{Beesxx,
+@misc{Bees98,
author = "Beeson, Michael",
title = {{Automatic Generation of EpsilonDelta Proofs of Continuity}},
link = "\url{http://www.michaelbeeson.com/research/papers/aisc.pdf}",
+ year = "1998",
abstract =
"As part of a project on automatic generation of proofs involving both
logic and computation, we have automated the production of some proofs
@@ 10222,7 +10235,7 @@ when shown in factored form.
for intermixing logical deduction steps with computational steps and
with inequality reasoning. Problems discussed here as examples involve
the continuity and uniform continuity of various specific functions.",
 paper = "Beesxx.pdf"
+ paper = "Bees98.pdf"
}
\end{chunk}
@@ 10864,8 +10877,8 @@ when shown in factored form.
\index{de Bruijn, N.G.}
\begin{chunk}{axiom.bib}
\article{Brui68,
 author = "de Bruijn, N.G."
+@article{Brui68,
+ author = "de Bruijn, N.G.",
title = {{The Mathematical Language Automath, its Usage, and Some of
its Extensions}},
journal = "Lecture Notes in Mathematics",
@@ 11375,6 +11388,32 @@ when shown in factored form.
\end{chunk}
+\index{Carette, Jacques}
+\index{Farmer, William M.}
+\index{Wajs, Jeremie}
+\begin{chunk}{axiom.bib}
+@misc{Care11b,
+ author = "Carette, Jacques and Farmer, William M. and Wajs, Jeremie",
+ title = {{Trustable Communication Between Mathematics Systems}},
+ year = "2011",
+ link = "\url{https://pdfs.semanticscholar.org/0d0b/206edf7ef1c01d7bfa1284c85b469b2fbd29.pdf}",
+ abstract =
+ "This paper presents a rigorous, unified framework for facilitating
+ communication between mathematics systems. A mathematics system is
+ given one or more interfaces which offer deductive and computational
+ services to other mathematics systems. To achieve communication
+ between systems, a client interface is linked to a server interface by
+ an asymmetric connection consisting of a pair of translations.
+ Answers to requests are trustable in the sense that they are correct
+ provided a small set of prescribed conditions are satisfied. The
+ frame work is robust with respect to interface extension and can
+ process requests for abstract services, where the server interface is
+ not fully specified.",
+ paper = "Care11b.pdf"
+}
+
+\end{chunk}
+
\index{Chlipala, Adam}
\begin{chunk}{axiom.bib}
@article{Chli10,
@@ 12234,7 +12273,6 @@ when shown in factored form.
\subsection{F} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\index{Farmer, William H.}
\begin{chunk}{axiom.bib}
@article{Farm92a,
@@ 12464,6 +12502,19 @@ when shown in factored form.
\end{chunk}
+\index{Floyd, W.}
+\begin{chunk}{axiom.bib}
+@incollection{Floy86,
+ author = "Floyd, W.",
+ title = {{Toward Interactive Design of Correct Programs}},
+ booktitle = "Reading in Artificial Intelligence and Software Engeering",
+ pages = "331334",
+ year = "1986",
+ isbn = "0934613125"
+}
+
+\end{chunk}
+
\index{Frade, Maria Joao}
\begin{chunk}{axiom.bib}
@article{Frad08,
@@ 12704,7 +12755,8 @@ when shown in factored form.
type = "technical report",
number = "940915",
instituion = "IRST Trento Italy",
 year = "1994"
+ year = "1994",
+ paper = "Giun94.pdf"
}
\end{chunk}
@@ 13298,7 +13350,7 @@ when shown in factored form.
abstract =
"This paper describes an implementation within Nuprl of mechanisms
that support the use of Nuprl's type theory as a language for
 constructing theoremprovind procedures. The main componenet of the
+ constructing theoremproving procedures. The main component of the
implementation is a large library of definitions, theorems and
proofs. This library may be regarded as the beginning of a book of
formal mathematics; it contains the formal development and explanation
@@ 14269,6 +14321,20 @@ when shown in factored form.
\end{chunk}
+\index{Maurer, D.}
+\begin{chunk}{axiom.bib}
+@article{Maur73,
+ author = "Maurer, D.",
+ title = {{Applications of Symbolic Mathematical Manipulation to
+ Algorithmic Verification (Abstract)}},
+ journal = "SIGSAM Bulletin",
+ volume = "26",
+ year = "1973",
+ pages = "4"
+}
+
+\end{chunk}
+
\index{McAllester, D.}
\index{Arkondas, K.}
\begin{chunk}{axiom.bib}
@@ 14470,7 +14536,6 @@ when shown in factored form.
\end{chunk}

\index{Meshveliani, Sergei D.}
\begin{chunk}{axiom.bib}
@misc{Mesh13,
@@ 14689,6 +14754,38 @@ when shown in factored form.
\end{chunk}
+\index{Milner, R.}
+\begin{chunk}{axiom.bib}
+@article{Miln84,
+ author = "Milner, R.",
+ title = {{The Use of Machines to Assist in Rigorous Proof}},
+ journal = "Philosophical Transactions of the Royal Society",
+ volume = "312",
+ pages = "411422",
+ number = "1522",
+ year = "1984",
+ abstract =
+ "A methodology for computer assisted proof is presented with an
+ example. A central ingredient in the method is the presentation of
+ tactics (or strategies) in an algorithmic metalanguage. Further, the
+ same language is also used to express combinators, by which simple
+ elementary tactics  which often correspond to the inference rules of
+ the logic employed  are combined into more complex tactics, which may
+ even be strategies complete for a class of problems. However, the
+ emphasis is not upon completeness but upon providing a metalogical
+ framework within which a user may express his insight into proof
+ methods and may delegate routine (but errorprone) work to the
+ computer. This method of tactic composition is presented at the start
+ of the paper in the form of an elementary theory of goalseeking. A
+ second ingredient of the methodology is the stratification of
+ machineassisted proof by an ancestry graph of applied theories, and
+ the example illustrates this stratification. In the final section,
+ some recent developments and applications of the method are cited.",
+ paper = "Miln84.pdf"
+}
+
+\end{chunk}
+
\index{MohringPaulin, Christine}
\begin{chunk}{axiom.bib}
@misc{Mohr14,
@@ 15863,6 +15960,35 @@ when shown in factored form.
\end{chunk}
+\index{SpectorZabusky, Antal}
+\index{Breitner, Joachim}
+\index{Rizkallah, Christine}
+\index{Weirich, Stephanie}
+\begin{chunk}{axiom.bib}
+@inproceedings{Spec18,
+ author = "SpectorZabusky, Antal and Breitner, Joachim and
+ Rizkallah, Christine and Weirich, Stephanie",
+ title = {{Total Haskell is Reasonable Coq}},
+ booktitle = "ACM SIGPLAN Int. Conf. on Certified Programs and
+ Proofs",
+ publisher = "ACM",
+ year = "2018",
+ abstract =
+ "We would like to use the Coq proof assistant to mechanically
+ verify properites of Haskell programs. To that end, we present a
+ tool, named {\tt hstocoq}, that translates total Haskell
+ programs into Coq programs via a shallow embedding. We apply our
+ tool in three case studies  a lawful {\tt Monad} instance,
+ ``Hutton's razor'', and an existing data structure library  and
+ prove their correctness. These examples show that this approach is
+ viable: both that {\tt hstocoq} applies to existing Haskell
+ code, and that the output it produces is amenable to
+ verification.",
+ paper = "Spec18.pdf"
+}
+
+\end{chunk}
+
\begin{chunk}{axiom.bib}
@misc{Stac17a,
author = "cstheory.stackexchange.com",
@@ 16118,6 +16244,43 @@ when shown in factored form.
\end{chunk}
+\index{Waldinger, R.J.}
+\index{Levitt, K.N.}
+\begin{chunk}{axiom.bib}
+@article{Wald74,
+ author = "Waldinger, R.J. and Levitt, K.N.",
+ title = {{Reasoning about Programs}},
+ journal = "Artificial Intelligence",
+ volume = "5",
+ number = "3",
+ year = "1974",
+ pages = "235316",
+ abstract =
+ "This paper describes a theorem prover that embodies knowledge about
+ programming constructs, such as numbers, arrays, lists, and
+ expressions. The program can reason about these concepts and is used
+ as part of a program verification system that uses the FloydNaur
+ explication of program semantics. It is implemented in the qa4
+ language; the qa4 system allows many pieces of strategic knowledge,
+ each expressed as a small program, to be coordinated so that a program
+ stands forward when it is relevant to the problem at hand. The
+ language allows clear, concise representation of this sort of
+ knowledge. The qa4 system also has special facilities for dealing with
+ commutative functions, ordering relations, and equivalence relations;
+ these features are heavily used in this deductive system. The program
+ interrogates the user and asks his advice in the course of a
+ proof. Verifications have been found for Hoare's FIND program, a
+ realnumber division algorithm, and some sort programs, as well as for
+ many simpler algorithms. Additional theorems have been proved about a
+ pattern matcher and a version of Robinson's unification algorithm. The
+ appendix contains a complete, annotated listing of the deductive
+ system and annotated traces of several of the deductions performed by
+ the system.",
+ paper = "Wald74.pdf"
+}
+
+\end{chunk}
+
\index{Walsh, Toby}
\index{Nunes, Alex}
\index{Bundy, Alan}
@@ 46667,6 +46830,36 @@ National Physical Laboratory. (1982)
\end{chunk}
+\index{Armando, Alessandro}
+\index{Zini, Daniele}
+\begin{chunk}{axiom.bib}
+@misc{Arma00,
+ author = "Armando, Alessandro and Zini, Daniele",
+ title = {{Towards Interoperable Mechanized Reasoning Systems:
+ The Logic Broker Architecture}},
+ year = "2000",
+ abstract =
+ "There is a growing interest in the integration of mechanized
+ reasoning systems such as automated theorem provers, computer algebra
+ systems, and model checkers. Stateoftheart reasoning systems are
+ the result of many manyears of careful development and engineering,
+ and usually they provide a high degree of sophistication in their
+ respective domain. Yet they often perform poorly when applied outside
+ the domain they have been designed for. The problem of integrating
+ mechanized reasoning systems is therefore being perceived as an
+ important issue in automated reasoning. In this paper we present
+ the Logic Broker Architecture, a framework which provides the needed
+ infrastructure for making mechanized reasoning systems interoperate.
+ The architecture provides location transparency, a way to forward
+ requests for logical services to appropriate reasoning systems via a
+ simple registration/subscription mechanism, and a translation
+ mechanism which ensures the transparent and provably sound exchange of
+ logical services.",
+ paper = "Arma00.pdf"
+}
+
+\end{chunk}
+
\index{Astesiano, Egidio}
\index{Bidoit, Michel}
\index{Kirchner, Helene}
@@ 47518,7 +47711,7 @@ ISBN 3764359013 (1998)
address = "INRIA Sophia Antipolis",
link =
"\url{http://wwwsop.inria.fr/cafe/Manuel.Bronstein/publications/issac98.pdf}",
 paper = "Bro98b.pdf"
+
}
\end{chunk}
@@ 47552,6 +47745,22 @@ ISBN 3764359013 (1998)
\end{chunk}
+\index{de Bruijn, N.G.}
+\begin{chunk}{axiom.bib}
+@incollection{Brui94a,
+ author = "de Bruijn, N.G.",
+ title = {{The Mathematical Vernacular, a Language for Mathematics
+ with Typed Sets}},
+ booktitle = "Selected Papers on Automath",
+ pages = "865935",
+ year = "1994",
+ publisher = "NorthHolland",
+ link = "\url{https://pure.tue.nl/ws/files/2073504/610209.pdf}",
+ paper = "Brui94a.pdf"
+}
+
+\end{chunk}
+
\index{Buchberger, Bruno}
\begin{chunk}{axiom.bib}
@article{Buch87,
@@ 47624,7 +47833,7 @@ ISBN 3764359013 (1998)
}
\end{chunk}
b
+
\index{Buchberger, B.}
\begin{chunk}{axiom.bib}
@book{Buch96,
@@ 47679,6 +47888,28 @@ b
\end{chunk}
+\index{Bundy, Alan}
+\begin{chunk}{axiom.bib}
+@incollection{Bund91,
+ author = "Bundy, Alan",
+ title = {{A Science of Reasoning (Extended Abstract)}},
+ booktitle = "Computational Logic: Essays in Honor of Alan
+ Robinson",
+ year = "1991",
+ publisher = "MIT Press",
+ abstract =
+ "How can we understand reasoning in general and mathematical proofs
+ in particular? It is argued that a highlevel understanding of proofs
+ is needed to complement the lowlevel understanding provided by
+ Logic. A role for computation is proposed to provide this highlevel
+ understanding, namely by the association of proof plans with
+ proofs. Criteria are given for assessing the association of a proof
+ plan with a proof.",
+ paper = "Bund91.pdf"
+}
+
+\end{chunk}
+
\index{Burge, William H.}
\begin{chunk}{axiom.bib}
@article{Burg74,
@@ 47723,6 +47954,24 @@ b
\end{chunk}
+\index{Buswell, S.}
+\index{Caprotti, O.}
+\index{Carlisle, D.P.}
+\index{Dewar, M.C.}
+\index{Gaetano, M.}
+\index{Kohlhase, M.}
+\begin{chunk}{axiom.bib}
+@misc{Busw04,
+ author = "Buswell, S. and Caprotti, O. and Carlisle, D.P. and Dewar, M.C.
+ and Gaetano, M. and Kohlhase, M.",
+ title = {{The OpenMath Standard}},
+ year = "2004",
+ link = "\url{https://www.openmath.org/standard/om2020040630/omstd20.pdf}",
+ paper = "Busw04.pdf"
+}
+
+\end{chunk}
+
\index{Butler, Greg}
\begin{chunk}{axiom.bib}
@inproceedings{Butl96,
@@ 47803,6 +48052,19 @@ b
\end{chunk}
+\index{Carlisle, David}
+\index{Ion, Patrick}
+\index{Miner, Robert}
+\begin{chunk}{axiom.bib}
+@misc{Carl14,
+ author = "Carlisle, David and Ion, Patrick and Miner, Robert",
+ title = {{Mathematical Markup Language}},
+ year = "2014",
+ link = "\url{https://www.w3.org/TR/MathML3/}"
+}
+
+\end{chunk}
+
\index{Carlson, B. C.}
\begin{chunk}{ignore}
\bibitem[Carlson 65]{Car65} Carlson, B C
@@ 48874,6 +49136,18 @@ A.E.R.E. Report R.8730. HMSO. (1977)
\subsection{E} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Elbers, Hugo Johannes}
+\begin{chunk}{axiom.bib}
+@phdthesis{Elbe98,
+ author = "Elbers, Hugo Johannes",
+ title = {{Connecting Informal and Formal Mathematics}},
+ year = "1998",
+ school = "Technische Universiteit Eindhoven",
+ paper = "Elbe98.pdf"
+}
+
+\end{chunk}
+
\index{Engelman, C.}
\begin{chunk}{axiom.bib}
@inproceedings{Enge65,
@@ 49968,6 +50242,18 @@ J. Inst. Math. Appl. 14 89103. (1974)
\end{chunk}
+\index{Hayes, Patrick J.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Haye74,
+ author = "Hayes, Patrick J.",
+ title = {{Some Problems and Nonproblems in Representation Theory}},
+ booktitle = "AI and Simulation of Behaviour Conference",
+ year = "1974",
+ pages = "6379"
+}
+
+\end{chunk}
+
\index{Hearn, Anthony}
\begin{chunk}{axiom.bib}
@misc{Hear87,
@@ 51185,6 +51471,27 @@ PrenticeHall. (1974)
\end{chunk}
+\index{Lester, D.R.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Lest01,
+ author = "Lester, D.R.",
+ title = {{Effective Continued Fractions}},
+ booktitle = "15th IEEE Symp. on Computer Arithmetic",
+ publisher = "IEEE Computer Society Press",
+ year = "2001",
+ pages = "163170",
+ abstract =
+ "Only the leading seven terms of a continued fraction are needed to
+ perform online arithmetic, provided the continued fractions are of
+ the correct form. This forms the basis of a proof that there is an
+ effective representation of the computable reals as continued
+ fractions: we also demonstrate that the basic arithmetic operations
+ are computable using this representation.",
+ paper = "Lest01.pdf"
+}
+
+\end{chunk}
+
\index{Levenworth, B.}
\begin{chunk}{axiom.bib}
@misc{Leve80,
@@ 53724,6 +54031,40 @@ J. Comput. Phys. 52 340350. (1983)
\end{chunk}
+\index{Trybulec, Andrzej}
+\begin{chunk}{axiom.bib}
+@misc{Tryb02,
+ author = "Trybulec, Andrzej",
+ title = {{Towards Practical Formalizaiton of Mathematics}},
+ comment = "abstract",
+ link =
+ "\url{http://www.macs.hw.ac.uk/~fairouz/forest//events/automath2002/abstracts/Andrzej.abst.html}",
+ abstract =
+ "In sixties the opinion that mathematics cannot be practically
+ formalized was well established. So the main achievement of de Bruijn,
+ among many others, is the decision that the problem must be reconsider
+ and probably positively solved. And I believe that 1967 will be
+ treated by future historians of mathematics as a turning point.
+
+ It is not easy to say precisely what we learnt in the meantime, if we
+ learnt anything at all. I believe that the most important results are:
+ \begin{enumerate}
+ \item we need experiments with much more advanced mathematics than
+ already done
+ \item a system for practical formalization of mathematics probably will
+ not be a simple system based on small number of primitive notions
+ \item integration with a computer algebra systems may be necessary or at
+ least a feasible system must have bigger computational power.
+ \end{enumerate}
+
+ Still we should me more concerned with the original ideas of de
+ Bruijn, the most important that eventually we have to be able to
+ formalize new mathematical results, published in mathematical
+ newspapers in this century."
+}
+
+\end{chunk}
+
\subsection{U} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{chunk}{ignore}
@@ 53829,6 +54170,35 @@ SIAM Philadelphia. (1992)
\end{chunk}
+\index{Vuillemin, J.}
+\begin{chunk}{axiom.bib}
+@techreport{Vuil87,
+ author = "Vuillemin, J.",
+ title = {{Exact Real Computer Arithmetic with Continued Fractions}},
+ institution = "Institut National de Recherche en Informatique et en
+ Automatique",
+ year = "1987",
+ number = "760",
+ abstract =
+ "We discuss a representation of the {\sl computable real numbers} by
+ continued fractions. This deals with the subtle points of undecidable
+ and integer division, as well as representing the infinite
+ $\infty=1/0$ and undefined $\bot=0/0$ numbers. Two general algorithms
+ for performing arithmetic operations are introduced. The
+ {\sl algebraic algorithm}, which computes sums and products of
+ continued fractions as a special case, basically operates in a
+ positional manner, producing one term of output for each term of
+ input. The {\sl transcendental algorithm} uses a general formula of
+ Gauss to compute the continued fractions of exponentials, logarithms,
+ trigonometric functions, as well as a wide class of special
+ functions. This work has been implemented in Le\_Lisp and the
+ performance of these algorithms appears to be quite good; however, no
+ competing system has been available for comparison",
+ paper = "Vuil87.pdf"
+}
+
+\end{chunk}
+
\subsection{W} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Wait, R.}
@@ 54246,6 +54616,93 @@ Math. Tables Aids Comput. 10 9196. (1956)
\end{chunk}
+\index{Zinn, Claus}
+\begin{chunk}{axiom.bib}
+@phdthesis{Zinn04,
+ author = "Zinn, Claus",
+ title = {{Understanding Informal Mathematical Discourse}},
+ school = "Universitat Erlangen Nurnberg",
+ year = "2004",
+ abstract =
+ "Automated reasoning is one of the most established disciplines in
+ informatics and artificial intelligence, and formal methods become
+ increasingly employed in practical applications. However, for the most
+ part, such applications seem to be limited to informaticsspecific
+ areas (e.g., the verification of correctness properties of software
+ and hardware specifications) and areas close to informatics such as
+ computational linguistics (e.g., the computation of consistence and
+ informativeness properties of semantic representations). Naturally,
+ there is also a potential for practical applications in the the area
+ of mathematics: the generation of proofs for mathematically
+ interesting and motivated theorems and, quite associated, the
+ computersupported formalisation of (parts of elementary)
+ mathematics. It is a matter of fact, however, that mathematicians
+ rarely use computersupport for the construction and verification of
+ proofs. This is mainly caused by the “unnaturalness” of the language
+ and the reasoning that such proof engines support.
+
+ In the past, researchers in the area of automated reasoning have
+ focused their work on formalisms and algorithms that allow the
+ construction and verification of proofs that are written in a
+ formallogical language and that only use a limited number of
+ inference rules. For the computer scientist, such formal proofs have
+ the advantage of a simple and ambiguousfree syntax, which can thus be
+ easily processed. Moreover, the limited number of inference rules has
+ a direct impact on the complexity of the search space that needs to be
+ conquered during the process of constructing proofs. The verification
+ of given formal proofs is greatly facilitated by the complete
+ explicitness of their logical argumentation where no reasoning step is
+ left out. For mathematicians, however, such formal proofs are usually
+ hard to understand. For them, they are written in an unfamiliar and
+ artificial language and much too detailed. Moreover, the sheer number
+ of inference steps, while logically relevant, describe only trivial
+ mathematical details and make it difficult to follow a proof’s main
+ underlying argumentation line. In practise, thus, mathematicians use
+ proof generation engines rather seldom, if at all. The same is true
+ with regard to proof verification tools. The amount of work that is
+ required to verify a mathematical proof with such tools is
+ considerable, if not prohibitive. Since proof verification systems
+ only accept formal proofs as input, the mathematician’s first task is
+ to manually translate the mathematical proof into the formal language
+ that is accepted by the verifier. This in turn includes the
+ translation of the proof’s underlying mathematical argumentation into
+ inference rules that are supported by the proof engine. Such
+ translations and refinements are usually very time consuming, tedious,
+ and prone to error themselves. Hence, how the proof verifier then
+ judges the result of proof translation and proof refinement is only
+ of limited relevance to the original mathematical proof. From the
+ mathematician’s point of view, there is thus a need for a proof
+ verification system that is capable of processing mathematical proofs
+ automatically, at least with regard to translating the mathematicians’
+ expert language into the system’s artificial formal language. Such a
+ system would have an enormous potential in the community of
+ mathematics, and this potential has been recognised early. In the
+ beginning of the 1960s, John McCarthy, one of the pioneers of
+ artificial intelligence, remarked that ``[c]hecking mathematical proofs
+ is potentially one of the most interesting and useful applications of
+ automatic computers'' [111]. More than forty years thereafter, a tool
+ that supports mathematicians with the verification of mathematical
+ proofs is more science fiction than reality. Its realisation is
+ associated with research questions within the disciplines of automated
+ reasoning and computational linguistics that are still only partially
+ answered.
+
+ This thesis aims at contributing towards the realisation of a
+ verifier for mathematical proofs. It attempts to provide a general
+ framework as well as an implementation for such a proof
+ engine. The dissertation’s objects of study are short and simple
+ proofs that were taken from textbooks on elementary number
+ theory. Fig. 1 depicts a proof of the mathematical truth that
+ every positive integer greater than 1 can be represented as a
+ product of one or more primes. The proof consists of only a few
+ lines and little mathematical knowledge is necessary to follow the
+ proof author’s argumentation. It is this kind of short proof that
+ we attempt to check automatically.",
+ paper = "Zinn04.pdf"
+}
+
+\end{chunk}
+
\index{O'Connor, Christine}
\begin{chunk}{axiom.bib}
@misc{OCon08,
diff git a/changelog b/changelog
index 9aac25e..fbda247 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20171202 tpd src/axiomwebsite/patches.html 20171202.01.tpd.patch
+20171202 tpd books/bookvolbib add references
20171127 tpd src/axiomwebsite/patches.html 20171127.01.tpd.patch
20171127 tpd books/bookvolbib add references
20171115 tpd src/axiomwebsite/patches.html 20171115.01.tpd.patch
diff git a/patch b/patch
index 66b8e8a..2cd26dc 100644
 a/patch
+++ b/patch
@@ 2,248 +2,490 @@ books/bookvolbib add references
Goal: Proving Axiom Correct
\index{Hamlet, Dick}
+\index{Maurer, D.}
\begin{chunk}{axiom.bib}
@inproceedings{Haml02,
 author = "Hamlet, Dick",
 title = {{Continuity in Software Systems}},
 booktitle = "ISSTA 2002 Int. Symp. on Software Testing and Analysis",
 pages = "196200",
 year = "2002",
+@article{Maur73,
+ author = "Maurer, D.",
+ title = {{Applications of Symbolic Mathematical Manipulation to
+ Algorithmic Verification (Abstract)},
+ journal = "SIGSAM Bulletin",
+ volume = "26",
+ year = "1973",
+ pages = "4"
}
\end{chunk}
\index{Fateman, Richard J.}
+\index{Waldinger, R.J.}
+\index{Levitt, K.N.}
\begin{chunk}{axiom.bib}
@inproceedings{Fate90a,
 author = "Fateman, Richard J.",
 title = {{Advances and Trends in the Design of Algebraic
 Manipulation Systems}},
 booktitle = "Proc. ISSAC'90",
 pages = "6067",
 year = "1990"
+@article{Wald74,
+ author = "Waldinger, R.J. and Levitt, K.N.",
+ title = {{Reasoning about Programs}},
+ journal = "Artificial Intelligence",
+ volume = "5",
+ number = "3",
+ year = "1974",
+ pages = "235316",
+ abstract =
+ "This paper describes a theorem prover that embodies knowledge about
+ programming constructs, such as numbers, arrays, lists, and
+ expressions. The program can reason about these concepts and is used
+ as part of a program verification system that uses the FloydNaur
+ explication of program semantics. It is implemented in the qa4
+ language; the qa4 system allows many pieces of strategic knowledge,
+ each expressed as a small program, to be coordinated so that a program
+ stands forward when it is relevant to the problem at hand. The
+ language allows clear, concise representation of this sort of
+ knowledge. The qa4 system also has special facilities for dealing with
+ commutative functions, ordering relations, and equivalence relations;
+ these features are heavily used in this deductive system. The program
+ interrogates the user and asks his advice in the course of a
+ proof. Verifications have been found for Hoare's FIND program, a
+ realnumber division algorithm, and some sort programs, as well as for
+ many simpler algorithms. Additional theorems have been proved about a
+ pattern matcher and a version of Robinson's unification algorithm. The
+ appendix contains a complete, annotated listing of the deductive
+ system and annotated traces of several of the deductions performed by
+ the system.",
+ paper = "Wald74.pdf"
}
\end{chunk}
\index{Beeson, M.}
+\index{Floyd, W.}
\begin{chunk}{axiom.bib}
@article{Bees92,
 author = "Beeson, M.",
 title = {{Mathpert: Computer support for learning algebra, trig, and
 calculus}},
 journal = "LNCS",
 volume = "624",
 pages = "454456",
 year = "1992",
 abstract =
 "Mathpert is a computerized environment for learning algebra, trig,
 and onevariable calculus. It permits students to direct the
 stepbystep solution of problems, and is capable of helping them
 by solving the problems itself if necessary.",
 paper = "Bees92.pdf"
+@incollection{Floy86,
+ author = "Floyd, W.",
+ title = {{Toward Interactive Design of Correct Programs}},
+ booktitle = "Reading in Artificial Intelligence and Software Engeering",
+ pages = "331334",
+ year = "1986",
+ isbn = "0934613125"
}
\end{chunk}
\index{Dijkstra, Edsger}
+\index{Milner, R.}
\begin{chunk}{axiom.bib}
@misc{Dijk72,
 author = "Dijkstra, Edsger",
 title = {{The Humble Programmer}},
 year = "1972",
 number = "EWD340",
 comment = "ACM Turing Lecture 1972",
 paper = "Dijk72.txt"
+@article{Miln84,
+ author = "Milner, R.",
+ title = {{The Use of Machines to Assist in Rigorous Proof}},
+ journal = "Philosophical Transactions of the Royal Society",
+ volume = "312",
+ pages = "411422",
+ number = "1522",
+ year = "1984",
+ abstract =
+ "A methodology for computer assisted proof is presented with an
+ example. A central ingredient in the method is the presentation of
+ tactics (or strategies) in an algorithmic metalanguage. Further, the
+ same language is also used to express combinators, by which simple
+ elementary tactics  which often correspond to the inference rules of
+ the logic employed  are combined into more complex tactics, which may
+ even be strategies complete for a class of problems. However, the
+ emphasis is not upon completeness but upon providing a metalogical
+ framework within which a user may express his insight into proof
+ methods and may delegate routine (but errorprone) work to the
+ computer. This method of tactic composition is presented at the start
+ of the paper in the form of an elementary theory of goalseeking. A
+ second ingredient of the methodology is the stratification of
+ machineassisted proof by an ancestry graph of applied theories, and
+ the example illustrates this stratification. In the final section,
+ some recent developments and applications of the method are cited.",
+ paper = "Miln84.pdf"
}
\end{chunk}
\index{Suppes, Patrick}
\index{Smith, Robert}
\index{Beard, Marian}
+\index{Giunchiglia, Fausto}
+\index{Pecchiari, Paolo}
+\index{Talcott, Carolyn}
\begin{chunk}{axiom.bib}
@article{Supp77,
 author = "Suppes, Patrick and Smith, Robert and Beard, Marian",
 title = {{UniversityLevel ComputerAssisted Instruction at Stanford: 1975}},
 journal = "Instructional Science",
 volume = "6",
 year = "1977",
 pages = "151185",
+@techreport{Giun94,
+ author = "Giunchiglia, Fausto and Pecchiari, Paolo and Talcott, Carolyn",
+ title = {{Reasoning Theories  Towards an Architecture for Open
+ Mechanized Reasoning}},
+ year = "1994",
+ institution = "Stanford University",
abstract =
 "This article provides an overview of current work on universitylevel
 computer assisted instruction at Stanford University. Brief
 descriptions are given of the main areas of current interest. The
 main emphasis is on the courses now being used: Introduction to Logic,
 Axiomatic Set Theory, Old Church Slavonic, History of the Russian
 Literary Language, Introduction to Bulgarian, Introduction to BASIC,
 Introduction to LISP, and various courses in music.",
 paper = "Supp77.pdf"
+ "Our ultimate goal is to provide a framework and a methodology which
+ will allow users, and not only system developers, to construct complex
+ reasoning systems by composing existing modules, or to add new modules
+ to existing systems, in a "plug and play" manner. These modules and
+ systems might be based on different logics; have different domain
+ models; use different vocabularies and data structures; use different
+ reasoning strategies; and have different interaction
+ capabilities. This paper makes two main contributions towards our
+ goal. First, it proposes a general architecture for a class of
+ reasoning systems called Open Mechanized Reasoning Systems (OMRSs). An
+ OMRS has three components: a reasoning theory component which is the
+ counterpart of the logical notion of formal system, a control
+ component which consists of a set of inference strategies, and an
+ interaction component which provides an OMRS with the capability of
+ interacting with other systems, including OMRSs and hum...",
+ paper = "Giun94.pdf"
}
\end{chunk}
\index{Char, B.W.}
\index{Geddes, K.O.}
\index{Gonnet, G.H.}
\index{Leong, B.L.}
\index{Monagan, M.B.}
\index{Watt, S.M.}
+\index{Carette, Jacques}
+\index{Farmer, William M.}
+\index{Wajs, Jeremie}
\begin{chunk}{axiom.bib}
@book{Char92,
 author = "Char, B.W. and Geddes, K.O. and Gonnet, G.H. and Leong, B.L.
 and Monagan, M.B. and Watt, S.M.",
 title = {{A Tutorial Introduction to Maple V}},
 year = "1992",
 publisher = "SpringerVerlag"
+@misc{Care11b,
+ author = "Carette, Jacques and Farmer, William M. and Wajs, Jeremie",
+ title = {{Trustable Communication Between Mathematics Systems}},
+ year = "2011",
+ link = "\url{https://pdfs.semanticscholar.org/0d0b/206edf7ef1c01d7bfa1284c85b469b2fbd29.pdf}",
+ abstract =
+ "This paper presents a rigorous, unified framework for facilitating
+ communication between mathematics systems. A mathematics system is
+ given one or more interfaces which offer deductive and computational
+ services to other mathematics systems. To achieve communication
+ between systems, a client interface is linked to a server interface by
+ an asymmetric connection consisting of a pair of translations.
+ Answers to requests are trustable in the sense that they are correct
+ provided a small set of prescribed conditions are satisfied. The
+ frame work is robust with respect to interface extension and can
+ process requests for abstract services, where the server interface is
+ not fully specified.",
+ paper = "Care11b.pdf"
}
\end{chunk}
\index{Harrison, John}
+\index{Carlisle, David}
+\index{Ion, Patrick}
+\index{Miner, Robert}
\begin{chunk}{axiom.bib}
@article{Harr94a,
 author = "Harrison, John",
 title = {{Constructing the Real Numbers in HOL}},
 journal = "Formal Methods in Systems Design",
 volume = "5",
 pages = "3539",
 year = "1994",
 abstract =
 "This paper describes a construction of the real numbers in the HOL
 theoremprover by strictly definitional means using a version of
 Dedekind's method. It also outlines the theory of mathematical
 analysis that has been built on top of it and discusses current and
 potential applications in verification and computer algebra.",
 paper = "Harr94a.pdf"
+@misc{Carl14,
+ author = "Carlisle, David and Ion, Patrick and Miner, Robert",
+ title = {{Mathematical Markup Language}},
+ year = "2014",
+ link = "\url{https://www.w3.org/TR/MathML3/}"
}
\end{chunk}
\index{Gordon, M.}
\index{Melham, T.}
+\index{Buswell, S.}
+\index{Caprotti, O.}
+\index{Carlisle, D.P.}
+\index{Dewar, M.C.}
+\index{Gaetano, M.}
+\index{Kohlhase, M.}
\begin{chunk}{axiom.bib}
@book{Gord93,
 author = "Gordon, M. and Melham, T.",
 title = {{Introduction to HOL}},
 publisher = "Cambridge University Press",
 year = "1993"
+@misc{Busw04,
+ author = "Buswell, S. and Caprotti, O. and Carlisle, D.P. and Dewar, M.C.
+ and Gaetano, M. and Kohlhase, M.",
+ title = {{The OpenMath Standard}},
+ year = "2004",
+ link = "\url{https://www.openmath.org/standard/om2020040630/omstd20.pdf}",
+ paper = "Busw04.pdf"
}
\end{chunk}
\index{Igarashi, Shigeru}
\index{London, Ralph L.}
\index{Luckham, David C.}
+\index{Armando, Alessandro}
+\index{Zini, Daniele}
\begin{chunk}{axiom.bib}
@article{Igar75,
 author = "Igarashi, Shigeru and London, Ralph L. and Luckham, David C.",
 titile = {{Automatic Program Verification I: A Logical Basis and Its
 Implementation}},
 journal = "Acta Informatica",
 volume = "4",
 number = "2",
 pages = "145182",
 year = "1975",
+@misc{Arma00,
+ author = "Armando, Alessandro and Zini, Daniele",
+ title = {{Towards Interoperable Mechanized Reasoning Systems:
+ The Logic Broker Architecture}},
+ year = "2000",
abstract =
 "Defining the semantics of programming languages by axioms and rules
 of inference yields a deduction system within which proofs may be
 given that programs satisfy specifications. The deduction system
 herein is shown to be consistent and also deduction complete with
 respect to Hoare's system. A subgoaler for the deduction system is
 described whose input is a significant subset of Pascal programs plus
 inductive assertions. The output is a set of verification conditions
 or lemmas to be proved. Several nontrivial arithmetic and sorting
 programs have been shown to satisfy specifications by using an
 interactive theorem prover to automatically generate proofs of the
 verification conditions. Additional components for a more powerful
 verification system are under construction.",
 paper = "Igar75.pdf"
+ "There is a growing interest in the integration of mechanized
+ reasoning systems such as automated theorem provers, computer algebra
+ systems, and model checkers. Stateoftheart reasoning systems are
+ the result of many manyears of careful development and engineering,
+ and usually they provide a high degree of sophistication in their
+ respective domain. Yet they often perform poorly when applied outside
+ the domain they have been designed for. The problem of integrating
+ mechanized reasoning systems is therefore being perceived as an
+ important issue in automated reasoning. In this paper we present
+ the Logic Broker Architecture, a framework which provides the needed
+ infrastructure for making mechanized reasoning systems interoperate.
+ The architecture provides location transparency, a way to forward
+ requests for logical services to appropriate reasoning systems via a
+ simple registration/subscription mechanism, and a translation
+ mechanism which ensures the transparent and provably sound exchange of
+ logical services.",
+ paper = "Arma00.pdf"
}
\end{chunk}
\index{Deutsch, L. Peter}
+\index{Lester, D.R.}
\begin{chunk}{axiom.bib}
@phdthesis{Deut73,
 author = "Deutsch, L. Peter",
 title = {{An Interactive Program Verifer}},
 institution = "University of California, Berkeley",
 year = "1973",
 paper = "Deut73.pdf"
+@inproceedings{Lest01,
+ author = "Lester, D.R.",
+ title = {{Effective Continued Fractions}},
+ booktitle = "15th IEEE Symp. on Computer Arithmetic",
+ publisher = "IEEE Computer Society Press",
+ year = "2001",
+ pages = "163170",
+ abstract =
+ "Only the leading seven terms of a continued fraction are needed to
+ perform online arithmetic, provided the continued fractions are of
+ the correct form. This forms the basis of a proof that there is an
+ effective representation of the computable reals as continued
+ fractions: we also demonstrate that the basic arithmetic operations
+ are computable using this representation.",
+ paper = "Lest01.pdf"
}
\end{chunk}
\index{King, James Cornelius}
+\index{Vuillemin, J.}
\begin{chunk}{axiom.bib}
@phdthesis{King70,
 author = "King, James Cornelius",
 title = {{A Program Verifier}},
 institution = "Carnegie Mellon University",
 year = "1970"
+@techreport{Vuil87,
+ author = "Vuillemin, J.",
+ title = {{Exact Real Computer Arithmetic with Continued Fractions}},
+ institution = "Institut National de Recherche en Informatique et en
+ Automatique",
+ year = "1987",
+ number = "760",
+ abstract =
+ "We discuss a representation of the {\sl computable real numbers} by
+ continued fractions. This deals with the subtle points of undecidable
+ and integer division, as well as representing the infinite
+ $\infty=1/0$ and undefined $\bot=0/0$ numbers. Two general algorithms
+ for performing arithmetic operations are introduced. The
+ {\sl algebraic algorithm}, which computes sums and products of
+ continued fractions as a special case, basically operates in a
+ positional manner, producing one term of output for each term of
+ input. The {\sl transcendental algorithm} uses a general formula of
+ Gauss to compute the continued fractions of exponentials, logarithms,
+ trigonometric functions, as well as a wide class of special
+ functions. This work has been implemented in Le\_Lisp and the
+ performance of these algorithms appears to be quite good; however, no
+ competing system has been available for comparison",
+ paper = "Vuil87.pdf"
}
\end{chunk}
\index{Good, Donald I.}
\index{London, Ralph L.}
\index{Bledsoe, W.W.}
+\index{Zinn, Claus}
\begin{chunk}{axiom.bib}
@article{Good75,
 author = "Good, Donald I. and London, Ralph L. and Bledsoe, W.W.",
 title = {{An Interactive Program Verification System}},
 journal = "SIGPLAN Notices",
 volume = "10",
 number = "6",
 pages = "482492",
 year = "1975",
+@phdthesis{Zinn04,
+ author = "Zinn, Claus",
+ title = {{Understanding Informal Mathematical Discourse}},
+ school = "Universitat Erlangen Nurnberg",
+ year = "2004",
abstract =
 "This paper is an initial progress report on the development of an
 interactive system for verifying that computer programs meet given
 formal specifications. The system is based on the conventional
 inductive assertion method: given a program and its specifications,
 the object is to generate the verification conditions, simplify them,
 and prove what remains. The important feature of the system is that
 the human user has the opportunity and obligation to help actively in
 the simplifying and proving. The user, for example, is the primary
 source of problem domain facts and properties needed in the proofs. A
 general description is given of the overall design philosophy,
 structure, and functional components of the system, and a simple
 sorting program is used to illustrate both the behavior of major
 system components and the type of user interaction the system provides.",
 paper = "Good75.pdf"
}

\end{chunk}

\index{Bledsoe, W.W.}
\index{Bruell, Peter}
\begin{chunk}{axiom.bib}
@article{Bled74,
 author = "Bledsoe, W.W. and Bruell, Peter",
 title = {{A ManMachine TheoremProving System}},
 journal = "Artificial Intelligence",
 volume = "5",
 number = "1",
 pages = "5172",
 year = "1974",
+ "Automated reasoning is one of the most established disciplines in
+ informatics and artificial intelligence, and formal methods become
+ increasingly employed in practical applications. However, for the most
+ part, such applications seem to be limited to informaticsspecific
+ areas (e.g., the verification of correctness properties of software
+ and hardware specifications) and areas close to informatics such as
+ computational linguistics (e.g., the computation of consistence and
+ informativeness properties of semantic representations). Naturally,
+ there is also a potential for practical applications in the the area
+ of mathematics: the generation of proofs for mathematically
+ interesting and motivated theorems and, quite associated, the
+ computersupported formalisation of (parts of elementary)
+ mathematics. It is a matter of fact, however, that mathematicians
+ rarely use computersupport for the construction and verification of
+ proofs. This is mainly caused by the “unnaturalness” of the language
+ and the reasoning that such proof engines support.
+
+ In the past, researchers in the area of automated reasoning have
+ focused their work on formalisms and algorithms that allow the
+ construction and verification of proofs that are written in a
+ formallogical language and that only use a limited number of
+ inference rules. For the computer scientist, such formal proofs have
+ the advantage of a simple and ambiguousfree syntax, which can thus be
+ easily processed. Moreover, the limited number of inference rules has
+ a direct impact on the complexity of the search space that needs to be
+ conquered during the process of constructing proofs. The verification
+ of given formal proofs is greatly facilitated by the complete
+ explicitness of their logical argumentation where no reasoning step is
+ left out. For mathematicians, however, such formal proofs are usually
+ hard to understand. For them, they are written in an unfamiliar and
+ artificial language and much too detailed. Moreover, the sheer number
+ of inference steps, while logically relevant, describe only trivial
+ mathematical details and make it difficult to follow a proof’s main
+ underlying argumentation line. In practise, thus, mathematicians use
+ proof generation engines rather seldom, if at all. The same is true
+ with regard to proof verification tools. The amount of work that is
+ required to verify a mathematical proof with such tools is
+ considerable, if not prohibitive. Since proof verification systems
+ only accept formal proofs as input, the mathematician’s first task is
+ to manually translate the mathematical proof into the formal language
+ that is accepted by the verifier. This in turn includes the
+ translation of the proof’s underlying mathematical argumentation into
+ inference rules that are supported by the proof engine. Such
+ translations and refinements are usually very time consuming, tedious,
+ and prone to error themselves. Hence, how the proof verifier then
+ judges the result of proof translation and proof refinement is only
+ of limited relevance to the original mathematical proof. From the
+ mathematician’s point of view, there is thus a need for a proof
+ verification system that is capable of processing mathematical proofs
+ automatically, at least with regard to translating the mathematicians’
+ expert language into the system’s artificial formal language. Such a
+ system would have an enormous potential in the community of
+ mathematics, and this potential has been recognised early. In the
+ beginning of the 1960s, John McCarthy, one of the pioneers of
+ artificial intelligence, remarked that ``[c]hecking mathematical proofs
+ is potentially one of the most interesting and useful applications of
+ automatic computers'' [111]. More than forty years thereafter, a tool
+ that supports mathematicians with the verification of mathematical
+ proofs is more science fiction than reality. Its realisation is
+ associated with research questions within the disciplines of automated
+ reasoning and computational linguistics that are still only partially
+ answered.
+
+ This thesis aims at contributing towards the realisation of a
+ verifier for mathematical proofs. It attempts to provide a general
+ framework as well as an implementation for such a proof
+ engine. The dissertation’s objects of study are short and simple
+ proofs that were taken from textbooks on elementary number
+ theory. Fig. 1 depicts a proof of the mathematical truth that
+ every positive integer greater than 1 can be represented as a
+ product of one or more primes. The proof consists of only a few
+ lines and little mathematical knowledge is necessary to follow the
+ proof author’s argumentation. It is this kind of short proof that
+ we attempt to check automatically.",
+ paper = "Zinn04.pdf"
+}
+
+\end{chunk}
+
+\index{Trybulec, Andrzej}
+\begin{chunk}{axiom.bib}
+@misc{Tryb02,
+ author = "Trybulec, Andrzej",
+ title = {{Towards Practical Formalizaiton of Mathematics}},
+ comment = "abstract",
+ link =
+ "\url{http://www.macs.hw.ac.uk/~fairouz/forest//events/automath2002/abstracts/Andrzej.abst.html}",
abstract =
 "This paper describes a manmachine theoremproving system at the
 University of Texas at Austin which has been used to prove a few
 theorems in general topology. The theorem (or subgoal) being proved is
 presented on the scope in its natural form so that the user can easily
 comprehend it and, by a series of interactive commands, can help with
 the proof when he desires. A feature called DETAIL is employed which
 allows the human to interact only when needed and only to the extent
 necessary for the proof.

 The program is built around a modified form of IMPLY, a
 naturaldeductionlike theorem proving technique which has been
 described earlier.",
 paper = "Bled74.pdf"
+ "In sixties the opinion that mathematics cannot be practically
+ formalized was well established. So the main achievement of de Bruijn,
+ among many others, is the decision that the problem must be reconsider
+ and probably positively solved. And I believe that 1967 will be
+ treated by future historians of mathematics as a turning point.
+
+ It is not easy to say precisely what we learnt in the meantime, if we
+ learnt anything at all. I believe that the most important results are:
+ \begin{enumerate}
+ \item we need experiments with much more advanced mathematics than
+ already done
+ \item a system for practical formalization of mathematics probably will
+ not be a simple system based on small number of primitive notions
+ \item integration with a computer algebra systems may be necessary or at
+ least a feasible system must have bigger computational power.
+ \end{enumerate}
+
+ Still we should me more concerned with the original ideas of de
+ Bruijn, the most important that eventually we have to be able to
+ formalize new mathematical results, published in mathematical
+ newspapers in this century."
}
\end{chunk}
+\index{Hayes, Patrick J.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Haye74,
+ author = "Hayes, Patrick J.",
+ title = {{Some Problems and Nonproblems in Representation Theory}},
+ booktitle = "AI and Simulation of Behaviour Conference",
+ year = "1974",
+ pages = "6379"
+}
+
+\end{chunk}
+
+\index{de Bruijn, N.G.}
+\begin{chunk}{axiom.bib}
+@incollection{Brui94a,
+ author = "de Bruijn, N.G.",
+ title = {{The Mathematical Vernacular, a Language for Mathematics
+ with Typed Sets}},
+ booktitle = "Selected Papers on Automath",
+ pages = "865935",
+ year = "1994",
+ publisher = "NorthHolland",
+ link = "\url{https://pure.tue.nl/ws/files/2073504/610209.pdf}",
+ paper = "Brui94a.pdf"
+}
+
+\end{chunk}
+
+\index{Elbers, Hugo Johannes}
+\begin{chunk}{axiom.bib}
+@phdthesis{Elbe98,
+ author = "Elbers, Hugo Johannes",
+ title = {{Connecting Informal and Formal Mathematics}},
+ year = "1998",
+ school = "Technische Universiteit Eindhoven",
+ paper = "Elbe98.pdf"
+}
+
+\end{chunk}
+
+\index{Bundy, Alan}
+\begin{chunk}{axiom.bib}
+@incollection{Bund91,
+ author = "Bundy, Alan",
+ title = {{A Science of Reasoning (Extended Abstract)}},
+ booktitle = "Computational Logic: Essays in Honor of Alan
+ Robinson",
+ year = "1991",
+ publisher = "MIT Press",
+ abstract =
+ "How can we understand reasoning in general and mathematical proofs
+ in particular? It is argued that a highlevel understanding of proofs
+ is needed to complement the lowlevel understanding provided by
+ Logic. A role for computation is proposed to provide this highlevel
+ understanding, namely by the association of proof plans with
+ proofs. Criteria are given for assessing the association of a proof
+ plan with a proof.",
+ paper = "Bund91.pdf"
+}
+
+\end{chunk}
+
+\index{Daly, Timothy}
+\index{Botch, Mark}
+\begin{chunk}{axiom.bib}
+@misc{Daly17,
+ author = "Daly, Timothy and Botch, Mark",
+ title = {{Axiom Developer Website}},
+ link = "\url{http://axiomdeveloper.org}",
+ year = "2017"
+}
+
+\end{chunk}
+
+\index{SpectorZabusky, Antal}
+\index{Breitner, Joachim}
+\index{Rizkallah, Christine}
+\index{Weirich, Stephanie}
+\begin{chunk}{axiom.bib}
+@inproceedings{Spec18,
+ author = "SpectorZabusky, Antal and Breitner, Joachim and
+ Rizkallah, Christine and Weirich, Stephanie",
+ title = {{Total Haskell is Reasonable Coq}},
+ booktitle = "ACM SIGPLAN Int. Conf. on Certified Programs and
+ Proofs",
+ publisher = "ACM",
+ year = "2018",
+ abstract =
+ "We would like to use the Coq proof assistant to mechanically
+ verify properites of Haskell programs. To that end, we present a
+ tool, named {\tt hstocoq}, that translates total Haskell
+ programs into Coq programs via a shallow embedding. We apply our
+ tool in three case studies  a lawful {\tt Monad} instance,
+ ``Hutton's razor'', and an existing data structure library  and
+ prove their correctness. These examples show that this approach is
+ viable: both that {\tt hstocoq} applies to existing Haskell
+ code, and that the output it produces is amenable to
+ verification.",
+ paper = "Spec18.pdf"
+}
+
+\end{chunk}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index d4c92ec..6e019b4 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5860,6 +5860,8 @@ books/bookvolbib add references
books/bookvolbib add references
20171127.01.tpd.patch
books/bookvolbib add references
+20171202.01.tpd.patch
+books/bookvolbib add references

1.9.1