From c161a2eb516505619cd588f1cdcfdb59df27923e Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Wed, 8 Jan 2020 01:45:32 0500
Subject: [PATCH] books/bookvolbib add references
Goal: Proving Axiom Sane
\index{Kell, Stephen}
\begin{chunk}{axiom.bib}
@inproceeding{Kell14,
author = "Kell, Stephen",
title = "In Search of Types",
booktitle = "Int. Symp. on New Ideas, New Pradigms, and Reflections
on Programming and Software (Onward!)",
publisher = "ACM",
year = "2014",
abstract =
"The concept of ``type'' has been used without a consistent,
precise definition in discussions about programming languages for
60 years. In this essay I explore various concepts lurking behind
distinct uses of this word, highlighting two traditions in which
the word came into use largely independently: engineering
traditions on the one hand, and those of symbolic logic on the
other. These traditions are founded on differing attitudes to the
nature and propose of abstraction, but their distinct uses of
``type'' have never been explicitly unified. One result is that
discourse {\sl across} these traditions often finds itself at
cross purposes, such as {\sl overapplying} one sense of ``type''
where another is appropriate, and occasionally proceeding to draw
wrong conslusions. I illustrate this with examples from wellknown
and justly wellregarded literature, and argue that ongoing
developments in both the theory and practice of programming make
now a good time to resolve these problems.",
paper = "Kell14.pdf"
}
\end{chunk}
\index{Dijkstra, Edsger W.}
\begin{chunk}{axiom.bib}
@misc{Dijk00,
author = "Dijkstra, Edsger W.",
title = {{EWD1305 Archive: Answers to questions from students of
Software Engineering}},
link = "\url{https://www.cs.utexas.edu/users/EWD/transcriptions/EWD13xx/EWD1305.html}",
year = "2000"
}
\end{chunk}
\index{Jaffe, Arthur}
\index{Quinn, Frank}
\begin{chunk}{axiom.bib}
@article{Jaff93,
author = "Jaffe, Arthur and Quinn, Frank",
title = {{``Theoretical Mathematics'': Towards a Cultural Synthesis
of Mathematics and Theoretical Physics}},
journal = "Bull. of the American Mathematical Society",
volume = "29",
number = "1",
pages = "113",
year = "1993",
abstract =
"Is specualative mathematics dangerous? Recent interactions
between physics and mathematics pose the question with some force:
traditional mathematical norms discourage speculation, but it is
the fabric of theoretical physics. In practice there can be
benefits, but there can also be unpleasant and destructive
consequences. Serious caution is required, and the issue should be
considered before, rather than after, obvious damage occurs. With
the hazards carefully in mind, we propose a framework that should
allow a healthy and positive role for speculation.",
paper = "Jaff92.pdf"
}
\end{chunk}
\begin{chunk}{axiom.bib}
@misc{Lean19,
author = "Lean",
title = {{Lean Chat Room}},
link = "\url{https://leanprover.zulipchat.com}",
year = "2019"
}
\end{chunk}
\index{Buzzard, Kevin}
\begin{chunk}{axiom.bib}
@misc{Xena19,
author = "Buzzard, Kevin",
title = {{Xena}},
link = "\url{https://xenaproject.wordpress.com}",
year = "2019"
}
\end{chunk}
\index{Hudson, Andrew Dana}
\begin{chunk}{axiom.bib}
@misc{Huds19,
author = "Hudson, Andrew Dana",
title = {{A Priest, a Rabbi, and a Robot Walk Into a Bar}},
year = "2019",
link =
"\url{https://slate.com/technology/futuretensefictionpriestrabbirobotbarandrewhudson.html},
abstract =
"A new short story looks at how artificial intelligence
could support, and distort, faith."
}
\end{chunk}
\index{Russell, Bertrand}
\begin{chunk}{axiom.bib}
@book{Russ1920,
author = "Russell, Bertrand",
title = {{Introduction to Mathematical Philosophy}},
publisher = "George Allen and Unwin, Ltd",
year = "1920"
}
\end{chunk}
\index{Bauer, Andrej}
\begin{chunk}{axiom.bib}
@misc{Baue19a,
author = "Bauer, Andrej",
title = {{Derivations as computations}},
year = "2019",
link = "\url{https://youtube.com/watch?v=YZqOVsuyQyQ}"
}
\end{chunk}
\index{Bottu, GertJan}
\index{Xie, Ningning}
\index{Mardirosian, Klara}
\index{Schrijvers, Tom}
\begin{chunk}{axiom.bib}
@misc{Bott19,
author = "Bottu, GertJan and Xie, Ningning and Mardirosian, Klara
and Schrijvers, Tom",
title = {{Coherence of Type Class Resolution}},
year = "2019",
link = "\url{http://youtube.com/watch?v=bmHd0MoCliM}",
abstract =
"Elaborationbased type class resolution, as found in languages
like Haskell, Mercury and PureScript, is generally
{\ls nondeterministic}: there can be multiple ways to satisfy a
wanted constraint in terms of global instances and locally given
constraints. Coherence is the key property that keeps this sane;
it guarantees that, despite the nondeterminism, programs will
behave predictably. even though elaborationbased resolution is
generally assumed coherent, as far as we know, there is no formal
proof of this property in the presence of sources of
nondeterminism, like suerclasses and flexible contexts.
This paper provides a formal proof to remedy the situation. The
proof is nontrivial because the semantics elaborates resolution
into a target language where different elaborations can be
distinguished by contexts that do not have a source language
counterpart. Inspired by the notion of full abstraction, we
present a twostop strategy that first elaborates
nondeterministically into an intermediate language that preserves
contextual equaivalence, and the deterministically elaborates from
there into the target language. We use an approach based on
logical relations to establish contextual equivalence and thus
coherence for the first step of elaboration, while the second
step's determinism straightforwardly preserves this coherence
property.",
paper = "Bott19.pdf"
}
\end{chunk}
\index{Lample, Guillaume}
\index{Charton, Francois}
\begin{chunk}{axiom.bib}
@misc{Lamp19,
author = "Lample, Guillaume and Charton, Francois",
title = {{Deep Learning for Symbolic Mathematics}},
year = "2019",
link = "\url{https://arxiv.org/pdf/1912.01412.pdf}",
abstract =
"Neural networks have a reputation for being better at solving
statistical or approximate problems than at performing
calculations or working with symbolic data. In this paper, we show
that they can be surprisingly good at more elaborated tasks in
mathematics, such as symbolic integration and solving differential
equations. We propose a syntax for representing mathematical
problems, and methods for generating large datasets that can be
used to train sequencetosequence models. We achieve results that
outperform commercial Computer Algebra Systems such as Matlab or
Mathematica.",
paper = "Lamp19.pdf"
}
\end{chunk}
\index{Loh, PoShen}
\begin{chunk}{axiom.bib}
@misc{Lohx19,
author = "Loh, PoShen",
title = {{A Simple Proof of the Quadratic Formula}},
year = "2019",
link = "\url{https://arxiv.org/pdf/1910.06709.pdf}",
abstract =
"This aarticle provides a simple proof of the quadratic formula,
which also produces an efficient and natural method for solving
general quadratic equations. The derivation is computationally
light and conceptually natural, and has the potential to demystify
quadratic equations for students worldwide.",
paper = "Lohx19.pdf"
}
\end{chunk}
\index{Kay, Alan}
\begin{chunk}{axiom.bib}
@misc{Kayx19,
author = "Kay, Alan",
title = {{Alan Kay Speaks at ATLAS Institute}},
year = "2019",
link = "\url{https://www.youtube.com/watch?v=nOrdzDaPYV4}"
}
\end{chunk}
\index{Bauer, Andrej}
\index{Stone, Christopher A.}
\begin{chunk}{axiom.bib}
@misc{Baue07,
author = "Bauer, Andrej and Stone, Christopher A.",
title = {{RZ: a Tool for Bringing Constructive and Computational
Mathematics Closer to Programming Practice}},
year = "2007",
link = "\url{http://math.andrej.com/wpcontent/uploads/2007/cielong.pdf}",
abstract =
"Realizability theory is not only a fundamental tool in logic and
computability, but also has direct application to the design and
implementation of programs: it can produce interfaces for the data
structure corresponding to a mathematical theory. Our tool, called
RS, serves as a bridge between the worlds of constructive
mathematics and programming. By using the realizability
interpretation of constructive mathematics, RZ translates
specifications in constructive logic into annotated interface code
in Objective Caml. The system supports a rich input language
allowing descriptions of complex mathematical structures. RZ does
not extract code from proofs, but allows any implementation
method, from handwritten code to code extracted from proofs by
other tools.",
paper = "Baue07.pdf",
keywords = "printed"
}
\end{chunk}
\index{Awodey, Steve}
\index{Bauer, Andrej}
\begin{chunk}{axiom.bib}
@misc{Awod04,
author = "Awodey, Steve and Bauer, Andrej",
title = {{Propositions as [Types]}},
year = "2004",
link = "\url{http://math.andrej.com/asset/data/bracket_types.pdf}",
abstract =
"Image factorizations in regular categories are stable under
pullbacks, as they model a natural modal operator in dependent
type theory. This unary type constructor [A] has turned up
previously in a syntactic form as a way of erasing computational
content, and formalizing a notion of proof irrelevance. Indeed,
semantically, the notion of a {\sl support} is sometimes used as
surrogate proposition asserting inhabitation of an indexed family.
We give rules for bracket types in dependent type theory and
provide complete semantics using regular categories. We show that
dependent type theory with the unit type, strong extensional
equality types, strong dependent sums, and bracket types is the
internal type theory of regular categories, in the same way that
the usual dependent type theory with dependent sums and products
is the internal type theory of locally cartesian closed
categories.
We also show how to interpret firstorder logic in type theory
with brackets, and we make use of the translation to compare type
theory with logic. Specifically, we show that the
propositionsastypes interpretation is complete with respect to a
certain fragment of intuitionistic firstorder logic, in the sense
that a formula from the fragment is derivable in intuitionistic
firstorder logic if, and only if, its interpretation in dependent
type theory is inhabited. As a consequence, a modified
doublenegation translation into type theory (without bracket
types) is complete, in the same sense, for all of classical
firstorder logic.",
paper = "Awod04.pdf",
keywords = "printed"
}
\end{chunk}
\index{Hoare, C.A.R}
\index{Shepherdson, J.C.}
\begin{chunk}{axiom.bib}
@book{Hoar85,
author = "Hoare, C.A.R and Shepherdson, J.C.",
title = {{Mathematical Logic and Programming Languages}},
year = "1985",
publisher = "PrenticeHall",
isbn = "0135614651"
}
\end{chunk}
\index{Luckham, D.C.}
\index{Park, D.M.R}
\index{Paterson, M.S.}
\begin{chunk}{axiom.bib}
@article{Luck70,
author = "Luckham, D.C. and Park, D.M.R and Paterson, M.S.",
title = {{On Formalised Computer Programs}},
journal = "J. of Computer and System Sciences",
volume = "4",
pages = "220249",
year = "1970",
paper = "Luck70.pdf"
}
\end{chunk}
\index{Manna, Zohar}
\begin{chunk}{axiom.bib}
@phdthesis{Mann68,
author = "Manna, Zohar",
title = {{Termination of Algorithms}},
school = "Carnegie Mellon University",
year = "1968",
link = "\url{http://apps/dtic.mil/dtic/tr/fulltext/u2/670558.pdf}",
abstract =
"The thesis contains two parts which are selfcontained units.
In Part I we present several results on the relation between
\begin{enumerate}
\item the problem of termination and equivalence of programs and
abstract programs, and
\item the first order predicate calculus
\end{enumerate}
Part II is concerned with the relation between
\begin{enumerate}
\item the termination of interpreted graphs, and
\item properties of wellordered sets and graph theory
\end{enumerate}",
paper = "Mann68.pdf"
}
\end{chunk}
\index{McCarthy, J.}
\begin{chunk}{axiom.bib}
@misc{Mcca60a,
author = "McCarthy, J.",
title = {{Programs with Common Sense}},
year = "1960",
abstract =
"Interesting work is being done in programming computers to solve
problems which require a high degree of intelligence in
humans. However, certain elementary verbal reasoning processes so
simple that they can be carried out by any nonfeebleminded human
have yet to be simulated by machine programs.
This paper will discuss programs to manipulate in a suitable
formal language (most likely a part of the predicate calculus)
common instrumental statements. The basic program will draw
immediate conclusions from a list of premises. These conclusions
will be either declarative or imperative sentences. When an
imperative sentence is deduced the program takes a corresponding
action. These actions may include printing sentences, moving
sentences on lists, and reinitiating the basic deduction process
on these lists.
Facilities will be provided for communication with humans in the
system via manual intervention and display devices connected to
the computer.",
paper = "Mcca60a.pdf"
}
\end{chunk}
\index{van Benthem Jutting, L.S.}
\index{McKinna, J.}
\index{Pollack, R.}
\begin{chunk}{axiom.bib}
@inproceedings{Bent93,
author = "van Benthem Jutting, L.S. and McKinna, J. and Pollack, R.",
title = {{Checking Algorithms for Pure Type Systems}},
booktitle = "Types for Proofs and Programs",
publisher = "Springer",
year = "1993",
pages = "1961",
abstract =
"This work is motivated by the problem of finding reasonable
algorithms for typechecking Pure Type Systems [Bar91] (PTS). There
are several implementations of formal systems that are either PTS
or closely related to PTS. For example, LEGO [LP92] implements the
Pure Calculus of Constructions (PCC) [CH88], the Extended Calculus
of Constructions [Luo90] and the Edinburgh Logical Framework (LF)
[HHP87]. ELF [Pfe89] implements LF; CONSTRUCTOR [Hel91] implements
arbitrary PTS with finite set of sorts. Are these implementations
actually correct? Of course, we may enumerate all derivations of a
given PTS, and Jutting [vBJ93] has shown that a large class of
normalizing PTS have decidable typechecking by computing the
normal forms of types, but such techniques are obviously not
usable in practice. Algorithms in the literature for particular
type systems, such as Huet's Constructive Engine [Hue89], do not
obviously extend even to such tame classes as the normalizing and
functional PTS.",
paper = "Bent93.pdf"
}
\end{chunk}
\index{Ranta, Aarne}
\begin{chunk}{axiom.bib}
@inproceedings{Rant93,
author = "Ranta, Aarne",
title = {{Type Theory and the Informal Language of Mathematics}},
booktitle = "Types for Proofs and Programs",
publisher = "Springer",
year = "1993",
pages = "352365",
paper = "Rant93.pdf"
}
\end{chunk}
\index{Parent, C.}
\begin{chunk}{axiom.bib}
@inproceedings{Pare93,
author = "Parent, C.",
title = {{Developing Certified Programs in the System Coq the
Program Tactic}},
booktitle = "Types for Proofs and Programs",
publisher = "Springer",
year = "1993",
pages = "291312",
abstract =
"The system Coq is an environment for proof development based on
the Calculus of Contructions extended by inductive
definitions. The specification of a program can be represented by
a logical formula and the program itself can be extracted from the
constructive proof of the specification. In this paper, we look at
the possibility of inverting the extraction process. More
precisely, we present a method which, given a specification and a
program, builds the logical conditions to be verified in order to
obtain a correctness proof of the program. We build a proof of the
specification from the program from which the program can be
extracted. Since some information cannot automatically be
inferred, we show how to annotate the program by specifiying some
of its parts in order to guide the search for the proof.",
paper = "Pare93.pdf",
keywords = "printed"
}
\end{chunk}
\index{Gordon, M.J.C}
\begin{chunk}{axiom.bib}
@article{Gord15,
author = "Gordon, M.J.C",
title = {{Tactics for Mechanized Reasoning: A Commentary on Milner
(1984) 'The Use of Machines to Assist in Rigorous Proof'}},
journal = "Philosophical Transactions: Mathematical, Physical and
Engineering Sciences",
volume = "373",
number = "2039",
pages = "111",
year = "2015",
abstract =
"Robin Milner's paper, ``The use of machines to assist in rigorous
proof'', introduces methods for automating mathematical reasoning
that are a milestone in the development of computerassisted
theorem proving. His ideas, particularly his theory of tactics,
revolutionized the architecture of proof assistants. His
methodology for automating rigorous proof soundly, particularly
his theory of type polymorphism in programming, led to major
contributions to the theory and design of programming
languages. His citation for the 1991 ACM A.M. Turing award, the
most prestigious award in computer science, credits him with,
among other achievements, 'probably the first theoretically based
yet practical tool for machine assisted proof construction'. This
commentary was written to celebrate the 350th anniversary of the
journal {\sl Philosophical Transactions of the Royal Society}."
paper = "Gord15.pdf",
keywords = "printed"
}
\end{chunk}
\index{Knuth, Donald E.}
\begin{chunk}{axiom.bib}
@misc{Knut19,
author = "Knuth, Donald E.",
title = {{Donald Knuth: Algorithms, Complexity, Life, and The Art of
Computer Programmig}},
link = "\url{https://www.youtube.com/watch?v=2Bd8fsXbST8}",
year = "2019",
comment = "Lex Fridman AI Podcast"
}
\end{chunk}
\index{Scott, Dana}
\index{Strachey, Christopher}
@misc{Scot92,
author = "Scott, Dana and Strachey, Christopher",
title = {{Toward a Mathematical Semantics for Computer Languages}},
year = "1992",
comment = "Oxford Programming Research Group Monograph PRG6"
abstract =
"Compilers for highlevel languages are generally constructed to
give the complete translation of the programs into machine
language. As machines merely juggle bit patterns, the concepts of
the original language may be lost or at least obscured during this
passage. The purpose of a mathematical semantics is to give a
correct and meaningful correspondence between programs and
mathematical entities in a way that is entirely independent of an
implementation. This plan is illustrated in a very elementary way
in the introduction. The first section connects the general method
with the usual idea of state transformations. The next section
shows why the mathematics of functions has to be modified to
accommodate recursive commands. Section 3 explains the
modification. Section 4 introduces the environments for handling
variables and identifiers and shows how the semantical equations
define equivalence of programs. Section 5 gives an exposition of
the new type of mathematical function spaces that are required for
the semantics of procedures when these are allowed in
assignments. The conclusion traces some of the background of the
project and points the way to future work.",
paper = "Scot92.pdf"
}
\end{chunk}
\index{Milner, Robin}
\begin{chunk}{axiom.bib}
@article{Miln72a,
author = "Milner, Robin",
title = {{Implementation and Applications of Scott's Logic for
Computable Functions}},
journal = "ACM SIGPLAN Notices",
volume = "7",
number = "1",
year = "1972",
pages = "16",
abstract =
"The basis for this paper is a logic designed by Dana Scott[1] in
1969 for formalizing arguments about computable functions of
higher type. This logic uses typed combinators, and we give a more
or less direct translation into typed $\lambda$calculus, which is
an easier formalism to use, though not so easy for the metatheory
because of the presence of bound variables. We then describe, by
example only, a proofchecker program which has been implemented
for this logic; the program is fully describe in [2]. We relate
the induction rule which is central to the logic to two more
familiar rules  Recursion Induction and Structural Induction 
showing that the former is a theorem of the logic, and that for
recursively defined structures the latter is a derived rule of the
logic. Finally we show how the syntax and semantics of a simple
programming language may be described completely in the logic, and
we give an example of a theorem which relates syntactic and
semantic properties of programs and which can be stated and proved
within the logic."
}
\end{chunk}
\index{Avigad, Jeremy}
\index{Harrison, John}
\begin{chunk}{axiom.bib}
@article{Avig14b,
author = "Avigad, Jeremy and Harrison, John",
title = {{Formally Verified Mathematics}},
journal = "Communications of the ACM",
volume = "57",
number = "4",
pages = "6675",
year = "2014",
abstract =
"With the help of computational proof assistants, formal
verification could beome the new standard for rigor in
mathematics.",
paper = "Avig14b.pdf"
}
\end{chunk}
\index{Landin, P.J.}
\begin{chunk}{axiom.bib}
@article{Land66,
author = "Landin, P.J.",
title = {{The Next 700 Programming Languages}},
journal = "Communications of the ACM",
volume = "9",
pages = "157166",
year = "1966",
abstract =
"A family of unimplemented computing languages is described that
is intended to span differences of application areas by a unified
framework. This framework dictates the rules about the uses of
usercoined names, and the conventions about characterizing
functional relationships. Within this framework the design of a
specific language splits into two independent parts. One is the
choice of written appearances of programs (or more generally,
their physical representation). The other is the choice of the
abstract entities (such as numbers, characterstrings, lists of
them, functional relations among them) that can be referred to in
the language.
The system is biased towards ``expressions'' rather than
``statements''. It includes a nonprocedural (purely functional)
subsystem that aims to expand the class of users' needs that can
be met by a single printinstruction, without sacrificing the
important properties that make conventional righthandside
expressions easy to construct and understand.",
paper = "Land66.pdf"
}
\end{chunk}
\index{Keenen, David C.}
\begin{chunk}{axiom.bib}
@misc{Keen14,
author = "Keenen, David C.",
title = {{To Dissect a Mockingbird: A Graphical Notation for the
Lambda Calculus with Animated Reduction}},
year = "2014",
link = "\url{http://dkeenan.com/Lambda}",
abstract =
"The lambda calculus, and the closely related theory of
combinators, are important in the foundations of mathematics,
logic and computer science. This paper provides an informal and
entertaining introduction by means of an animated graphical
notation.",
keywords = "printed, DONE"
}
\end{chunk}
\index{Friedman, Daniel P.}
\index{Eastland, Carl}
\begin{chunk}{axiom.bib}
@book{Frie15,
author = "Friedman, Daniel P. and Eastland, Carl",
title = {{The Little Prover}},
publisher = "The MIT Press",
year = "2015",
isbn = "9780262527958",
keywords = "shelf"
}
\end{chunk}
\index{Donald, B.R.}
\index{Kapur, D.}
\index{Mundy, J.L.}
\begin{chunk}{axiom.bib}
@book{Dona92,
author = "Donald, B.R. and Kapur, D. and Mundy, J.L.",
title = {{Symbolic and Numerical Computation for Artificial
Intelligence}},
publisher = "Academic Press Limited",
year = "1992",
isbn = "0 12 220535 9",
keywords = "shelf"
}
\end{chunk}
\index{Friedman, Daniel P.}
\index{Christiansen, David Thrane}
\begin{chunk}{axiom.bib}
@book{Frie18,
author = "Friedman, Daniel P. and Christiansen, David Thrane",
title = {{The Little Typer}},
publisher = "The MIT Press",
year = "2018",
isbn = "9780262536431",
keywords = "shelf"
}
\end{chunk}
\index{Daepp, Ulrich}
\index{Gorkin, Pamela}
\begin{chunk}{axiom.bib}
@book{Daep11,
author = "Daepp, Ulrich and Gorkin, Pamela",
title = {{Reading, Writing, and Proving}},
year = "2011",
publisher = "Springer",
isbn = "9781441994783",
keywords = "shelf"
}
\end{chunk}
\index{Girard, JeanYves}
\index{Lafont, Yves}
\index{Regnier, Laurent}
\begin{chunk}{axiom.bib}
@book{Gira95a,
author = "Girard, JeanYves and Lafont, Yves and Regnier, Laurent",
title = {{Advances in Linear Logic}},
publisher = "Cambridge University Press",
year = "1995",
isbn = "0521559618",
keywords = "shelf"
}
\end{chunk}
\index{Barrett, William A.}
\index{Couch, John D.}
\begin{chunk}{axiom.bib}
@book{Barr79,
author = "Barrett, William A. and Couch, John D.",
title = {{Compiler Construction: Theory and Practice}},
publisher = "Science Research Associates",
year = "1979",
isbn = "057421335X",
keywords = "shelf"
}
\end{chunk}
\index{Weitz, Edmund}
\begin{chunk}{axiom.bib}
@book{Weit16,
author = "Weitz, Edmund",
title = {{Common Lisp Recipes}},
publisher = "Apress",
year = "2016",
isbn = "9781484211779",
keywords = "shelf"
}
\end{chunk}
\index{Feynman, Richard}
\index{Hey, Anthony J.G.}
\begin{chunk}{axiom.bib}
@book{Feyn02,
author = "Feynman, Richard and Hey, Anthony J.G.",
title = {{Feynman and Computation}},
publisher = "Westview Press",
year = "2002",
isbn = "081334039X",
keywords = "shelf"
}
\end{chunk}
\index{Carter, Nathan}
\begin{chunk}{axiom.bib}
@book{Cart09,
author = "Carter, Nathan",
title = {{Visual Group Theory}},
publisher = "Mathematical Association of America",
year = "2009",
isbn = "9780883857571",
keywords = "shelf"
}
\end{chunk}
\index{Goguen, Joseph A.}
\index{Malolm, Grant}
\begin{chunk}{axiom.bib}
@book{Gogu96,
author = "Goguen, Joseph A. and Malolm, Grant",
title = {{Algebraic Semantics of Imperative Programs}},
publisher = "MIT Press",
year = "1996",
isbn = "026207172X",
keywords = "shelf"
}
\end{chunk}
\index{Tanimoto, Steven L.}
\begin{chunk}{axiom.bib}
@book{Tani95,
author = "Tanimoto, Steven L.",
title = {{The Elements of Artificial Intelligence Using Common
Lisp}},
publisher = "Computer Science Press",
year = "1995",
isbn = "0716782693",
keywords = "shelf"
}
\end{chunk}
\index{Petzold, Charles}
\begin{chunk}{axiom.bib}
@book{Petz08,
author = "Petzold, Charles",
title = {{The Annotated Turing}},
publisher = "Wiley",
year = "2008",
isbn = "9780470229057".
keywords = "shelf"
}
\end{chunk}
\index{Wiener, Norbert}
\begin{chunk}{axiom.bib}
@book{Wien61,
author = "Wiener, Norbert",
title = {{Cybernetics}},
publisher = "MIT Press",
year = "1961",
keywords = "shelf"
}
\end{chunk}
\index{Monin, JeanFrancois}
\begin{chunk}{axiom.bib}
@book{Moni03,
author = "Monin, JeanFrancois",
title = {{Understanding Formal Methods}},
publisher = "Springer",
year = "2003",
isbn = "1852332476",
keywords = "shelf"
}
\end{chunk}
\index{Wilf, William}
\index{Johnsson, Richard K.}
\index{Weinstock, Charles B.}
\index{Hobbs, Steven O.}
\index{Geschke, Charles M.}
\begin{chunk}{axiom.bib}
@book{Wilf75,
author = "Wilf, William and Johnsson, Richard K. and
Weinstock, Charles B. and Hobbs, Steven O.
and Geschke, Charles M.",
title = {{The Design of an Optimizing Compiler}},
publisher = "Elsevier",
year = "1975",
isbn = "0444001581",
keywords = "shelf"
}
\end{chunk}
\index{Goldstein, Rebecca}
\begin{chunk}{axiom.bib}
@book{Gold05,
author = "Goldstein, Rebecca",
title = {{Incompleteness}},
publisher = "Atlas Books",
year = "2005",
isbn = "0393327604",
keywords = "shelf"
}
\end{chunk}
\index{Queinnec, Christian}
\begin{chunk}{axiom.bib}
@book{Quei94,
author = "Queinnec, Christian",
title = {{Lisp In Small Pieces}},
publisher = "Cambridge University Press",
year = "1994",
isbn = "0521545668",
keywords = "shelf"
}
\end{chunk}
\index{Kalorkoti, K.}
\begin{chunk}{axiom.bib}
@misc{Kalo18,
author = "Kalorkoti, K.",
title = {{Introduction to Computer Algebra}},
comment = "Course Notes",
year = "2018",
keywords = "shelf"
}
\end{chunk}
\index{Friedman, Daniel P.}
\index{Byrd, William E.}
\index{Kiselyov, Oleg}
\begin{chunk}{axiom.bib}
@book{Frie05,
author = "Friedman, Daniel P. and Byrd, William E. and
Kiselyov, Oleg",
title = {{The Reasoned Schemer}},
publisher = "MIT Press",
year = "2005",
isbn = "0262562146",
keywords = "shelf"
}
\end{chunk}
\index{Friedman, Daniel P.}
\index{Felleisen, Matthias}
\begin{chunk}{axiom.bib}
@book{Frie96,
author = "Friedman, Daniel P. and Felleisen, Matthias",
title = {{The Seasoned Schemer}},
publisher = "MIT Press",
year = "1996",
isbn = "026256100X",
keywords = "shelf"
}
\end{chunk}
\index{Friedman, Daniel P.}
\index{Felleisen, Matthias}
\begin{chunk}{axiom.bib}
@book{Frie99,
author = "Friedman, Daniel P. and Felleisen, Matthias",
title = {{The Little Schemer}},
publisher = "MIT Press",
year = "1999",
isbn = "0262560992",
keywords = "shelf"
}
\end{chunk}
\index{Brady, Edwin}
\begin{chunk}{axiom.bib}
@book{Brad17a,
author = "Brady, Edwin",
title = {{TypeDriven Development with IDRIS}},
publisher = "Manning Publications",
year = "2017",
isbn = "9781617293023",
keywords = "shelf"
}
\end{chunk}
\index{Bundy, Alan}
\index{Basin, David}
\index{Hutter, Dieter}
\index{Ireland, Andrew}
\begin{chunk}{axiom.bib}
@book{Bund05,
author = "Bundy, Alan and Basin, David and Hutter, Dieter and
Ireland, Andrew",
title = {{Rippling: MetaLevel Guidance for Mathematical
Reasoning}},
publisher = "Cambridge University Press",
year = "2005",
isbn = "9780521834490",
keywords = "shelf"
}
\end{chunk}
\index{Nagel, Ernest}
\index{Newman, James R.}
\begin{chunk}{axiom.bib}
@book{Nage01,
author = "Nagel, Ernest and Newman, James R.",
title = {{Godel's Proof}},
publisher = "New York University Press",
year = "2001",
isbn = "0814758169",
keywords = "shelf"
}
\end{chunk}
\index{Sozeau, Matthieu}
\index{Boulier, Simon}
\index{Forster, Yannick}
\index{Tabareau, Nicolas}
\index{Winterhalter, Theo}
\begin{chunk}{axiom.bib}
@misc{Soze19,
author = "Sozeau, Matthieu and Boulier, Simon and Forster, Yannick
and Tabareau, Nicolas and Winterhalter, Theo",
title = {{Coq Coq Correct!}},
year = "2019",
link = "\url{https://www.irif.fr/~sozeau/research/publications/drafts/Coq_Coq_Correct.pdf}",
abstract =
"Coq is built around a welldelimited kernel that performs
typechecking for definitions in a variant of the Calculus of
Inductive Constructions (CIC). Although the metatheory of CIC is
very stable and reliable, the correctness of its implementation in
Coq is less clear. Indeed, implementing an efficient type checker
for CIC is a rather complex task, and many parts of the code rely
on implicit invariants which can easily be broken by further
evolution of the code. Therefore, on average, one critical bug has
been found every year in Coq. This paper presents the first
implementation of a type checker for the kernel of Coq, which is
proven correct in Coq with respect to its formal
specification. Note that because of Godel's incompleteness
theorem, there is no hope to prove completely the correctness of
the specification of Coq inside Coq (in particular strong
normalisation or canonicity), but it is possible to prove the
correctness of the implementation assuming the correctness of the
specification. Our work is based on the METACOQ project [Anand et
al. 2018; Sozeau et al. 2019] which provides metaprogramming
facilities to work with terms and declarations at the level of
this kernel. Our type checker is based on the specification of the
typing relation of the Polymorphic Cumulative Calculus of
Inductive Constructions (PCUIC) at the basis of Coq and the
verification of a relatively efficient and sound typechecker for
it. In addition to the kernel implementation, an essential feature
of Coq is socalled {\sl extraction} [Lebouzey 2004]; the
production of executable code in functional languages from Coq
definitions. We present a verified version of this subtle
typeandproof erasure step, therefore enabling the verified
extraction of a safe typechecker for Coq.",
paper = "Soze19.pdf",
keywords = "printed"
}
\end{chunk}
\index{Crouse, Maxwell}
\index{Whitehead, Spencer}
\index{Abdelaziz, Ibrahim}
\index{Makni, Bassem}
\index{Cornelio, Cristina}
\index{Kapanipathi, Pavan}
\index{Pell, Edwin}
\index{Srinivas, Kavitha}
\index{Thost, Veronika}
\index{Witbrock, Michael}
\index{Fokoue, Achille}
\begin{chunk}{axiom.bib}
@misc{Crou19,
author = "Crouse, Maxwell and Whitehead, Spencer and
Abdelaziz, Ibrahim and Makni, Bassem and
Cornelio, Cristina and Kapanipathi, Pavan and
Pell, Edwin and Srinivas, Kavitha and
Thost, Veronika and Witbrock, Michael and
Fokoue, Achille",
title = {{A Deep Reinforcement Learning Base Approach to Learning
Transferable Proof Guidance Strategies}},
year = "2019",
linke = "\url{https://arxiv.org/pdf/1911.02065.pdf}",
abstract =
"Traditional firstorder logic (FOL) reasoning systems usually
rely on manual heuristics for proof guidance. We propose TRAIL: a
system that learns to perform proof guidance using reinforcement
learning. A key design principle of our system is that it is
general enough to allow transfer to problems in different domains
that do not share the same vocabulary of the training set. To do
so, we developed a novel representation of the internal state of a
prover in terms of clauses and inference actions, and a novel
neuralbased attention mechanism to learn interactions between
clauses. We demonstrate that this approach enables the system to
generalize from training to test data across domains with
different vocabularies, suggesting that the nerual architecture in
TRAIL is well suited for representing and processing of logical
formalisms.",
paper = "Crou19.pdf"
}
\end{chunk}
\index{Crouse, Maxwell}
\index{Abdelaziz, Ibrahim}
\index{Cornelio, Cristina}
\index{Thost, Veronika}
\index{Wu, Lingfei}
\index{Forbus, Kenneth}
\index{Fokoue, Achille}
\begin{chunk}{axiom.bib}
@misc{Crou19a,
author = "Crouse, Maxwell and Abdelaziz, Ibrahim and
Cornelio, Cristina and Thost, Veronika and
Wu, Lingfei and Forbus, Kenneth and Fokoue, Achille",
title = {{Improving Graph Neural Network Representations of Logical
Formulae with Subgraph Pooling}},
year = "2019",
linke = "\url{https://arxiv.org/pdf/1911.06904.pdf}",
abstract =
"Recent advances in the integration of deep learning with
automated theorem proving have centered around the representation
of graphstructured representations, in large part driven by the
rapidly emerging body of research in geometric deep
learning. Typically, structureaware neural methods for embedding
logical formulae have been variants of either Tree LSTMs or
GNNs. While more effective than character and tokenlevel
approaches, such methods have often made representational
tradeoffs that limited their ability to effectively represent the
global structure of their inputs. In this work, we introduce a
novel approach for embedding logical formulae using DAG LSTMs that
is designed to overome the limitations of both Tree LSTMs and
GNNs. The effectiveness of the proposed framework is demonstrated
on the tasks of premise selection and proof step classification
where it achieves the stateoftheart performance on two standard
datasets.",
paper = "Crou19a.pdf"
}
\end{chunk}
\index{Gauthier, Thibault}
\begin{chunk}{axiom.bib}
@misc{Gaut19,
author = "Gauthier, Thibault",
title = {{Deep Reinforcement Learning in HOL4}},
year = "2019",
link = "\url{https://arxiv.org/pdf/1910.11797.pdf}",
abstract =
"The paper describes an implementation of deep reinforcement
learning through selfsupervised learning within the proof
assistant HOL4. A close interaction between the machine learning
modules and the HOL4 library is achieved by the choice of tree
neural networks (TNNs) as machine learning models and the internal
use of HOL4 terms to represent tree structures of TNNs. Recursive
improvement is possible when a given task is expressed as a search
problem. In this case, a Monte Carlo Tree Search (MCTS) algorithm
guided by a TNN can be used to explore the search space and
produce better examples for training the next TNN. As an
illustration, tasks over propositional and arithmetical terms,
representative of fundamental theorem proving techniques, are
specified and learned: truth estimation, endtoend computation,
term rewriting and term synthesis.",
paper = "Gaut19.pdf"
}
\end{chunk}
\index{Piotrowski, Bartosz}
\index{Brown, Chad E.}
\index{Kaliszyk, Cezary}
\begin{chunk}{axiom.bib}
@misc{Piot19,
author = "Piotrowski, Bartosz and Brown, Chad E. and
Kaliszyk, Cezary",
title = {{Can Neural Networks Learn Symbolic Rewriting?}},
year = "2019",
link = "\url{https://arxiv.org/pdf/1911.04783.pdf}",
abstract =
"This work investigates if the current neural architectures are
adequate for learning symbolic rewriting. Two kinds of data sets
are proposed for this research  one based on automated proofs
and the other being a synthetic set of polynomial terms. The
experiments with use of the current neural machine translation
models are performed and its results are discussed. Ideas for
extending this line of research are proposed and its relevance is
motivated.",
paper = "Piot19.pdf"
}
\end{chunk}
\index{Brown, Chad E.}
\index{Gauthier, Thibault}
\begin{chunk}{axiom.bib}
@misc{Brow19,
author = "Brown, Chad E. and Gauthier, Thibault",
title = {{SelfLearned Formula Synthesis in Set Theory}},
year = "2019",
link = "\url{https://arxiv.org/pdf/1912.01525.pdf}",
abstract =
"A reinforcement learning algorithm accomplishes the task of
synthesizing a settheoretical formula that evaluates to a given
truth value for given assignments.",
paper = "Brow19.pdf"
}
\end{chunk}
\index{Olsak, Miroslav}
\index{Kaliszyk, Cezary}
\index{Urban, Josef}
\begin{chunk}{axiom.bib}
@misc{Olsa19,
author = "Olsak, Miroslav and Kaliszyk, Cezary and Urban, Josef",
title = {{Property Invariant Embedding for Automated Reasoning}},
year = "2019",
link = "\url{https://arxiv.org/pdf/1911.12073.pdf}",
abstract =
"Automated reasoning and theorem proving have recently become
major challenges for machine learning. In other domains,
representations that are able to abstract over unimportant
transformations, such as abstraction over translations and
rotations in vision, are becoming more common. Standard methods of
embedding mathematical formulas for learning theorem proving are
however yet unable to handle many important transformations. In
particular, embedding previously unseen labels, that often arise
in definitional encodings and in Skolemizatin, has been very weak
so far. Similar problems appear when tranferring knowledge between
known symbols.
We propose a novel encoding of formulas that extends existing
graph neural network models. This encoding represents symbols only
by nodes in the graph, without giving the network any knowledge of
the original labels. We provide additional links between such
nodes that allow the network to recover the meaning and therefore
correctly embed such nodes irrespective of the given labels. We
test the proposed encoding in an automated theorem prover based on
the tableaux connection calculus, and show that it improves on the
best characterizations used so far. The encoding is further
evaluated on the premise selection task and a newly introduced
symbol guessing task, and shown to correctly predict 65\% of the
symbol names.",
paper = "Olsa19.pdf"
}
\end{chunk}
\index{Wang, Qingxiang}
\index{Brown, Chad}
\index{Kaliszyk, Cezary}
\index{Urban, Josef}
\begin{chunk}{axiom.bib}
@misc{Wang19a,
author = "Wang, Qingxiang and Brown, Chad and Kaliszyk, Cezary and
Urban, Josef",
title = {{Exploration of Neural Machine Translation in
Autoformalization of Mathematics in Mizar}},
year = "2019",
link = "\url{https://arxiv.org/pdf/1912.02636.pdf}",
abstract =
"In this paper we share several experiments trying to
automatically translate informal mathematics into formal
mathematics. In our context informal mathematics refers to
humanwritten mathematical sentences in the LaTeX format; and
formal mathematics refers to statements in the Mizar language. We
conducted our experiments against three established neural
networkbased machine translation models that are know to deliver
competitive results on translating between natural languages. To
train these models we also prepared four informaltoformal
datasets. We compare and analyze our results according to whether
the model is supervised or unsupervised. In order to augment the
data available for autoformalization and improve the results, we
develop a custom typeelaboration mechanism and integrate it into
the supervised translation.",
paper = "Wang19a.pdf"
}
\end{chunk}

books/bookvol13.pamphlet  12 +
books/bookvol15.pamphlet  939 +++++++++++++++++++++++++++
books/bookvolbib.pamphlet  1206 ++++++++++++++++++++++++++++++++++++++
changelog  4 +
src/axiomwebsite/patches.html  2 +
5 files changed, 2014 insertions(+), 149 deletions()
diff git a/books/bookvol13.pamphlet b/books/bookvol13.pamphlet
index 64f9ada..84f52d8 100644
 a/books/bookvol13.pamphlet
+++ b/books/bookvol13.pamphlet
@@ 5292,6 +5292,18 @@ efficient checking is possible.
presented.",
+\subsection{Hoare \cite{Hoar85}}
+
+The Euclidean algorithm defines the greatest common divisor, and we
+write
+\[\begin{array}{rcl}
+gcd(m,n)& = &\\
+&&(m>n \rightarrow gcd(n,m)\\
+&&rem(n/m)=0 \rightarrow m\\
+&&T \rightarrow gcd(rem(n/m),m))
+\end{array}
+\]
+
\subsection{Hoare \cite{Hoar87}}
Let us suppose first that they agree to confine attention to positive
diff git a/books/bookvol15.pamphlet b/books/bookvol15.pamphlet
index 7171b65..dc049df 100755
 a/books/bookvol15.pamphlet
+++ b/books/bookvol15.pamphlet
@@ 483,10 +483,18 @@ November 10, 2003 ((iHy))
%\chapter{Reference}
%\chapter{Architecture}
+%the general problem
+%the specific problem
+%what you did (contributions, what research is about)
+%take home ideas
+
% NOTE REWRITE LOOPS INTO FUNCTIONS
\chapter{Motivation}
+In the logical traditional fallacy of ``appeal to authority'' I
+present quotes from the literature.
+
\begin{quote}
{\bf Let us change our traditional attitude to the construction of
programs. Instead of imagining that our main task is to instruct a
@@ 497,9 +505,165 @@ human beings what we want a computer to do.}\\
This literate program contains the actual source code for the new Sane
version of Axiom. One of the key goals is to support understanding and
longterm maintenance of this new version of Axiom.Key ideas as well
+longterm maintenance of this new version of Axiom. Key ideas as well
as their implementation in code details are discussed.
+Computational Mathematics has had two distinct branches, the computer
+algebra branch and the mathematical logic branch. There has been
+little crossover between these two fields. Ideally we would have a
+system where both were combined into a single system.
+
+\begin{quote}
+{\bf It is reasonable to hope that the relationship between
+computation and mathematical logic will be as fruitful in the next
+century as that between analysis and physics in the last. The
+development of this relationship demands a concern for both
+applications and for mathematical elegance.}\\
+ John McCarthy \cite{Mcca63}
+\end{quote}
+
+Axiom has developed in the Computer Algebra branch and, until now, has
+ignored the mathematical logic branch. The time has come to converge
+these branches.
+
+This project has the goal of proving Axiom Sane (aka rational,
+coherent, judicious, and sound). To do that we enhance Axiom with the
+necessary logic structures (e.g. axioms, judgements, assumptions,
+etc.) to support formal proofs of the algorithms.
+
+Dijkstra is one of the fathers of a large part of the movement toward
+formal proofs and program semantics.
+
+\begin{quote}
+{\bf The required techniques of effective reasoning are pretty formal,
+but as long as programming is done by people that don't master them,
+the software crisis will remain with us and will be considered an
+incurable disease.}\\
+ Edsgar Dijkstra \cite{Dijk00}
+\end{quote}
+
+The missive of creating a world where formal proofs of programs is the
+norm was given by Dijkstra.
+
+\begin{quote}
+{\bf The programmer should not ask how applicable the techniques of
+sound programming are, he should create a world in which they are
+applicable. It is his only way of delivering a highquality design.}\\
+ Edsgar Dijkstra \cite{Dijk00}
+\end{quote}
+
+The challenge we face, and the problem we attack, is constructing this
+``world'' so that Axiom programmers can develop algorithms whose
+implementations are highquality, proven code.
+
+There are, of course, "political problems" in the sense that
+programmers outright reject the very notion of proving programs
+correct.
+
+\begin{quote}
+{\bf One reason for preferring symbolmanipulating, calculating
+arguments is that their design is much better teachable than the
+design of verbal/pictorial arguments. Largescale introduction of
+courses on such calculational methodology, however, would encounter
+unsurmountable political problems.}\\
+ Edsgar Dijkstra \cite{Dijk00}
+\end{quote}
+
+The antiproof arguments abound and are not novel. Dijstra provides
+hope (and working examples) that these can be overcome.
+
+\begin{quote}
+{\bf The first pleasant  and very encouraging!  experience was the
+killing of the myth that formal proofs are of necessity long, tedious,
+laborious, errorprone, and whathaveyou. On the contrary, our proofs
+turned out to be short and simple to check, carried out  as they are
+ in straightforward manipulations from a modest repertoire.}\\
+ Dijkstra and Scholten \cite{Dijk90}
+\end{quote}
+
+There is a growing movement to formalize mathematics using computer
+aided proofs. The Xena Project \cite{Xena19} argues that we need to
+teach the next generation to develop verified algorithms. The thrust
+is toward {\sl rigorous mathematics}, that is, mathematics
+{\sl that is guaranteed to be correct}.
+
+\begin{quote}
+{\bf The classical engineering disciplines all have their standard
+mathematical techniques that are applied to the design of any
+artifact, before it is deployed, to gain confidence about its safety,
+suitability for some purpose, and so on. The engineers in a discipline
+more or less agree on what are ``the rules'' to be followed in vetting
+a design. Those rules are specified with a high degree of rigor, so
+that it isn't a matter of opinion whether a design is safe. Why
+doesn't software engineering have a corresponding agreedupon
+standard, whereby programmers convince themselves that their systems
+are safe, secure, and correct? The concepts and tools may not quite be
+ready yet for broad adoption, but they have been under development for
+decades. }\\
+ Adam Chlipala \cite{Chli17}
+\end{quote}
+
+Axiom has many algorithms that have mathematical specifications, such
+as the GCD. Proving that the implementation meets the specification
+will make the code more reliable.
+
+\begin{quote}
+{\bf Proofs serve two main purposes. First, proofs provide a way to ensure
+the reliability of mathematical claims, just as laboratory
+verification provides a check in the other sciences. Second, the act
+of finding a proof often yields, as a byproduct, new insights and
+unexpected new data, just as does work in the laboratory.}\\
+ Jaffe and Quinn \cite{Jaff93}
+\end{quote}
+
+There is the fundamental question of which logic to choose. It turns
+out that this can be decided at the programmer's convenience if we
+could separate the question of ``the logic'' from the ``machinery''
+to implement the logic.
+
+As a fellow computational mathematician, Andrej Bauer is reducing a
+logic system to its finegrain structure, separating the question of
+the kernel (aka the nucleus) from the judgements that define the logic.
+
+\begin{quote}
+{\bf A Proof Assistant Wish List:
+\begin{itemize}
+\item small trusted kernel
+\item userdefinable dependent type theories
+\item including userdefinable judgemental equality
+\item no commitment to an ambient type theory
+\item support common proofdevelopment techniques
+\end{itemize}
+}
+
+ Andrej Bauer \cite{Baue19a}
+\end{quote}
+
+We plan to develop the judgements, axioms, and other logic machinery
+in a fully factored form so that it can be inherited. This allows the
+definition of a commutative versus a noncommutative domain by simply
+choosing different categories to inherit. Bauer's idea of separation
+of the nucleus from the logic allows us to experiement with different
+forms of reasoning in an integrated way. This achieves one of Milner's
+goals.
+
+\begin{quote}
+{\bf [...] in any realistic work with the machine as a proof assistant
+we expect to be working in a particular problem domain, or theory as
+we shall call it [...] it should [...] allow us access to those
+tactics that we have previously defined either of general use or
+pertaining to the theory in question. Furthermore, almost every
+interesting applied theory is founded upon more primitive theories
+(called its ancestor theories), and while working in any theory we
+expect to have access to all material pertaining to its ancestors.
+
+An important function of the proof assistant is therefore to keep our
+tower of theories properly organized, allowing us [...] to work in
+any existing theory (not only those at the top of the tower) by
+proving new theorems in them.}\\
+ Robin Milner \cite{Miln84}
+\end{quote}
+
Axiom supports ``First Class Dynamic Types''. This allows code to
construct and query new types at run time.
@@ 566,6 +730,47 @@ math) is dead. Long live the King (Concrete Mathematics).}\\
 Doron Zeilberger \cite{Zeil02}
\end{quote}
+Make no mistake, this is an enourmous task.
+
+It requires a deep understanding of how Axiom implements firstorder
+dependent type theory. Dependent types are undecidable so there have
+to be heuristics and some userextensible mechanism for new
+heuristics.
+
+It requires a deep understanding of firstorder dependent types. How
+can we construct a new dependent type "on the fly" in the interpreter
+that is typecorrect and provable?
+
+It requires a deep understanding of Type Theory. Which form of type
+theory is used? How can it be factored into categories? How can we
+show that all inherited paths form sound and complete types?
+
+It requires a deep understanding of the Calculus of Construction with
+induction. Coq and Lean implement this form of logic. They are both at
+the leading edge of the field and still under active development and
+debate.
+
+It requires a deep understanding of Program Verification. Coq and Lean
+do not (yet) have libraries that directly support program
+semantics. Nor does the Spad language (yet) have welldefined
+semantics.
+
+It requires proving algorithms that may never have been proven, may
+not be correct, and may not terminate under all inputs. Further, many
+of the algorithms have no specification.
+
+It requires constructing a welltyped compiler and a welltyped
+interpreter. The compiler needs to parse both the Spad language and
+the new logical extensions.
+
+It requires validation and verification of the welltypedness of the
+compiler and interpreter, both of which are implemented in CLOS on top
+of Common Lisp.
+
+It requires constructing the whole tower on a trusted kernel of logic
+which itself might sit on a trusted nucleus that can adapt to a range
+of logics. This must be verified and validated ``to the metal''.
+
\chapter{The Problem}
\section{A Brief History}
@@ 2255,8 +2460,70 @@ UABBREV ::= UCHAR
\label{UABBREVsyntax}
\end{figure}
+\index[fig]{FLOAT syntax}
+\begin{figure}[H]
+\centering
+\begin{tikzpicture}[
+ point/.style={coordinate},>=stealth',thick,draw=black!50,
+ tip/.style={>,shorten >=0.007pt},every join/.style={rounded corners},
+ hv path/.style={to path={ (\tikztotarget)}},
+ vh path/.style={to path={ (\tikztotarget)}},
+ text height=1.5ex,text depth=.25ex % align text horizontally
+ ]
+ \matrix[column sep=4mm] {
+ % First row:
+ & & & & & & & & & & & \node (plus) [terminal] {+};\\
+ % Second row:
+ \node (p1) [point] {}; & \node (ui1) [nonterminal] {unsigned integer};&
+ \node (p2) [point] {}; & \node (dot) [terminal] {.}; &
+ \node (p3) [point] {}; & \node (digit) [terminal] {digit}; &
+ \node (p4) [point] {}; & \node (p5) [point] {}; &
+ \node (p6) [point] {}; & \node (e) [terminal] {E}; &
+ \node (p7) [point] {}; & &
+ \node (p8) [point] {}; & \node (ui2) [nonterminal] {unsigned integer};&
+ \node (p9) [point] {}; & \node (p10) [point] {};\\
+ % Third row:
+ & & & & & & & & & & & \node (minus)[terminal] {};\\
+ };
+
+ { [start chain]
+ \chainin (p1);
+ \chainin (ui1) [join=by tip];
+ \chainin (p2) [join];
+ \chainin (dot) [join=by tip];
+ \chainin (p3) [join];
+ \chainin (digit) [join=by tip];
+ \chainin (p4) [join];
+ { [start branch=digit loop]
+ \chainin (p3) [join=by {skip loop=6mm,tip}];
+ }
+ \chainin (p5) [join,join=with p2 by {skip loop=6mm,tip}];
+ \chainin (p6) [join];
+ \chainin (e) [join=by tip];
+ \chainin (p7) [join];
+ { [start branch=plus]
+ \chainin (plus) [join=by {vh path,tip}];
+ \chainin (p8) [join=by {hv path,tip}];
+ }
+ { [start branch=minus]
+ \chainin (minus) [join=by {vh path,tip}];
+ \chainin (p8) [join=by {hv path,tip}];
+ }
+ \chainin (p8) [join];
+ \chainin (ui2) [join=by tip];
+ \chainin (p9) [join,join=with p6 by {skip loop=11mm,tip}];
+ \chainin (p10) [join=by tip];
+ }
+\end{tikzpicture}
+\begin{verbatim}
+FLOAT ::=
+\end{verbatim}
+\caption{FLOAT syntax}
+\label{FLOATsyntax}
+\end{figure}
+
\index[fig]{ABBREV syntax}
\begin{figure}[ht]
+\begin{figure}[H]
\centering
\begin{tikzpicture}[
point/.style={coordinate},>=stealth',thick,draw=black!50,
@@ 2802,6 +3069,86 @@ turns a string into characters.
\end{chunk}
+\index[fig]{IF syntax}
+\begin{figure}[H]
+\centering
+\begin{tikzpicture}[
+ point/.style={coordinate},>=stealth',thick,draw=black!50,
+ tip/.style={>,shorten >=0.007pt},every join/.style={rounded corners},
+ hv path/.style={to path={ (\tikztotarget)}},
+ vh path/.style={to path={ (\tikztotarget)}},
+ text height=1.5ex,text depth=.25ex % align text horizontally
+ ]
+ \matrix[column sep=4mm] {
+ \node (p1) [point] {}; &
+ \node (if) [terminal] {if}; &
+ \node (test) [nonterminal] {test}; &
+ \node (then) [terminal] {then}; &
+ \node (trueblk) [nonterminal] {block}; &
+ \node (p5) [point] {}; &
+ \node (else) [terminal] {else}; &
+ \node (falseblk) [nonterminal] {block}; &
+ \node (p7) [point] {}; &
+ \node (p8) [point] {}; \\
+ };
+
+ { [start chain]
+ \chainin (p1);
+ \chainin (if) [join];
+ \chainin (test) [join];
+ \chainin (then) [join];
+ \chainin (trueblk) [join];
+ \chainin (p5) [join];
+ \chainin (else) [join];
+ \chainin (falseblk) [join];
+ \chainin (p7) [join,join=with p5 by {skip loop=5mm,tip}];
+ \chainin (p8) [join];
+ }
+\end{tikzpicture}
+\begin{verbatim}
+IF ::= if TEST then BLOCK [else BLOCK]
+\end{verbatim}
+\caption{IF syntax}
+\label{IFsyntax}
+\end{figure}
+
+\index[fig]{FOR syntax}
+\begin{figure}[H]
+\centering
+\begin{tikzpicture}[
+ point/.style={coordinate},>=stealth',thick,draw=black!50,
+ tip/.style={>,shorten >=0.007pt},every join/.style={rounded corners},
+ hv path/.style={to path={ (\tikztotarget)}},
+ vh path/.style={to path={ (\tikztotarget)}},
+ text height=1.5ex,text depth=.25ex % align text horizontally
+ ]
+ \matrix[column sep=4mm] {
+ \node (p1) [point] {}; &
+ \node (for) [terminal] {for}; &
+ \node (var) [terminal] {variable.}; &
+ \node (in) [terminal] {in}; &
+ \node (expr) [nonterminal] {expression}; &
+ \node (rep) [terminal] {repeat}; &
+ \node (blk) [nonterminal] {block}; \\
+ };
+
+ { [start chain]
+ \chainin (p1);
+ \chainin (for) [join];
+ \chainin (var) [join];
+ \chainin (in) [join];
+ \chainin (expr) [join];
+ \chainin (rep) [join];
+ \chainin (blk) [join];
+ }
+\end{tikzpicture}
+\begin{verbatim}
+FOR ::= for VARIABLE in EXPRESSION repeat BLOCK
+\end{verbatim}
+\caption{FOR syntax}
+\label{FORsyntax}
+\end{figure}
+
\section{The Compiler Function}
Given a {\bf theparse} structure, construct the corresponding
@@ 3616,7 +3963,8 @@ SIGNAME ::= SPECIALNAME  SYMBOL
FSMSIG ::= INDENT SIGNAME [':' SIGINTYPE '>' SIGOUTTYPE] [SIGIFSEC]
\end{verbatim}
\begin{figure}[ht]
+\index[fig]{FSMSIG syntax}
+\begin{figure}[H]
\centering
\begin{tikzpicture}
@@ 3648,114 +3996,24 @@ FSMSIG ::= INDENT SIGNAME [':' SIGINTYPE '>' SIGOUTTYPE] [SIGIFSEC]
(q10) edge[above] node{ifspec} (q11);
\end{tikzpicture}
\caption{FUNSIG Anonymous function signature}
\label{FSMSIG}
\end{figure}

\begin{figure}[ht]
\centering
%% if_stmt ::= "if" expression ":" suite
%% ["else" ":" suite]
%%
\begin{tikzpicture}[point/.style={coordinate},>=stealth',thick,draw=black!50,
 tip/.style={>,shorten >=0.007pt},every join/.style={rounded corners},
 hv path/.style={to path={ (\tikztotarget)}},
 vh path/.style={to path={ (\tikztotarget)}},
 text height=1.5ex,text depth=.25ex]
 \matrix[ampersand replacement=\&,column sep=4mm] {
 \node(p1) [point] {}; \&
 \node(ifs) [terminal] {if}; \&
 \node(expr1) [nonterminal] {expr}; \&
 \node(colon1) [terminal] {;}; \&
 \node(suite1) [nonterminal] {suite}; \&
 \node(p5) [point] {}; \&
 \node(else) [terminal] {else}; \&
 \node(colon3) [terminal] {;}; \&
 \node(suite3) [nonterminal] {suite}; \&
 \node(p16) [point] {}; \&
 \node(p17) [point] {}; \\
 };

 { [start chain]
 \chainin (p1);
 \chainin (ifs) [join=by tip];
 \chainin (expr1) [join=by tip];
 \chainin (colon1) [join=by tip];
 \chainin (suite1) [join];
 \chainin (p5) [join];
% \chainin (p16) [join,join=with p5 by {skip loop=11mm,tip}];
 \chainin (else) [join=by tip];
 \chainin (colon3) [join=by tip];
 \chainin (suite3) [join=by tip];
 \chainin (p16) [join];
 \chainin (p17) [join=by tip];
 \chainin (p16) [join=with p5 by {skip loop=11mm,tip}];
 }
\end{tikzpicture}
\caption{IF syntax}
\label{IFsyntax}
+\begin{verbatim}
+FSMSIG ::=
+\end{verbatim}
+\caption{FSMSIG syntax}
+\label{FSMSIGsyntax}
\end{figure}
+\index[fig]{LEAVE syntax}
\begin{figure}[ht]
\centering
\begin{tikzpicture}[
 point/.style={coordinate},>=stealth',thick,draw=black!50,
 tip/.style={>,shorten >=0.007pt},every join/.style={rounded corners},
 hv path/.style={to path={ (\tikztotarget)}},
 vh path/.style={to path={ (\tikztotarget)}},
 text height=1.5ex,text depth=.25ex % align text horizontally
 ]
 \matrix[column sep=4mm] {
 % First row:
 & & & & & & & & & & & \node (plus) [terminal] {+};\\
 % Second row:
 \node (p1) [point] {}; & \node (ui1) [nonterminal] {unsigned integer};&
 \node (p2) [point] {}; & \node (dot) [terminal] {.}; &
 \node (p3) [point] {}; & \node (digit) [terminal] {digit}; &
 \node (p4) [point] {}; & \node (p5) [point] {}; &
 \node (p6) [point] {}; & \node (e) [terminal] {E}; &
 \node (p7) [point] {}; & &
 \node (p8) [point] {}; & \node (ui2) [nonterminal] {unsigned integer};&
 \node (p9) [point] {}; & \node (p10) [point] {};\\
 % Third row:
 & & & & & & & & & & & \node (minus)[terminal] {};\\
 };

 { [start chain]
 \chainin (p1);
 \chainin (ui1) [join=by tip];
 \chainin (p2) [join];
 \chainin (dot) [join=by tip];
 \chainin (p3) [join];
 \chainin (digit) [join=by tip];
 \chainin (p4) [join];
 { [start branch=digit loop]
 \chainin (p3) [join=by {skip loop=6mm,tip}];
 }
 \chainin (p5) [join,join=with p2 by {skip loop=6mm,tip}];
 \chainin (p6) [join];
 \chainin (e) [join=by tip];
 \chainin (p7) [join];
 { [start branch=plus]
 \chainin (plus) [join=by {vh path,tip}];
 \chainin (p8) [join=by {hv path,tip}];
 }
 { [start branch=minus]
 \chainin (minus) [join=by {vh path,tip}];
 \chainin (p8) [join=by {hv path,tip}];
 }
 \chainin (p8) [join];
 \chainin (ui2) [join=by tip];
 \chainin (p9) [join,join=with p6 by {skip loop=11mm,tip}];
 \chainin (p10) [join=by tip];
 }
\end{tikzpicture}
\caption{FLOAT syntax}
\label{FLOATsyntax}
+TODO
+\caption{LEAVE syntax}
+\begin{verbatim}
+LEAVE
+\end{verbatim}
+\label{LEAVEsyntax}
\end{figure}


\begin{verbatim}
FUNCTIONSPEC ::= INTTYPE
 INTYPE > OUTPUT
@@ 4179,9 +4437,262 @@ definition of {\bf bye} and restore it when the interpreter exits.
\end{chunk}
+\chapter{Axioms and Logic Rules}
+
+\begin{quote}
+{\bf Dieudonn\'e suggests that casual reasoning is a childhood disease
+of mathematical areas.}\\
+ Arthur Jaffe and Frank Quinn \cite{Jaff93}
+\end{quote}
+
+\begin{quote}
+{\bf What mathematicians are accomplishing is to advance human
+understanding of mathematics.}\\
+ William P. Thurston \cite{Thur94}
+\end{quote}
+
+\begin{quote}
+{\bf If you make the tools, you make the rules}\\
+ Andrew Dana Hudson \cite{Huds19}
+\end{quote}
+
+Collected here are some axioms that need to be distributed among the
+various categories so that they can be inherited at the proper time.
+
+There is an interesting design question.
+
+Axiom already has a mechanism for inheriting signatures from
+categories. That is, we can get a plus signature from, say, the
+Integer category.
+
+Suppose we follow the same pattern. Currently Axiom inherits certain
+socalled ``attributes'', such as ApproximateAttribute, which implies
+that the computation results are only approximate.
+
+We could adapt the same mechanism to inherit the Transitive
+property. In fact, if we follow the ``tiny theory'' approach of
+Carette and Farmer where each property is in its own inheritable
+category, then we can ``mix and match'' the axioms at will.
+
+An axiom category would also export a function. This function would
+essentially be a ``tactic'' used in a proof. It would modify the proof
+step by applying the function to the step.
+
+Theorems could have the same structure.
+
+This allows theorems to be constructed at run time (since
+Axiom supports ``First Class Dynamic Types''.
+
+In addition, this design can be "pushed down" into the Spad language
+so that Spad statements (e.g. assignment) had proofrelated
+properties. A ramge such as [1..10] would provide explicit bounds in a
+proof ``by language definition''. Defining the logical properties of
+language statements in this way would make it easier to construct
+proofs since the invariants would be partially constructed already.
+
+The design merges the computer algebra inheritance structure with the
+proof of algorithms structure, all under the same mechanism.
+
+{\bf Reflexivity}
+
+\begin{prooftree}
+\AxiomC{}
+\UnaryInfC{$e=e$}
+\end{prooftree}
+
+{\bf Symmetry}
+
+\begin{prooftree}
+\AxiomC{$e_2=e_1$}
+\UnaryInfC{$e_1=e_2$}
+\end{prooftree}
+
+{\bf Transitivity}
+
+\begin{prooftree}
+\AxiomC{$e_1=e_3$}
+\AxiomC{$e_3=e_2$}
+\BinaryInfC{$e_1=e_2$}
+\end{prooftree}
+
+{\bf Congruence}
+
+\begin{prooftree}
+\AxiomC{$f=f^\prime$}
+\AxiomC{$e_1=e_1^\prime$}
+\AxiomC{$\ldots$}
+\AxiomC{$e_n=e_n^\prime$}
+\QuaternaryInfC{$f(e_1,\ldots,e_n)=f^\prime(e_1^\prime,\ldots,e_n^\prime)$}
+\end{prooftree}
+
+For SemiRings we know that
+\[\begin{array}{rcl}
+(a+b)+c&=& a+(b+c)\\
+0+a &=& a\\
+a+0 &=& a\\
+a+b &=& b+a\\
+(a\times b)\times c&=&a\times(b\times c)\\
+1\times a &=& a\\
+a\times 1 &=& a\\
+a\times(b+c) &=& (a\times b)+(a\times c)\\
+(a+b)\times c &=& (a\times c)+(b\times c)\\
+0\times a &=& 0\\
+a\times 0 &=& 0\\
+\end{array}\]
+
+For Rng we have
+
+An rng is a set $R$ with two binary operations $(+,)$ such that
+\begin{itemize}
+\item $(R,+)$ is an abelian group
+\item $(R,)$ is a semigroup
+\item Multiplication distributes over additin
+\item $f(x+y) = f(x)+f(y)$
+\item $f(x*y) = f(x)*f(y)$
+\end{itemize}
+An rng does not have an identity element.
+
+{\bf Variable}
+
+\begin{prooftree}
+\AxiomC{$\langle x^{\tau},\sigma,\Gamma\rangle \to
+\langle \sigma (x^{\tau}),\sigma,\Gamma\rangle$}
+\end{prooftree}
+
+{\bf CallArguments}
+
+\begin{prooftree}
+\AxiomC{$\langle e_i,\sigma,\Gamma\rangle \to
+\langle e_i^\prime, \sigma^\prime, \Gamma\rangle$}
+\UnaryInfC{$e_0 (v_1,\ldots,e_i,\ldots,e_n),\sigma,\Gamma\rangle\to
+\langle e_0 (v_1,\ldots,e_i^\prime,\ldots,e_n),\sigma^\prime,\Gamma\rangle$}
+\end{prooftree}
+where the $x_i$ are parameters of $v_0$
+
+{\bf CallOperator}
+
+\begin{prooftree}
+\AxiomC{$\langle e_0,\sigma,\Gamma\rangle \to
+\langle e_0,\sigma^\prime,\Gamma\rangle$}
+\UnaryInfC{$\langle e_0 (v_1,\ldots,v_n),\sigma,\Gamma\rangle \to
+\langle e_0^\prime (v_1,\ldots,v_n),\sigma^\prime,\Gamma\rangle$}
+\end{prooftree}
+where the $x_i$ are the parameters of $v_0$
+
+{\bf Call}
+
+\begin{prooftree}
+\AxiomC{$\langle v_0^{\tau_0}(v_1^{\tau_1},\ldots,v_n^{\tau_n}),
+\sigma,\Gamma\rangle
+\to \langle v_0^{\tau_0}[v_1^{\tau_1}/x_1,\ldots,
+v_n^{\tau_n}/x_n],\sigma,\Gamma\rangle$}
+\end{prooftree}
+where the $x_i$ are parameters of $v_0$
+
+{\bf Qualified Expression}
+
+\begin{prooftree}
+\AxiomC{$\begin{array}{ccc}
+& \langle \delta_1,\sigma,\Gamma_1\rangle \to
+\langle\delta_1^\prime,\sigma,\Gamma_2\rangle
+& \langle\delta_2,\sigma,\Gamma_2\rangle \to
+\langle\delta_2^\prime,\sigma,\Gamma_3\rangle\\
+\cdots
+& \langle\delta_n,\sigma,\Gamma_n\rangle \to
+\langle\delta_n^\prime,\sigma,\Gamma_{n+1}\rangle
+& \langle e,\sigma,\Gamma_{n+1}\rangle \to
+\langle e^\prime,\sigma^\prime,\Gamma_{n+2}\rangle
+\end{array}$}
+\UnaryInfC{$\langle e {\rm\ where\ }\delta_1\cdots\delta_n,\sigma,\Gamma_1
+\rangle \to \langle e^\prime,\sigma^\prime,\Gamma_{n+2}\rangle$}
+\end{prooftree}
+
+{\bf SequenceHead}
+
+\begin{prooftree}
+\AxiomC{$\langle s_1,\sigma_1,\Gamma_1\rangle\to
+\langle s_1^\prime,\sigma_2,\Gamma_2\rangle$}
+\UnaryInfC{$\langle s_1;s_2,\sigma_1,\Gamma_1\rangle\to
+\langle s_1^\prime;s_2,\sigma_2,\Gamma_2\rangle$}
+\end{prooftree}
+
+{\bf SequenceTail}
+
+\begin{prooftree}
+\AxiomC{$\langle v_1;s_2,\sigma,\Gamma\rangle\to
+\langle s_2,\sigma,\Gamma\rangle$}
+\end{prooftree}
+
+{\bf IfTrue}
+
+\begin{prooftree}
+\AxiomC{$\langle s_1,\sigma,\Gamma\rangle\to
+\langle s_1^\prime,\sigma^\prime,\Gamma^\prime\rangle$}
+\UnaryInfC{$\langle {\rm\ if\ true\ then\ }s_1; s_2,\sigma,\Gamma\rangle\to
+\langle s_1^\prime,\sigma^\prime,\Gamma^\prime\rangle$}
+\end{prooftree}
+
+{\bf IfFalse}
+
+\begin{prooftree}
+\AxiomC{$\langle s_2,\sigma,\Gamma\rangle\to
+\langle s_2^\prime,\sigma^\prime,\Gamma^\prime\rangle$}
+\UnaryInfC{$\langle {\rm\ if\ false\ then\ } s_1; s_2,\sigma,\Gamma\rangle\to
+\langle s_2^\prime,\sigma^\prime,\Gamma^\prime\rangle$}
+\end{prooftree}
+
+{\bf AssignmentLeft}
+
+\begin{prooftree}
+\AxiomC{$\langle e_1,\sigma_0,\Gamma\rangle \to
+\langle e_1^\prime, \sigma_1, \Gamma\rangle$}
+\UnaryInfC{$\langle e_1:=e_2,\sigma,\Gamma\rangle\to
+\langle e_1^\prime:=e_2,\sigma_1,\Gamma\rangle$}
+\end{prooftree}
+
+{\bf AssignmentRight}
+
+\begin{prooftree}
+\AxiomC{$\langle e_2,\sigma,\Gamma\rangle \to
+\langle e_2^\prime,\sigma^\prime,\Gamma\rangle$}
+\UnaryInfC{$\langle l:=e_2,\sigma,\Gamma\rangle\to
+\langle l:=e_2^\prime,\sigma^\prime,\Gamma\rangle$}
+\end{prooftree}
+
+{\bf Assignment}
+
+\begin{prooftree}
+\AxiomC{}
+\UnaryInfC{$\langle l:=v^{\tau},\sigma,\Gamma\rangle\to
+\langle v^{\tau},\sigma[v^{\tau}/l],\Gamma\rangle$}
+\end{prooftree}
+
+{\bf Immediate Definition}
+
+\begin{prooftree}
+\AxiomC{$\langle e,\sigma,\Gamma\rangle\to
+\langle e^\prime,\sigma_1,\Gamma\rangle$}
+\UnaryInfC{$\langle x:\tau:=e,\sigma,\Gamma\rangle\to
+\langle x:\tau:=e^\prime,\sigma_1,\Gamma\rangle$}
+\end{prooftree}
+
+{\bf Immediate Definition}
+
+\begin{prooftree}
+\AxiomC{$\langle x:\tau:=v^{\tau},\sigma,\Gamma\rangle\to
+\langle v^{\tau},\sigma,\Gamma,x^{\tau}==v^{\tau}\rangle$}
+\end{prooftree}
\chapter{The Categories}
+One of the primary concerns is {\bf Coherence} \cite{Bott19} of these
+type definitions. Because we are using CLOS the system automatically
+computes the coherence between types.
+
+Axiom computes type resolution based on {\sl modemaps} but the
+talk by Bottu and Mardirosian \cite{Bott19} does type resolution
+by creating unique names instead.
+
There are patterns in the following code. Violating these patterns
will generate obscure bugs so be careful. Lets assume a given class.
@@ 42055,6 +42566,163 @@ walk the sorted keys to output the sorted lines.
\end{chunk}
+\chapter{Musings}
+
+From Bauer \cite{Baue07}
+
+Given General Indeuctive Types, the theory {\tt Branching}
+describes that a branching type consists of a set $s$ and a set $t$
+depending on $s$. The theory $W$ is parameterized by a branching type
+$B$. It specifies a set $w$ of wellfounded trees and a treeforming
+operation $tree$ with a dependent type\\
+$\Pi_{s\in B.s}(B.t(x) \rightarrow w) \rightarrow w.$
+Given a branching type $x$ and a map
+$f~:~B.t(x) \rightarrow w$, $tree~x~f$ is the tree whose root has
+branching type $x$ and whose successor labeled by $l\in~B.t(x)$ is the
+tree $f(l)$. The inductive nature of $w$ is expressed with the axiom
+{\tt induction}, which states that for every property $M.p$, if $M.p$
+is an inductive property then every tree satisfies it. A property is
+said to be {\sl inductive} if a tree $tree~x~f$ satisfies it whenever
+all its successors satisfy it.
+
+Parameter W : [B : Branching] $\rightarrow$\\
+thy\\
+\hspace*{0.2cm}Parameter w : Set.\\
+\hspace*{0.2cm}Parameter tree : [x : B.x] $\rightarrow$
+(B.t x $\rightarrow$ w) $\rightarrow$ w.\\
+\hspace*{0.2cm}Axiom induction:\\
+\hspace*{0.4cm}$\forall$ M : thy Parameter p : w
+$\rightarrow$ Prop. end,\\
+\hspace*{0.4cm}($\forall$ x : B.x,
+$\forall$ f : B.t x $\rightarrow$ w,\\
+\hspace*{0.6cm}(($\forall$ y : B.t x, M.p (f y))
+$\rightarrow$ M.p (tree x f))) $\rightarrow$\\
+\hspace*{0.4cm}$\forall$ t : w, M.p t.\\
+end.
+
+A handwritten OCAML program is
+\begin{verbatim}
+module W (B : Branching) = struct
+ type w = Tree of B.s * (B.t > w)
+ let tree x y = Tree (x, y)
+ let rec induction f (Tree (x, g)) =
+ f x g (fun y  induction f (g y))
+end
+\end{verbatim}
+
+
+The RZ program generates:
+\begin{verbatim}
+module type Branching =
+ sig
+ type s
+ (** predicate (=s=) : s > s > bool *)
+ (** assertion symmetric_s : forall x:s, y:s, x =s= y > y =s= x
+ assertion transitive_s :
+ forall x:s, y:s, z:s, x =s= y /\ y =s= z > x =s= z
+ *)
+ (** predicate s : s > bool *)
+ (** assertion total_def_s : forall x:s, x : s <> x =s= x
+ *)
+ (** branching types *)
+ type t
+ (** predicate (=t=) : s > t > t > bool *)
+ (** assertion strict_t : forall x:s, y:t, z:t, y =(t x)= z > x : s
+ assertion extensional_t :
+ forall x:x, y:s, z:t, w:t, s =s= y > z =(t x)= w > z =(t y)= w
+ assertion symetric_t :
+ forall x:s, y:t z:t, y =(t x)= z > z =(t x)= y
+ assertion transitive_t :
+ forall x:s, y:t, z:t, w:t, y =(t x)= z /\ z =(t x)= w >
+ y =(t x)= w
+ *)
+ (** predicate t : s > t > bool *)
+ (** assertion total_def_t :
+ forall x:s, y:t, y : t x <> y =(t x)= y
+ *)
+ (** branch labels *)
+ end
+
+module W : functor (B : Branching) >
+sig
+ type w
+ (** prediate (=w=) : w > w > bool *)
+ (** assertion symmetric_w :
+ forall x:w, y:w, x =w= y > y =w= x
+ assertion transitive_w :
+ forall x:w, y:w, z:w, x =w= y /\ y =w= z > x =w= z
+ *)
+ (** predicate w : w > bool *)
+ (** assertion total_def_w : forall x:w, x : w <> x =w= x
+ *)
+ val tree : B.s > (B.t > w) > w
+ (** assertion tree_support :
+ forall x:B.s, y:B.s, x =B.s= y >
+ forall f:B.t > w, g:B.t > w,
+ (forall z:B.t, t:B.t, z =(B.t x)= t > f z =w= g t) >
+ tree x f =w= tree y g
+ *)
+ val induction : (B.s > (B.t > w) > (B.t > 'ty_p) > 'ty_p) > w > 'ty_p
+ (** assertion 'ty_p [p:w > 'ty_p > bool] induction :
+ (forall x:w, a:'ty_p, p x a > x : w) >
+ (forall x:w, y:w, a:'ty_p, x =w= y > p x a > p y a) >
+ forall f:B.s > (B.t > w) > (B.t > 'ty_p) > 'ty_p,
+ (forall (x:B.s),
+ forall f':B.t > w,
+ (forall y:B.t, z:B.t, y =(B.t x)= z >
+ f' y =w= f' z) >
+ forall g:B.t > 'ty_p,
+ (forall y:B.t, y : B.t x > p (f' y) (g y)) >
+ p (tree x f') f x f' g)) >
+ forall (t:w), p t (induction f t)
+ *)
+end
+\end{verbatim}
+
+
+From Bauer \cite{Baue19}
+\begin{itemize}
+\item Type : Type ... a paradoxical universe of types
+\item $\Pi (x : T_1), T_2$ ... dependent products
+\item $\lambda (x : T) \rightarrow e$ ... functions
+\item $e_1 e_2$ ... application
+\item $e : T$ ... type ascriptions
+\end{itemize}
+
+\begin{itemize}
+\item Definition x := e. ... define a value
+\item Axiom x : T. ... assume a constant
+\item Check e. ... check the type of an expression
+\item Eval e. ... evaluate an expression
+\item Load "". ... load a file
+\end{itemize}
+
+From Bauer \cite{Baue19a}
+\begin{itemize}
+\item $\Gamma \vdash A {\tt type}$ is a type
+\item $\Gamma \vdash t : A$ is a term of type $A$
+\item $\Gamma \vdash A \equiv B$ types $A$ and $B$ are equal
+\item $\Gamma \vdash t \equiv u : A$ terms $t$ and $u$ of type $A$ are
+equal
+\end{itemize}
+
+From Bauer \cite{Baue19a}, Rules for dependent products
+\begin{itemize}
+\item rule $\Pi$ (A type) (\{x:A\} B type) type
+\item rule $\lambda$ (A type) (\{x:A\} B type)
+ (\{x:A\} e : \{B\}) : $\Pi$ A B
+\item app (A type) (\{x:A\} B type)
+(S : $\Pi$ A B) (a : A) : B\{a\}
+\item rule $\Pi\_\beta$ (A type) (\{x:A\} B type)
+(\{x:A\} S : B\{x\}) (a : A)\\
+: app A B ($\lambda$ A B S) a $\equiv$ S\{a\} : B\{a\}
+\item rule Id (A type (a : A) (b : A) type
+\item rule equality\_reflection\\
+(A type (a:A0 (b:A) (p:Id A a b) : a $\equiv$ b : A
+\end{itemize}
+
+\chapter{Quote collections}
+
\begin{quote}
{\bf The best programs are written so that computing machines can
perform them quickly and so that human beings can understand them
@@ 42142,6 +42810,67 @@ his stomach all that he has ever eaten.}\\
 Arthur Schopenhauer \cite{Scho16}
\end{quote}
+\begin{quote}
+{\bf When one considers how hard it is to write a computer program
+even approaching the intellectual scope of a good mathematical paper,
+and how much greater time and effort have to be put into it to make it
+``almost'' formally correct, it is preposterous to claim that
+mathematics as we practice it is anywhere near formally correct.}\\
+ William P. Thurston \cite{Thur94}
+\end{quote}
+
+\begin{quote}
+{\bf Given the concepts 0, {\sl number}, and {\sl successor}
+and the rules
+\begin{enumerate}
+\item 0 is a {\sl number}
+\item the {\sl successor} of any {\sl number} is a {\sl number}
+\item no two {\sl numbers} have the same {\sl successor}
+\item 0 is not the {\sl successor} of any {\sl number}
+\item any property which belongs to 0 and also to the {\sl succesor}
+of every {\sl number} which has the property, belongs to all the
+{\sl numbers}
+\end{enumerate}}
+
+ Giuseppe Peano \cite{Russ1920}
+\end{quote}
+
+\begin{quote}
+{\bf I WANT a type theory with this strange property.\\
+Well, then you deserve it.}\\
+ Andrej Bauer \cite{Baue19a}
+\end{quote}
+
+\begin{quote}
+{\bf The Axiom Sane effort is, to quote Alan Kay, ``the simplest thing that
+is qualitatively different from where we are''.}\\
+ Tim Daly \cite{Kayx19}
+\end{quote}
+
+\begin{quote}
+{\bf I am a biological copying machine.}\\
+ Tim Daly
+\end{quote}
+
+\begin{quote}
+{\bf Computers are intellectual mirrors. To program, you must be the
+machine.}\\
+ Tim Daly
+\end{quote}
+
+\begin{quote}
+{\bf From a certain point of view, having a convenient representation
+of one's behavior available for modification is what is meant by
+consciousness.}\\
+ John McCarthy \cite{Mcca63}
+\end{quote}
+
+\begin{quote}
+{\bf Even when I write a oneshot program I write it in a literate way
+because I get it right faster that way.}\\
+ Donald Knuth \cite{Knut19}
+\end{quote}
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\appendix
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index f26de0c..759e401 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 729,7 +729,8 @@ paragraph for those unfamiliar with the terms.
author = "Barendregt, H. P.",
title = {{The Lambda Calculus: Its Syntax and Semantics}},
publisher = "Elsevier Science",
 year = "1984"
+ year = "1984",
+ keywords = "shelf"
}
\end{chunk}
@@ 2987,7 +2988,7 @@ paragraph for those unfamiliar with the terms.
pages = "365458",
year = "1991",
publisher = "MIT Press",
 isbn = "0444880747"
+ isbn = "0444880747",
}
\end{chunk}
@@ 3159,7 +3160,8 @@ paragraph for those unfamiliar with the terms.
Among the specific forms of types we discuss are simple types,
recursive types, polymorphic types, and dependent types. We also
briefly touch upon subtypes and inheritance, and the role of types
 in module systems for logic programming languages."
+ in module systems for logic programming languages.",
+ keywords = "shelf"
}
\end{chunk}
@@ 10342,6 +10344,27 @@ when shown in factored form.
\end{chunk}
\index{Avigad, Jeremy}
+\index{Harrison, John}
+\begin{chunk}{axiom.bib}
+@article{Avig14b,
+ author = "Avigad, Jeremy and Harrison, John",
+ title = {{Formally Verified Mathematics}},
+ journal = "Communications of the ACM",
+ volume = "57",
+ number = "4",
+ pages = "6675",
+ year = "2014",
+ abstract =
+ "With the help of computational proof assistants, formal
+ verification could beome the new standard for rigor in
+ mathematics.",
+ paper = "Avig14b.pdf",
+ keywords = "printed, DONE"
+}
+
+\end{chunk}
+
+\index{Avigad, Jeremy}
\begin{chunk}{axiom.bib}
@misc{Avig17b,
author = "Avigad, Jeremy",
@@ 13279,7 +13302,8 @@ when shown in factored form.
title = {{Fundamental Proof Methods in Computer Science}},
publisher = "MIT Press",
year = "2017",
 isbn = "9780262035538"
+ isbn = "9780262035538",
+ keywords = "shelf"
}
\end{chunk}
@@ 13596,6 +13620,49 @@ when shown in factored form.
\end{chunk}
\index{Awodey, Steve}
+\index{Bauer, Andrej}
+\begin{chunk}{axiom.bib}
+@misc{Awod04,
+ author = "Awodey, Steve and Bauer, Andrej",
+ title = {{Propositions as [Types]}},
+ year = "2004",
+ link = "\url{http://math.andrej.com/asset/data/bracket_types.pdf}",
+ abstract =
+ "Image factorizations in regular categories are stable under
+ pullbacks, as they model a natural modal operator in dependent
+ type theory. This unary type constructor [A] has turned up
+ previously in a syntactic form as a way of erasing computational
+ content, and formalizing a notion of proof irrelevance. Indeed,
+ semantically, the notion of a {\sl support} is sometimes used as
+ surrogate proposition asserting inhabitation of an indexed family.
+
+ We give rules for bracket types in dependent type theory and
+ provide complete semantics using regular categories. We show that
+ dependent type theory with the unit type, strong extensional
+ equality types, strong dependent sums, and bracket types is the
+ internal type theory of regular categories, in the same way that
+ the usual dependent type theory with dependent sums and products
+ is the internal type theory of locally cartesian closed
+ categories.
+
+ We also show how to interpret firstorder logic in type theory
+ with brackets, and we make use of the translation to compare type
+ theory with logic. Specifically, we show that the
+ propositionsastypes interpretation is complete with respect to a
+ certain fragment of intuitionistic firstorder logic, in the sense
+ that a formula from the fragment is derivable in intuitionistic
+ firstorder logic if, and only if, its interpretation in dependent
+ type theory is inhabited. As a consequence, a modified
+ doublenegation translation into type theory (without bracket
+ types) is complete, in the same sense, for all of classical
+ firstorder logic.",
+ paper = "Awod04.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Awodey, Steve}
\begin{chunk}{axiom.bib}
@misc{Awod12,
author = "Awodey, Steve",
@@ 13992,6 +14059,20 @@ when shown in factored form.
\end{chunk}
+\index{Barrett, William A.}
+\index{Couch, John D.}
+\begin{chunk}{axiom.bib}
+@book{Barr79,
+ author = "Barrett, William A. and Couch, John D.",
+ title = {{Compiler Construction: Theory and Practice}},
+ publisher = "Science Research Associates",
+ year = "1979",
+ isbn = "057421335X",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
\index{Barthe, Gilles}
\begin{chunk}{axiom.bib}
@article{Bart85,
@@ 14088,6 +14169,35 @@ when shown in factored form.
\end{chunk}
\index{Bauer, Andrej}
+\index{Stone, Christopher A.}
+\begin{chunk}{axiom.bib}
+@misc{Baue07,
+ author = "Bauer, Andrej and Stone, Christopher A.",
+ title = {{RZ: a Tool for Bringing Constructive and Computational
+ Mathematics Closer to Programming Practice}},
+ year = "2007",
+ link = "\url{http://math.andrej.com/wpcontent/uploads/2007/cielong.pdf}",
+ abstract =
+ "Realizability theory is not only a fundamental tool in logic and
+ computability, but also has direct application to the design and
+ implementation of programs: it can produce interfaces for the data
+ structure corresponding to a mathematical theory. Our tool, called
+ RS, serves as a bridge between the worlds of constructive
+ mathematics and programming. By using the realizability
+ interpretation of constructive mathematics, RZ translates
+ specifications in constructive logic into annotated interface code
+ in Objective Caml. The system supports a rich input language
+ allowing descriptions of complex mathematical structures. RZ does
+ not extract code from proofs, but allows any implementation
+ method, from handwritten code to code extracted from proofs by
+ other tools.",
+ paper = "Baue07.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Bauer, Andrej}
\begin{chunk}{axiom.bib}
@misc{Baue19,
author = "Bauer, Andrej",
@@ 14141,6 +14251,39 @@ when shown in factored form.
\end{chunk}
+\index{van Benthem Jutting, L.S.}
+\index{McKinna, J.}
+\index{Pollack, R.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Bent93,
+ author = "van Benthem Jutting, L.S. and McKinna, J. and Pollack, R.",
+ title = {{Checking Algorithms for Pure Type Systems}},
+ booktitle = "Types for Proofs and Programs",
+ publisher = "Springer",
+ year = "1993",
+ pages = "1961",
+ abstract =
+ "This work is motivated by the problem of finding reasonable
+ algorithms for typechecking Pure Type Systems [Bar91] (PTS). There
+ are several implementations of formal systems that are either PTS
+ or closely related to PTS. For example, LEGO [LP92] implements the
+ Pure Calculus of Constructions (PCC) [CH88], the Extended Calculus
+ of Constructions [Luo90] and the Edinburgh Logical Framework (LF)
+ [HHP87]. ELF [Pfe89] implements LF; CONSTRUCTOR [Hel91] implements
+ arbitrary PTS with finite set of sorts. Are these implementations
+ actually correct? Of course, we may enumerate all derivations of a
+ given PTS, and Jutting [vBJ93] has shown that a large class of
+ normalizing PTS have decidable typechecking by computing the
+ normal forms of types, but such techniques are obviously not
+ usable in practice. Algorithms in the literature for particular
+ type systems, such as Huet's Constructive Engine [Hue89], do not
+ obviously extend even to such tame classes as the normalizing and
+ functional PTS.",
+ paper = "Bent93.pdf"
+}
+
+\end{chunk}
+
\index{Berger, U.}
\index{Schwichtenberg, H.}
\begin{chunk}{axiom.bib}
@@ 14433,7 +14576,8 @@ when shown in factored form.
publisher = "Clarendon Press",
year = "1997",
isbn = "0198751419",
 paper = "Bost97.pdf"
+ paper = "Bost97.pdf",
+ keywords = "shelf"
}
\end{chunk}
@@ 14452,7 +14596,7 @@ when shown in factored form.
abstract =
"Elaborationbased type class resolution, as found in languages
like Haskell, Mercury and PureScript, is generally
 {\ls nondeterministic}: there can be multiple ways to satisfy a
+ {\sl nondeterministic}: there can be multiple ways to satisfy a
wanted constraint in terms of global instances and locally given
constraints. Coherence is the key property that keeps this sane;
it guarantees that, despite the nondeterminism, programs will
@@ 14671,6 +14815,19 @@ when shown in factored form.
\end{chunk}
+\index{Brady, Edwin}
+\begin{chunk}{axiom.bib}
+@book{Brad17a,
+ author = "Brady, Edwin",
+ title = {{TypeDriven Development with IDRIS}},
+ publisher = "Manning Publications",
+ year = "2017",
+ isbn = "9781617293023",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
\index{Bradford, R.J.}
\index{Davenport, J.H.}
\begin{chunk}{axiom.bib}
@@ 14949,6 +15106,23 @@ when shown in factored form.
\end{chunk}
+\index{Brown, Chad E.}
+\index{Gauthier, Thibault}
+\begin{chunk}{axiom.bib}
+@misc{Brow19,
+ author = "Brown, Chad E. and Gauthier, Thibault",
+ title = {{SelfLearned Formula Synthesis in Set Theory}},
+ year = "2019",
+ link = "\url{https://arxiv.org/pdf/1912.01525.pdf}",
+ abstract =
+ "A reinforcement learning algorithm accomplishes the task of
+ synthesizing a settheoretical formula that evaluates to a given
+ truth value for given assignments.",
+ paper = "Brow19.pdf"
+}
+
+\end{chunk}
+
\index{Burstall, R.M.}
\begin{chunk}{axiom.bib}
@article{Burs69,
@@ 15476,6 +15650,19 @@ when shown in factored form.
\end{chunk}
+\index{Carter, Nathan}
+\begin{chunk}{axiom.bib}
+@book{Cart09,
+ author = "Carter, Nathan",
+ title = {{Visual Group Theory}},
+ publisher = "Mathematical Association of America",
+ year = "2009",
+ isbn = "9780883857571",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
\index{Cervesato, Iliano}
\index{Pfenning, Frank}
\begin{chunk}{axiom.bib}
@@ 15790,7 +15977,7 @@ when shown in factored form.
propose a construction of a dictionary between automated theorem
provers and (La)Tex exploiting syntactic parsers. We describe its
application to a repository of humanwritten facts and definitions
 in algebraic geometry (The Stacks Project). We use deep learing
+ in algebraic geometry (The Stacks Project). We use deep learning
techniques.",
paper = "Choj17.pdf"
}
@@ 15942,7 +16129,8 @@ when shown in factored form.
title = {{Logic Programming}},
publisher = "Academic Press",
year = "1982",
 isbn = "0121755207"
+ isbn = "0121755207",
+ keywords = "shelf"
}
\end{chunk}
@@ 16248,7 +16436,8 @@ when shown in factored form.
title = {{The Essential Turing}},
publisher = "Oxford University Press",
year = "2004",
 isbn = "9780198250807"
+ isbn = "9780198250807",
+ keywords = "shelf"
}
\end{chunk}
@@ 16333,6 +16522,87 @@ when shown in factored form.
\end{chunk}
+\index{Crouse, Maxwell}
+\index{Whitehead, Spencer}
+\index{Abdelaziz, Ibrahim}
+\index{Makni, Bassem}
+\index{Cornelio, Cristina}
+\index{Kapanipathi, Pavan}
+\index{Pell, Edwin}
+\index{Srinivas, Kavitha}
+\index{Thost, Veronika}
+\index{Witbrock, Michael}
+\index{Fokoue, Achille}
+\begin{chunk}{axiom.bib}
+@misc{Crou19,
+ author = "Crouse, Maxwell and Whitehead, Spencer and
+ Abdelaziz, Ibrahim and Makni, Bassem and
+ Cornelio, Cristina and Kapanipathi, Pavan and
+ Pell, Edwin and Srinivas, Kavitha and
+ Thost, Veronika and Witbrock, Michael and
+ Fokoue, Achille",
+ title = {{A Deep Reinforcement Learning Base Approach to Learning
+ Transferable Proof Guidance Strategies}},
+ year = "2019",
+ linke = "\url{https://arxiv.org/pdf/1911.02065.pdf}",
+ abstract =
+ "Traditional firstorder logic (FOL) reasoning systems usually
+ rely on manual heuristics for proof guidance. We propose TRAIL: a
+ system that learns to perform proof guidance using reinforcement
+ learning. A key design principle of our system is that it is
+ general enough to allow transfer to problems in different domains
+ that do not share the same vocabulary of the training set. To do
+ so, we developed a novel representation of the internal state of a
+ prover in terms of clauses and inference actions, and a novel
+ neuralbased attention mechanism to learn interactions between
+ clauses. We demonstrate that this approach enables the system to
+ generalize from training to test data across domains with
+ different vocabularies, suggesting that the nerual architecture in
+ TRAIL is well suited for representing and processing of logical
+ formalisms.",
+ paper = "Crou19.pdf"
+}
+
+\end{chunk}
+
+\index{Crouse, Maxwell}
+\index{Abdelaziz, Ibrahim}
+\index{Cornelio, Cristina}
+\index{Thost, Veronika}
+\index{Wu, Lingfei}
+\index{Forbus, Kenneth}
+\index{Fokoue, Achille}
+\begin{chunk}{axiom.bib}
+@misc{Crou19a,
+ author = "Crouse, Maxwell and Abdelaziz, Ibrahim and
+ Cornelio, Cristina and Thost, Veronika and
+ Wu, Lingfei and Forbus, Kenneth and Fokoue, Achille",
+ title = {{Improving Graph Neural Network Representations of Logical
+ Formulae with Subgraph Pooling}},
+ year = "2019",
+ linke = "\url{https://arxiv.org/pdf/1911.06904.pdf}",
+ abstract =
+ "Recent advances in the integration of deep learning with
+ automated theorem proving have centered around the representation
+ of graphstructured representations, in large part driven by the
+ rapidly emerging body of research in geometric deep
+ learning. Typically, structureaware neural methods for embedding
+ logical formulae have been variants of either Tree LSTMs or
+ GNNs. While more effective than character and tokenlevel
+ approaches, such methods have often made representational
+ tradeoffs that limited their ability to effectively represent the
+ global structure of their inputs. In this work, we introduce a
+ novel approach for embedding logical formulae using DAG LSTMs that
+ is designed to overome the limitations of both Tree LSTMs and
+ GNNs. The effectiveness of the proposed framework is demonstrated
+ on the tasks of premise selection and proof step classification
+ where it achieves the stateoftheart performance on two standard
+ datasets.",
+ paper = "Crou19a.pdf"
+}
+
+\end{chunk}
+
\index{Cutland, Nigel}
\begin{chunk}{axiom.bib}
@book{Cutl80,
@@ 16348,6 +16618,20 @@ when shown in factored form.
\subsection{D} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Daepp, Ulrich}
+\index{Gorkin, Pamela}
+\begin{chunk}{axiom.bib}
+@book{Daep11,
+ author = "Daepp, Ulrich and Gorkin, Pamela",
+ title = {{Reading, Writing, and Proving}},
+ year = "2011",
+ publisher = "Springer",
+ isbn = "9781441994783",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
\index{Dahl, O.J.}
\index{Dijkstra, E.W.}
\index{Hoare, C.A.R}
@@ 16448,7 +16732,6 @@ when shown in factored form.
pages = "347362",
year = "1992",
publisher = "Academic Press",

abstract =
"Historically symbolic and numeric computation have pursued
different lines of evolution, have been written in different
@@ 16843,7 +17126,8 @@ when shown in factored form.
title = {{Predicate Calculus and Program Semantics}},
publisher = "Springer",
year = "1990",
 isbn = "0387969578"
+ isbn = "0387969578",
+ keywords = "shelf"
}
\end{chunk}
@@ 16943,6 +17227,22 @@ when shown in factored form.
\end{chunk}
+\index{Donald, B.R.}
+\index{Kapur, D.}
+\index{Mundy, J.L.}
+\begin{chunk}{axiom.bib}
+@book{Dona92,
+ author = "Donald, B.R. and Kapur, D. and Mundy, J.L.",
+ title = {{Symbolic and Numerical Computation for Artificial
+ Intelligence}},
+ publisher = "Academic Press Limited",
+ year = "1992",
+ isbn = "0 12 220535 9",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
\index{Dowek, Gilles}
\begin{chunk}{axiom.bib}
@inbook{Dowe01,
@@ 17518,6 +17818,20 @@ when shown in factored form.
\end{chunk}
+\index{Feynman, Richard}
+\index{Hey, Anthony J.G.}
+\begin{chunk}{axiom.bib}
+@book{Feyn02,
+ author = "Feynman, Richard and Hey, Anthony J.G.",
+ title = {{Feynman and Computation}},
+ publisher = "Westview Press",
+ year = "2002",
+ isbn = "081334039X",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
\index{Fieker, Claus}
\index{Hart, William}
\index{Hofmann, Tommy}
@@ 17639,6 +17953,78 @@ when shown in factored form.
\end{chunk}
+\index{Friedman, Daniel P.}
+\index{Felleisen, Matthias}
+\begin{chunk}{axiom.bib}
+@book{Frie96,
+ author = "Friedman, Daniel P. and Felleisen, Matthias",
+ title = {{The Seasoned Schemer}},
+ publisher = "MIT Press",
+ year = "1996",
+ isbn = "026256100X",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
+\index{Friedman, Daniel P.}
+\index{Felleisen, Matthias}
+\begin{chunk}{axiom.bib}
+@book{Frie99,
+ author = "Friedman, Daniel P. and Felleisen, Matthias",
+ title = {{The Little Schemer}},
+ publisher = "MIT Press",
+ year = "1999",
+ isbn = "0262560992",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
+\index{Friedman, Daniel P.}
+\index{Byrd, William E.}
+\index{Kiselyov, Oleg}
+\begin{chunk}{axiom.bib}
+@book{Frie05,
+ author = "Friedman, Daniel P. and Byrd, William E. and
+ Kiselyov, Oleg",
+ title = {{The Reasoned Schemer}},
+ publisher = "MIT Press",
+ year = "2005",
+ isbn = "0262562146",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
+\index{Friedman, Daniel P.}
+\index{Eastland, Carl}
+\begin{chunk}{axiom.bib}
+@book{Frie15,
+ author = "Friedman, Daniel P. and Eastland, Carl",
+ title = {{The Little Prover}},
+ publisher = "The MIT Press",
+ year = "2015",
+ isbn = "9780262527958",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
+\index{Friedman, Daniel P.}
+\index{Christiansen, David Thrane}
+\begin{chunk}{axiom.bib}
+@book{Frie18,
+ author = "Friedman, Daniel P. and Christiansen, David Thrane",
+ title = {{The Little Typer}},
+ publisher = "The MIT Press",
+ year = "2018",
+ isbn = "9780262536431",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
\subsection{G} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Gabriel, Richard P.}
@@ 17803,6 +18189,33 @@ when shown in factored form.
\end{chunk}
+\index{Gauthier, Thibault}
+\begin{chunk}{axiom.bib}
+@misc{Gaut19,
+ author = "Gauthier, Thibault",
+ title = {{Deep Reinforcement Learning in HOL4}},
+ year = "2019",
+ link = "\url{https://arxiv.org/pdf/1910.11797.pdf}",
+ abstract =
+ "The paper describes an implementation of deep reinforcement
+ learning through selfsupervised learning within the proof
+ assistant HOL4. A close interaction between the machine learning
+ modules and the HOL4 library is achieved by the choice of tree
+ neural networks (TNNs) as machine learning models and the internal
+ use of HOL4 terms to represent tree structures of TNNs. Recursive
+ improvement is possible when a given task is expressed as a search
+ problem. In this case, a Monte Carlo Tree Search (MCTS) algorithm
+ guided by a TNN can be used to explore the search space and
+ produce better examples for training the next TNN. As an
+ illustration, tasks over propositional and arithmetical terms,
+ representative of fundamental theorem proving techniques, are
+ specified and learned: truth estimation, endtoend computation,
+ term rewriting and term synthesis.",
+ paper = "Gaut19.pdf"
+}
+
+\end{chunk}
+
\index{Geddes, Keith O.}
\index{Gonnet, Gaston H.}
\index{Smedley, Trevor J.}
@@ 18006,6 +18419,21 @@ when shown in factored form.
\end{chunk}
+\index{Girard, JeanYves}
+\index{Lafont, Yves}
+\index{Regnier, Laurent}
+\begin{chunk}{axiom.bib}
+@book{Gira95a,
+ author = "Girard, JeanYves and Lafont, Yves and Regnier, Laurent",
+ title = {{Advances in Linear Logic}},
+ publisher = "Cambridge University Press",
+ year = "1995",
+ isbn = "0521559618",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
\index{Gleich, David}
\begin{chunk}{axiom.bib}
@misc{Glei05,
@@ 18044,6 +18472,20 @@ when shown in factored form.
\end{chunk}
+\index{Goguen, Joseph A.}
+\index{Malolm, Grant}
+\begin{chunk}{axiom.bib}
+@book{Gogu96,
+ author = "Goguen, Joseph A. and Malolm, Grant",
+ title = {{Algebraic Semantics of Imperative Programs}},
+ publisher = "MIT Press",
+ year = "1996",
+ isbn = "026207172X",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
\index{Goldblatt, Robert}
\begin{chunk}{axiom.bib}
@book{Gold84,
@@ 18056,6 +18498,19 @@ when shown in factored form.
\end{chunk}
+\index{Goldstein, Rebecca}
+\begin{chunk}{axiom.bib}
+@book{Gold05,
+ author = "Goldstein, Rebecca",
+ title = {{Incompleteness}},
+ publisher = "Atlas Books",
+ year = "2005",
+ isbn = "0393327604",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
\index{Gonthier, Goerges}
\index{Mahboubi, Assia}
\index{Rideau, Laurence}
@@ 18150,6 +18605,22 @@ when shown in factored form.
\index{Milner, Arthur J.}
\index{Wadsworth, Christopher P.}
\begin{chunk}{axiom.bib}
+@book{Gord79f,
+ author = "Gordon, Michael J. and Milner, Arthur J. and
+ Wadsworth, Christopher P.",
+ title = {{Edinburgh LCF}},
+ publisher = "SpringerVerlag",
+ year = "1979",
+ isbn = "3540097244",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
+\index{Gordon, Michael J.}
+\index{Milner, Arthur J.}
+\index{Wadsworth, Christopher P.}
+\begin{chunk}{axiom.bib}
@incollection{Gord79a,
author = "Gordon, Michael J. and Milner, Arthur J. and
Wadsworth, Christopher P.",
@@ 18236,6 +18707,39 @@ when shown in factored form.
\end{chunk}
+\index{Gordon, M.J.C}
+\begin{chunk}{axiom.bib}
+@article{Gord15,
+ author = "Gordon, M.J.C",
+ title = {{Tactics for Mechanized Reasoning: A Commentary on Milner
+ (1984) 'The Use of Machines to Assist in Rigorous Proof'}},
+ journal = "Philosophical Transactions: Mathematical, Physical and
+ Engineering Sciences",
+ volume = "373",
+ number = "2039",
+ pages = "111",
+ year = "2015",
+ abstract =
+ "Robin Milner's paper, ``The use of machines to assist in rigorous
+ proof'', introduces methods for automating mathematical reasoning
+ that are a milestone in the development of computerassisted
+ theorem proving. His ideas, particularly his theory of tactics,
+ revolutionized the architecture of proof assistants. His
+ methodology for automating rigorous proof soundly, particularly
+ his theory of type polymorphism in programming, led to major
+ contributions to the theory and design of programming
+ languages. His citation for the 1991 ACM A.M. Turing award, the
+ most prestigious award in computer science, credits him with,
+ among other achievements, 'probably the first theoretically based
+ yet practical tool for machine assisted proof construction'. This
+ commentary was written to celebrate the 350th anniversary of the
+ journal {\sl Philosophical Transactions of the Royal Society}.",
+ paper = "Gord15.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Goto, Kazushige}
\index{van de Geijn, Robert A.}
\begin{chunk}{axiom.bib}
@@ 18557,7 +19061,8 @@ when shown in factored form.
title = {{Book of Proof}},
publisher = "Hammack, Richard",
year = "2018",
 paper = "Hamm18.pdf"
+ paper = "Hamm18.pdf",
+ keywords = "shelf"
}
\end{chunk}
@@ 18681,7 +19186,8 @@ when shown in factored form.
title = {{Practical Foundations for Progamming Languages}},
publisher = "Cambridge University Press",
year = "2016",
 isbn = "9781107150300"
+ isbn = "9781107150300",
+ keywords = "shelf"
}
\end{chunk}
@@ 19406,6 +19912,20 @@ when shown in factored form.
\end{chunk}
+\index{Hoare, C.A.R}
+\index{Shepherdson, J.C.}
+\begin{chunk}{axiom.bib}
+@book{Hoar85,
+ author = "Hoare, C.A.R and Shepherdson, J.C.",
+ title = {{Mathematical Logic and Programming Languages}},
+ year = "1985",
+ publisher = "PrenticeHall",
+ isbn = "0135614651",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
\index{Holzl, Johannes}
\index{Heller, Armin}
\begin{chunk}{axiom.bib}
@@ 19868,7 +20388,7 @@ when shown in factored form.
publisher = "SpringerVerlag",
year = "1975",
isbn = "0387901442",
 keywords = "owned"
+ keywords = "shelf"
}
\end{chunk}
@@ 20148,6 +20668,18 @@ when shown in factored form.
\end{chunk}
+\index{Kalorkoti, K.}
+\begin{chunk}{axiom.bib}
+@misc{Kalo18,
+ author = "Kalorkoti, K.",
+ title = {{Introduction to Computer Algebra}},
+ comment = "Course Notes",
+ year = "2018",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
\index{Kamareddine, Fairouz}
\index{Laan, Twan}
\index{Nederpelt, Rob}
@@ 20204,6 +20736,36 @@ when shown in factored form.
\end{chunk}
+\index{Kay, Alan}
+\begin{chunk}{axiom.bib}
+@misc{Kayx19,
+ author = "Kay, Alan",
+ title = {{Alan Kay Speaks at ATLAS Institute}},
+ year = "2019",
+ link = "\url{https://www.youtube.com/watch?v=nOrdzDaPYV4}"
+}
+
+\end{chunk}
+
+\index{Keenen, David C.}
+\begin{chunk}{axiom.bib}
+@misc{Keen14,
+ author = "Keenen, David C.",
+ title = {{To Dissect a Mockingbird: A Graphical Notation for the
+ Lambda Calculus with Animated Reduction}},
+ year = "2014",
+ link = "\url{http://dkeenan.com/Lambda}",
+ abstract =
+ "The lambda calculus, and the closely related theory of
+ combinators, are important in the foundations of mathematics,
+ logic and computer science. This paper provides an informal and
+ entertaining introduction by means of an animated graphical
+ notation.",
+ keywords = "printed, DONE"
+}
+
+\end{chunk}
+
\index{Kerber, Manfred}
\begin{chunk}{axiom.bib}
@article{Kerb10,
@@ 20237,7 +20799,8 @@ when shown in factored form.
title = {{The Art of the Metaobject Protocol}},
publisher = "MIT Press",
year = "1991",
 isbn = "0262610744"
+ isbn = "0262610744",
+ keywords = "shelf"
}
\end{chunk}
@@ 20317,12 +20880,12 @@ when shown in factored form.
\end{chunk}
\index{Knuth, Donal E.}
+\index{Knuth, Donald E.}
\index{Larrabee, Tracy}
\index{Roberts, Paul M.}
\begin{chunk}{axiom.bib}
@misc{Knut87,
 author = "Knuth, Donal E. and Larrabee, Tracy and Roberts, Paul M.",
+ author = "Knuth, Donald E. and Larrabee, Tracy and Roberts, Paul M.",
title = {{Mathematical Writing}},
year = "1987",
link = "\url{jmlr.csail.mit.edu/reviewingpapers/knuth_mathematical_writing.pdf}"
@@ 20330,6 +20893,19 @@ when shown in factored form.
\end{chunk}
+\index{Knuth, Donald E.}
+\begin{chunk}{axiom.bib}
+@misc{Knut19,
+ author = "Knuth, Donald E.",
+ title = {{Donald Knuth: Algorithms, Complexity, Life, and The Art of
+ Computer Programmig}},
+ link = "\url{https://www.youtube.com/watch?v=2Bd8fsXbST8}",
+ year = "2019",
+ comment = "Lex Fridman AI Podcast"
+}
+
+\end{chunk}
+
\index{Kohlhase, Michael}
\index{Muller, Christine}
\index{Rabe, Florian}
@@ 20665,6 +21241,31 @@ when shown in factored form.
\end{chunk}
+\index{Lample, Guillaume}
+\index{Charton, Francois}
+\begin{chunk}{axiom.bib}
+@misc{Lamp19,
+ author = "Lample, Guillaume and Charton, Francois",
+ title = {{Deep Learning for Symbolic Mathematics}},
+ year = "2019",
+ link = "\url{https://arxiv.org/pdf/1912.01412.pdf}",
+ abstract =
+ "Neural networks have a reputation for being better at solving
+ statistical or approximate problems than at performing
+ calculations or working with symbolic data. In this paper, we show
+ that they can be surprisingly good at more elaborated tasks in
+ mathematics, such as symbolic integration and solving differential
+ equations. We propose a syntax for representing mathematical
+ problems, and methods for generating large datasets that can be
+ used to train sequencetosequence models. We achieve results that
+ outperform commercial Computer Algebra Systems such as Matlab or
+ Mathematica.",
+ paper = "Lamp19.pdf",
+ keywords = "printed, DONE"
+}
+
+\end{chunk}
+
\index{Lamport, Leslie}
\index{Paulson, Lawrence C.}
\begin{chunk}{axiom.bib}
@@ 20700,6 +21301,40 @@ when shown in factored form.
\end{chunk}
+\index{Landin, P.J.}
+\begin{chunk}{axiom.bib}
+@article{Land66,
+ author = "Landin, P.J.",
+ title = {{The Next 700 Programming Languages}},
+ journal = "Communications of the ACM",
+ volume = "9",
+ pages = "157166",
+ year = "1966",
+ abstract =
+ "A family of unimplemented computing languages is described that
+ is intended to span differences of application areas by a unified
+ framework. This framework dictates the rules about the uses of
+ usercoined names, and the conventions about characterizing
+ functional relationships. Within this framework the design of a
+ specific language splits into two independent parts. One is the
+ choice of written appearances of programs (or more generally,
+ their physical representation). The other is the choice of the
+ abstract entities (such as numbers, characterstrings, lists of
+ them, functional relations among them) that can be referred to in
+ the language.
+
+ The system is biased towards ``expressions'' rather than
+ ``statements''. It includes a nonprocedural (purely functional)
+ subsystem that aims to expand the class of users' needs that can
+ be met by a single printinstruction, without sacrificing the
+ important properties that make conventional righthandside
+ expressions easy to construct and understand.",
+ paper = "Land66.pdf",
+ keywords = "DONE"
+}
+
+\end{chunk}
+
\begin{chunk}{axiom.bib}
@misc{Lean19,
author = "Lean",
@@ 20880,6 +21515,25 @@ when shown in factored form.
\end{chunk}
+\index{Loh, PoShen}
+\begin{chunk}{axiom.bib}
+@misc{Lohx19,
+ author = "Loh, PoShen",
+ title = {{A Simple Proof of the Quadratic Formula}},
+ year = "2019",
+ link = "\url{https://arxiv.org/pdf/1910.06709.pdf}",
+ abstract =
+ "This aarticle provides a simple proof of the quadratic formula,
+ which also produces an efficient and natural method for solving
+ general quadratic equations. The derivation is computationally
+ light and conceptually natural, and has the potential to demystify
+ quadratic equations for students worldwide.",
+ paper = "Lohx19.pdf",
+ keywords = "DONE"
+}
+
+\end{chunk}
+
\index{Lou, Zhaohui}
\begin{chunk}{axiom.bib}
@phdthesis{Loux90,
@@ 20995,6 +21649,22 @@ when shown in factored form.
\end{chunk}
+\index{Luckham, D.C.}
+\index{Park, D.M.R}
+\index{Paterson, M.S.}
+\begin{chunk}{axiom.bib}
+@article{Luck70,
+ author = "Luckham, D.C. and Park, D.M.R and Paterson, M.S.",
+ title = {{On Formalised Computer Programs}},
+ journal = "J. of Computer and System Sciences",
+ volume = "4",
+ pages = "220249",
+ year = "1970",
+ paper = "Luck70.pdf"
+}
+
+\end{chunk}
+
\index{Luther, Marko}
\index{Strecker, Martin}
\begin{chunk}{axiom.bib}
@@ 21187,6 +21857,34 @@ when shown in factored form.
\end{chunk}
+\index{Manna, Zohar}
+\begin{chunk}{axiom.bib}
+@phdthesis{Mann68,
+ author = "Manna, Zohar",
+ title = {{Termination of Algorithms}},
+ school = "Carnegie Mellon University",
+ year = "1968",
+ link = "\url{http://apps/dtic.mil/dtic/tr/fulltext/u2/670558.pdf}",
+ abstract =
+ "The thesis contains two parts which are selfcontained units.
+
+ In Part I we present several results on the relation between
+ \begin{enumerate}
+ \item the problem of termination and equivalence of programs and
+ abstract programs, and
+ \item the first order predicate calculus
+ \end{enumerate}
+
+ Part II is concerned with the relation between
+ \begin{enumerate}
+ \item the termination of interpreted graphs, and
+ \item properties of wellordered sets and graph theory
+ \end{enumerate}",
+ paper = "Mann68.pdf"
+}
+
+\end{chunk}
+
\index{MartinL\"of, P.}
\begin{chunk}{axiom.bib}
@article{Mart84,
@@ 21234,6 +21932,37 @@ when shown in factored form.
\end{chunk}
+\index{McCarthy, J.}
+\begin{chunk}{axiom.bib}
+@misc{Mcca60a,
+ author = "McCarthy, J.",
+ title = {{Programs with Common Sense}},
+ year = "1960",
+ abstract =
+ "Interesting work is being done in programming computers to solve
+ problems which require a high degree of intelligence in
+ humans. However, certain elementary verbal reasoning processes so
+ simple that they can be carried out by any nonfeebleminded human
+ have yet to be simulated by machine programs.
+
+ This paper will discuss programs to manipulate in a suitable
+ formal language (most likely a part of the predicate calculus)
+ common instrumental statements. The basic program will draw
+ immediate conclusions from a list of premises. These conclusions
+ will be either declarative or imperative sentences. When an
+ imperative sentence is deduced the program takes a corresponding
+ action. These actions may include printing sentences, moving
+ sentences on lists, and reinitiating the basic deduction process
+ on these lists.
+
+ Facilities will be provided for communication with humans in the
+ system via manual intervention and display devices connected to
+ the computer.",
+ paper = "Mcca60a.pdf"
+}
+
+\end{chunk}
+
\index{Mhamdi, Tarek}
\index{Hasan, Osman}
\index{Tahar, Sofiene}
@@ 21249,6 +21978,19 @@ when shown in factored form.
\end{chunk}
+\index{Monin, JeanFrancois}
+\begin{chunk}{axiom.bib}
+@book{Moni03,
+ author = "Monin, JeanFrancois",
+ title = {{Understanding Formal Methods}},
+ publisher = "Springer",
+ year = "2003",
+ isbn = "1852332476",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
\index{de Moura, Leonardo}
\index{Avigad, Jeremy}
\index{Kong, Soonho}
@@ 21418,7 +22160,8 @@ when shown in factored form.
title = {{Theoretical Introduction to Programming}},
publisher = "Springer",
year = "2006",
 isbn = "1846280214"
+ isbn = "1846280214",
+ keywords = "shelf"
}
\end{chunk}
@@ 21799,6 +22542,20 @@ when shown in factored form.
\subsection{N} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Nagel, Ernest}
+\index{Newman, James R.}
+\begin{chunk}{axiom.bib}
+@book{Nage01,
+ author = "Nagel, Ernest and Newman, James R.",
+ title = {{Godel's Proof}},
+ publisher = "New York University Press",
+ year = "2001",
+ isbn = "0814758169",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
\index{Nathanson, Melvyn B.}
\begin{chunk}{axiom.bib}
@article{Nath08,
@@ 22204,6 +22961,45 @@ when shown in factored form.
\end{chunk}
+\index{Olsak, Miroslav}
+\index{Kaliszyk, Cezary}
+\index{Urban, Josef}
+\begin{chunk}{axiom.bib}
+@misc{Olsa19,
+ author = "Olsak, Miroslav and Kaliszyk, Cezary and Urban, Josef",
+ title = {{Property Invariant Embedding for Automated Reasoning}},
+ year = "2019",
+ link = "\url{https://arxiv.org/pdf/1911.12073.pdf}",
+ abstract =
+ "Automated reasoning and theorem proving have recently become
+ major challenges for machine learning. In other domains,
+ representations that are able to abstract over unimportant
+ transformations, such as abstraction over translations and
+ rotations in vision, are becoming more common. Standard methods of
+ embedding mathematical formulas for learning theorem proving are
+ however yet unable to handle many important transformations. In
+ particular, embedding previously unseen labels, that often arise
+ in definitional encodings and in Skolemizatin, has been very weak
+ so far. Similar problems appear when tranferring knowledge between
+ known symbols.
+
+ We propose a novel encoding of formulas that extends existing
+ graph neural network models. This encoding represents symbols only
+ by nodes in the graph, without giving the network any knowledge of
+ the original labels. We provide additional links between such
+ nodes that allow the network to recover the meaning and therefore
+ correctly embed such nodes irrespective of the given labels. We
+ test the proposed encoding in an automated theorem prover based on
+ the tableaux connection calculus, and show that it improves on the
+ best characterizations used so far. The encoding is further
+ evaluated on the premise selection task and a newly introduced
+ symbol guessing task, and shown to correctly predict 65\% of the
+ symbol names.",
+ paper = "Olsa19.pdf"
+}
+
+\end{chunk}
+
\index{Olsson, Ola}
\index{Wallenburg, Angela}
\begin{chunk}{axiom.bib}
@@ 22432,6 +23228,7 @@ when shown in factored form.
author = "Patterson, Daniel and Ahmed, Amal",
title = {{The Next 700 Compiler Correctness Theorems}},
booktitle = "Inter. Conf. on Functional Programming",
+ link = "\url{https://www.youtube.com/watch?v=qrwzpo6ISCQ}",
publisher = "ACM",
year = "2019",
abstract =
@@ 22478,6 +23275,31 @@ when shown in factored form.
\end{chunk}
+\index{Perrone, Paolo}
+\begin{chunk}{axiom.bib}
+@misc{Perr19,
+ author = "Perrone, Paolo",
+ title = {{Notes on Category Theory}},
+ year = "2019",
+ link = "\url{https://arxiv.org/pdf/1912.10642.pdf}",
+ paper = "Perr19.pdf"
+}
+
+\end{chunk}
+
+\index{Petzold, Charles}
+\begin{chunk}{axiom.bib}
+@book{Petz08,
+ author = "Petzold, Charles",
+ title = {{The Annotated Turing}},
+ publisher = "Wiley",
+ year = "2008",
+ isbn = "9780470229057",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
\index{Pfenning, Frank}
\begin{chunk}{axiom.bib}
@misc{Pfen06,
@@ 22503,6 +23325,30 @@ when shown in factored form.
\end{chunk}
+\index{Piotrowski, Bartosz}
+\index{Brown, Chad E.}
+\index{Kaliszyk, Cezary}
+\begin{chunk}{axiom.bib}
+@misc{Piot19,
+ author = "Piotrowski, Bartosz and Brown, Chad E. and
+ Kaliszyk, Cezary",
+ title = {{Can Neural Networks Learn Symbolic Rewriting?}},
+ year = "2019",
+ link = "\url{https://arxiv.org/pdf/1911.04783.pdf}",
+ abstract =
+ "This work investigates if the current neural architectures are
+ adequate for learning symbolic rewriting. Two kinds of data sets
+ are proposed for this research  one based on automated proofs
+ and the other being a synthetic set of polynomial terms. The
+ experiments with use of the current neural machine translation
+ models are performed and its results are discussed. Ideas for
+ extending this line of research are proposed and its relevance is
+ motivated.",
+ paper = "Piot19.pdf"
+}
+
+\end{chunk}
+
\index{Pirog, Maciej}
\index{Gibbons, Jeremy}
\begin{chunk}{axiom.bib}
@@ 22583,7 +23429,8 @@ when shown in factored form.
title = {{Logical Foundations of CyberPhysical Systems}},
publisher = "Springer",
year = "2018",
 isbn = "9783319635873"
+ isbn = "9783319635873",
+ keywords = "shelf"
}
\end{chunk}
@@ 22736,6 +23583,19 @@ when shown in factored form.
\end{chunk}
+\index{Queinnec, Christian}
+\begin{chunk}{axiom.bib}
+@book{Quei94,
+ author = "Queinnec, Christian",
+ title = {{Lisp In Small Pieces}},
+ publisher = "Cambridge University Press",
+ year = "1994",
+ isbn = "0521545668",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
\subsection{R} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Rabe, Florian}
@@ 22856,6 +23716,20 @@ when shown in factored form.
\end{chunk}
+\index{Ranta, Aarne}
+\begin{chunk}{axiom.bib}
+@inproceedings{Rant93,
+ author = "Ranta, Aarne",
+ title = {{Type Theory and the Informal Language of Mathematics}},
+ booktitle = "Types for Proofs and Programs",
+ publisher = "Springer",
+ year = "1993",
+ pages = "352365",
+ paper = "Rant93.pdf"
+}
+
+\end{chunk}
+
\index{Raskovsky, Martin}
\index{Collier, Phil}
\begin{chunk}{axiom.bib}
@@ 23232,7 +24106,8 @@ when shown in factored form.
author = "Russell, Bertrand",
title = {{Introduction to Mathematical Philosophy}},
publisher = "George Allen and Unwin, Ltd",
 year = "1920"
+ year = "1920",
+ keywords = "shelf"
}
\end{chunk}
@@ 23705,6 +24580,39 @@ when shown in factored form.
\end{chunk}
+\index{Scott, Dana}
+\index{Strachey, Christopher}
+\begin{chunk}{axiom.bib}
+@misc{Scot92,
+ author = "Scott, Dana and Strachey, Christopher",
+ title = {{Toward a Mathematical Semantics for Computer Languages}},
+ year = "1992",
+ comment = "Oxford Programming Research Group Monograph PRG6",
+ abstract =
+ "Compilers for highlevel languages are generally constructed to
+ give the complete translation of the programs into machine
+ language. As machines merely juggle bit patterns, the concepts of
+ the original language may be lost or at least obscured during this
+ passage. The purpose of a mathematical semantics is to give a
+ correct and meaningful correspondence between programs and
+ mathematical entities in a way that is entirely independent of an
+ implementation. This plan is illustrated in a very elementary way
+ in the introduction. The first section connects the general method
+ with the usual idea of state transformations. The next section
+ shows why the mathematics of functions has to be modified to
+ accommodate recursive commands. Section 3 explains the
+ modification. Section 4 introduces the environments for handling
+ variables and identifiers and shows how the semantical equations
+ define equivalence of programs. Section 5 gives an exposition of
+ the new type of mathematical function spaces that are required for
+ the semantics of procedures when these are allowed in
+ assignments. The conclusion traces some of the background of the
+ project and points the way to future work.",
+ paper = "Scot92.pdf"
+}
+
+\end{chunk}
+
\index{Selsam, Daniel}
\begin{chunk}{axiom.bib}
@misc{Sels19,
@@ 23968,6 +24876,54 @@ when shown in factored form.
\end{chunk}
+\index{Sozeau, Matthieu}
+\index{Boulier, Simon}
+\index{Forster, Yannick}
+\index{Tabareau, Nicolas}
+\index{Winterhalter, Theo}
+\begin{chunk}{axiom.bib}
+@misc{Soze19,
+ author = "Sozeau, Matthieu and Boulier, Simon and Forster, Yannick
+ and Tabareau, Nicolas and Winterhalter, Theo",
+ title = {{Coq Coq Correct!}},
+ year = "2019",
+ link = "\url{https://www.irif.fr/~sozeau/research/publications/drafts/Coq_Coq_Correct.pdf}",
+ abstract =
+ "Coq is built around a welldelimited kernel that performs
+ typechecking for definitions in a variant of the Calculus of
+ Inductive Constructions (CIC). Although the metatheory of CIC is
+ very stable and reliable, the correctness of its implementation in
+ Coq is less clear. Indeed, implementing an efficient type checker
+ for CIC is a rather complex task, and many parts of the code rely
+ on implicit invariants which can easily be broken by further
+ evolution of the code. Therefore, on average, one critical bug has
+ been found every year in Coq. This paper presents the first
+ implementation of a type checker for the kernel of Coq, which is
+ proven correct in Coq with respect to its formal
+ specification. Note that because of Godel's incompleteness
+ theorem, there is no hope to prove completely the correctness of
+ the specification of Coq inside Coq (in particular strong
+ normalisation or canonicity), but it is possible to prove the
+ correctness of the implementation assuming the correctness of the
+ specification. Our work is based on the METACOQ project [Anand et
+ al. 2018; Sozeau et al. 2019] which provides metaprogramming
+ facilities to work with terms and declarations at the level of
+ this kernel. Our type checker is based on the specification of the
+ typing relation of the Polymorphic Cumulative Calculus of
+ Inductive Constructions (PCUIC) at the basis of Coq and the
+ verification of a relatively efficient and sound typechecker for
+ it. In addition to the kernel implementation, an essential feature
+ of Coq is socalled {\sl extraction} [Lebouzey 2004]; the
+ production of executable code in functional languages from Coq
+ definitions. We present a verified version of this subtle
+ typeandproof erasure step, therefore enabling the verified
+ extraction of a safe typechecker for Coq.",
+ paper = "Soze19.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Soare, Robert I.}
\begin{chunk}{axiom.bib}
@misc{Soar99,
@@ 24322,6 +25278,20 @@ when shown in factored form.
\end{chunk}
+\index{Tanimoto, Steven L.}
+\begin{chunk}{axiom.bib}
+@book{Tani95,
+ author = "Tanimoto, Steven L.",
+ title = {{The Elements of Artificial Intelligence Using Common
+ Lisp}},
+ publisher = "Computer Science Press",
+ year = "1995",
+ isbn = "0716782693",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
\index{Tankink, Carst}
\index{Kaliszyk, Cezary}
\index{Urban, Josef}
@@ 24847,7 +25817,8 @@ when shown in factored form.
publisher = "Cambridge University Press",
year = "2006",
isbn = "9780511161162",
 paper = "Vell06.pdf"
+ paper = "Vell06.pdf",
+ keywords = "shelf"
}
\end{chunk}
@@ 25044,6 +26015,38 @@ when shown in factored form.
\end{chunk}
+\index{Wang, Qingxiang}
+\index{Brown, Chad}
+\index{Kaliszyk, Cezary}
+\index{Urban, Josef}
+\begin{chunk}{axiom.bib}
+@misc{Wang19a,
+ author = "Wang, Qingxiang and Brown, Chad and Kaliszyk, Cezary and
+ Urban, Josef",
+ title = {{Exploration of Neural Machine Translation in
+ Autoformalization of Mathematics in Mizar}},
+ year = "2019",
+ link = "\url{https://arxiv.org/pdf/1912.02636.pdf}",
+ abstract =
+ "In this paper we share several experiments trying to
+ automatically translate informal mathematics into formal
+ mathematics. In our context informal mathematics refers to
+ humanwritten mathematical sentences in the LaTeX format; and
+ formal mathematics refers to statements in the Mizar language. We
+ conducted our experiments against three established neural
+ networkbased machine translation models that are know to deliver
+ competitive results on translating between natural languages. To
+ train these models we also prepared four informaltoformal
+ datasets. We compare and analyze our results according to whether
+ the model is supervised or unsupervised. In order to augment the
+ data available for autoformalization and improve the results, we
+ develop a custom typeelaboration mechanism and integrate it into
+ the supervised translation.",
+ paper = "Wang19a.pdf"
+}
+
+\end{chunk}
+
\index{Wang, Ke}
\begin{chunk}{axiom.bib}
@misc{Wang19,
@@ 25204,6 +26207,19 @@ when shown in factored form.
\end{chunk}
+\index{Weitz, Edmund}
+\begin{chunk}{axiom.bib}
+@book{Weit16,
+ author = "Weitz, Edmund",
+ title = {{Common Lisp Recipes}},
+ publisher = "Apress",
+ year = "2016",
+ isbn = "9781484211779",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
\index{Werner, Benjamin}
\begin{chunk}{axiom.bib}
@inbook{Wern97,
@@ 25261,6 +26277,37 @@ when shown in factored form.
\end{chunk}
+\index{Wiener, Norbert}
+\begin{chunk}{axiom.bib}
+@book{Wien61,
+ author = "Wiener, Norbert",
+ title = {{Cybernetics}},
+ publisher = "MIT Press",
+ year = "1961",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
+\index{Wilf, William}
+\index{Johnsson, Richard K.}
+\index{Weinstock, Charles B.}
+\index{Hobbs, Steven O.}
+\index{Geschke, Charles M.}
+\begin{chunk}{axiom.bib}
+@book{Wilf75,
+ author = "Wilf, William and Johnsson, Richard K. and
+ Weinstock, Charles B. and Hobbs, Steven O.
+ and Geschke, Charles M.",
+ title = {{The Design of an Optimizing Compiler}},
+ publisher = "Elsevier",
+ year = "1975",
+ isbn = "0444001581",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
\index{Wilson, David J.}
\index{Bradford, Russell J.}
\index{Davenport, James H.}
@@ 25753,7 +26800,8 @@ when shown in factored form.
title = {{Handbook of Logic in Computer Science (Volume 2)}},
publisher = "Oxford Science Publications",
year = "1992",
 isbn = "0198537611"
+ isbn = "0198537611",
+ keywords = "shelf"
}
\end{chunk}
@@ 26327,7 +27375,8 @@ when shown in factored form.
title = {{Lambda Calculus with Types}},
publisher = "Cambridge University Press",
year = "2013",
 isbn = "9780521766142"
+ isbn = "9780521766142",
+ keywords = "shelf"
}
\end{chunk}
@@ 28470,7 +29519,8 @@ when shown in factored form.
title = {{Program Verification}},
year = "1992",
publisher = "AddisonWesley",
 isbn = "0201416085"
+ isbn = "0201416085",
+ keywords = "shelf"
}
\end{chunk}
@@ 29072,7 +30122,8 @@ when shown in factored form.
title = {{Handbook of Practical Logic and Automated Reasoning}},
publisher = "Cambridge University Press",
year = "2009",
 isbn = "9780521899574"
+ isbn = "9780521899574",
+ keywords = "shelf"
}
\end{chunk}
@@ 30329,7 +31380,8 @@ when shown in factored form.
title = {{Functional Programming Through Lambda Calculus}},
year = "2011",
publisher = "Dover",
 isbn = "9780486478838"
+ isbn = "9780486478838",
+ keywords = "shelf"
}
\end{chunk}
@@ 30828,7 +31880,8 @@ when shown in factored form.
title = {{Type Theory and Formal Proof}},
year = "2014",
publisher = "Cambridge University Press",
 isbn = "9781107036505"
+ isbn = "9781107036505",
+ keywords = "shelf"
}
\end{chunk}
@@ 31132,7 +32185,8 @@ when shown in factored form.
title = {{Logic and Computation}},
publisher = "Press Syndicate of Cambridge University",
year = "1987",
 isbn = "0521346320"
+ isbn = "0521346320",
+ keywords = "shelf"
}
\end{chunk}
@@ 31158,7 +32212,8 @@ when shown in factored form.
title = {{ML for the Working Programmer 2nd Edition}},
year = "1996",
publisher = "Cambridge University Press",
 isbn = "052156543X"
+ isbn = "052156543X",
+ keywords = "shelf"
}
\end{chunk}
@@ 31366,7 +32421,8 @@ when shown in factored form.
title = {{Types and Programming Languages}},
publisher = "MIT Press",
year = "2002",
 isbn = "9780262162098"
+ isbn = "9780262162098",
+ keywords = "shelf"
}
\end{chunk}
@@ 31607,7 +32663,8 @@ when shown in factored form.
title = {{Handbook of Automated Reasoning (2 Volumes)}},
year = "2001",
publisher = "MIT Press",
 isbn = "0262182238"
+ isbn = "0262182238",
+ keywords = "shelf"
}
\end{chunk}
@@ 34483,7 +35540,8 @@ when shown in factored form.
proofs and certified programs using Coq. With its large collection of
examples and exercies it is an invaluable tool for researchers,
students, and engineers interested in formal methods and the
 development of zerofault software."
+ development of zerofault software.",
+ keywords = "shelf"
}
\end{chunk}
@@ 34525,7 +35583,7 @@ when shown in factored form.
software development process from the specification of requirements to
the finished system. These methos are potentially applicable to the
development of correct hardware systems as well",
 keywords = "axiomref, CASProof, printed"
+ keywords = "axiomref, CASProof, shelf"
}
@@ 35442,6 +36500,24 @@ when shown in factored form.
\end{chunk}
+\index{Bundy, Alan}
+\index{Basin, David}
+\index{Hutter, Dieter}
+\index{Ireland, Andrew}
+\begin{chunk}{axiom.bib}
+@book{Bund05,
+ author = "Bundy, Alan and Basin, David and Hutter, Dieter and
+ Ireland, Andrew",
+ title = {{Rippling: MetaLevel Guidance for Mathematical
+ Reasoning}},
+ publisher = "Cambridge University Press",
+ year = "2005",
+ isbn = "9780521834490",
+ keywords = "shelf"
+}
+
+\end{chunk}
+
\index{Byrd, William}
\begin{chunk}{axiom.bib}
@misc{Byrd17,
@@ 36050,7 +37126,8 @@ when shown in factored form.
Mendler, N.P. and Panagaden, P. and Tsaaki, J.T. and Smith, S.F.",
title = {{Implementing Mathematics with The Nuprl Proof Development System}},
publisher = "PrenticeHall",
 year = "1985"
+ year = "1985",
+ paper = "Cons85.pdf"
}
\end{chunk}
@@ 37089,7 +38166,8 @@ when shown in factored form.
title = {{Essentials of Programming Languages}},
publisher = "MIT Press",
year = "2008",
 isbn = "9780262062794"
+ isbn = "9780262062794",
+ keywords = "shelf"
}
\end{chunk}
@@ 37381,7 +38459,8 @@ when shown in factored form.
link = "\url{http://www.cs.ox.ac.uk/tom.melham/pub/Gordon1993ITH.html}",
publisher = "Cambridge University Press",
year = "1993",
 isbn = "0521441897"
+ isbn = "0521441897",
+ keywords = "shelf"
}
\end{chunk}
@@ 39403,6 +40482,39 @@ when shown in factored form.
\index{Milner, Robin}
\begin{chunk}{axiom.bib}
+@article{Miln72a,
+ author = "Milner, Robin",
+ title = {{Implementation and Applications of Scott's Logic for
+ Computable Functions}},
+ journal = "ACM SIGPLAN Notices",
+ volume = "7",
+ number = "1",
+ year = "1972",
+ pages = "16",
+ abstract =
+ "The basis for this paper is a logic designed by Dana Scott[1] in
+ 1969 for formalizing arguments about computable functions of
+ higher type. This logic uses typed combinators, and we give a more
+ or less direct translation into typed $\lambda$calculus, which is
+ an easier formalism to use, though not so easy for the metatheory
+ because of the presence of bound variables. We then describe, by
+ example only, a proofchecker program which has been implemented
+ for this logic; the program is fully describe in [2]. We relate
+ the induction rule which is central to the logic to two more
+ familiar rules  Recursion Induction and Structural Induction 
+ showing that the former is a theorem of the logic, and that for
+ recursively defined structures the latter is a derived rule of the
+ logic. Finally we show how the syntax and semantics of a simple
+ programming language may be described completely in the logic, and
+ we give an example of a theorem which relates syntactic and
+ semantic properties of programs and which can be stated and proved
+ within the logic."
+}
+
+\end{chunk}
+
+\index{Milner, Robin}
+\begin{chunk}{axiom.bib}
@article{Miln78,
author = "Milner, Robin",
title = {{A Theory of Type Polymorphism in Programming}},
@@ 39458,7 +40570,8 @@ when shown in factored form.
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"
+ paper = "Miln84.pdf",
+ keywords = "printed, DONE"
}
\end{chunk}
@@ 39619,7 +40732,8 @@ when shown in factored form.
title = {{Concrete Semantics}},
isbn = "9783105420",
publisher = "Springer",
 year = "2014"
+ year = "2014",
+ keywords = "shelf"
}
\end{chunk}
@@ 40631,7 +41745,8 @@ when shown in factored form.
seriously}},
year = "2000",
publisher = "Cambridge University Press",
 isbn = "0521771730"
+ isbn = "0521771730",
+ keywords = "shelf"
}
\end{chunk}
@@ 44122,10 +45237,11 @@ Comm. Math. Helv., Vol 18 pp 283308, (1946)
\index{Ritt, Joseph Fels}
\begin{chunk}{axiom.bib}
@book{Ritt48,
 author = {{Ritt, Joseph Fels}},
+ author = "Ritt, Joseph Fels",
title = {{Integration in Finite Terms}},
publisher = "Columbia University Press, New York",
 year = "1948"
+ year = "1948",
+ keywords = "shelf"
}
\end{chunk}
@@ 57007,7 +58123,7 @@ VM/370 SPAD.SCRIPTS August 24, 1979 SPAD.SCRIPT
isbn ="0122042301",
link = "\url{http://staff.bath.ac.uk/masjhd/masternew.pdf}",
paper = "Dave88.pdf",
 keywords = "axiomref",
+ keywords = "axiomref, shelf",
beebe = "Davenport:1988:CA"
}
@@ 76929,7 +78045,8 @@ Springer Verlag Heidelberg, 1989, ISBN 0387969802
title = {{ComputerAided Reasoning: An Approach}},
publisher = "Kluwer Academic Publishers",
year = "2000",
 isbn = "0792377443"
+ isbn = "0792377443",
+ keywords = "shelf"
}
\end{chunk}
@@ 76943,7 +78060,8 @@ Springer Verlag Heidelberg, 1989, ISBN 0387969802
title = {{ComputerAided Reasoning: ACL2 Case Studies}},
publisher = "Kluwer Academic Publishers",
year = "2000",
 isbn = "0792378490"
+ isbn = "0792378490",
+ keywords = "shelf"
}
\end{chunk}
diff git a/changelog b/changelog
index 0ff0a39..9bd2038 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,7 @@
+20200107 tpd src/axiomwebsite/patches.html 20200107.01.tpd.patch
+20200107 tpd books/bookvol13 updated
+20200107 tpd books/bookvol15 updated
+20200107 tpd books/bookvolbib new references
20191219 tpd src/axiomwebsite/patches.html 20191219.01.tpd.patch
20191219 tpd books/bookheader.tex latex cleanup
20191219 tpd books/bookvol0 latex cleanup
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 4b1895b..9f1b581 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 6018,6 +6018,8 @@ books/bookvol15 add initial parse function
books/bookvol15 add new code
20191219.01.tpd.patch
books/bookvol* cleanup
+20200107.01.tpd.patch
+books/bookvol15 updated

1.9.1