From 88f9b3e2fa7e98a5fe6f5ae883298dc0fa2147d0 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Mon, 4 Feb 2019 02:50:08 0500
Subject: [PATCH] books/bookvol10.4 add documentation to CRAPACK
Goal: Literate Axiom

books/bookvol10.4.pamphlet  32 ++
changelog  2 +
patch  1163 +
src/axiomwebsite/patches.html  4 +
4 files changed, 39 insertions(+), 1162 deletions()
diff git a/books/bookvol10.4.pamphlet b/books/bookvol10.4.pamphlet
index 7d13d66..ef5f7c3 100644
 a/books/bookvol10.4.pamphlet
+++ b/books/bookvol10.4.pamphlet
@@ 17596,6 +17596,37 @@ CoordinateSystems(R) : SIG == CODE where
\end{chunk}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{package CRAPACK CRApackage}
+
+From \cite{Knil18}: Given the integers $a$, $b$, a linear modular equation
+\index{linear modular equation} or congruence
+\index{congruence} $ax+b=0 \bmod m$ asks to find an integer $x$ such
+that $ax+b$ is divisible by $m$. This linear equation can always be
+solved if $a$ and $m$ are coprime. The Chinese Remainder Theorem
+\index{Chinese Remainder Theorem} deals with the
+system of linear modular equations
+\index{system of linear modular equations}
+$x=b_1\bmod m_1, x=b_2\bmod m_2, \ldots, x=b_n\bmod m_n$, where
+$m_k$ are the moduli.
+\index{moduli}. More generally, for an integer $n\times n$ matrix
+$A$ we call $Ax=b\bmod m$ a Chinese Remainder Theorem system or
+shortly CRT system if the $m_j$ are pairwise relatively prime and in
+each row there is a matrix element $A_{ij}$ relatively prime to $m_i$.
+
+{\bf Theorem}: Every Chinese Remainder theorem system has a solution.
+\index{{\bf Theorem}: Chinese Remainder}
+
+The classical single variable case is when $A_{i1}=1$ and
+$A_{ij}=0$ for $j>1$. Let $M=m_1\cdots m_2\cdots m_n$ be the product.
+In this onedimensional case, the result implies that
+$x\bmod M\rightarrow (x\bmod m_1,\ldots,x\bmod m_n)$ is a ring
+isomorphism. Define $M_i=M/m_i$. An explicit algorithm is to
+find numbers $y_i$,$z_i$ with $y_iM_i+z_im_i=1$ (finding $y$, $z$
+solving $ay+bz=1$ for coprime $a,b$ is computed using the
+Euclidean algorithm
+\index{Euclidean algorithm}), then finding
+$x=b_1m_1y_1+\cdots+b_nm_ny_n$. See \cite{Mart97a},\cite{Ding96}
+and \cite{Knil12} for the multivariate case.
+
\begin{chunk}{CRApackage.input}
)set break resume
)sys rm f CRApackage.output
@@ 86717,6 +86748,7 @@ mu = (1)^k, when n is the product of k distinct primes. The corresponding
Axiom operation is moebiusMu. This function occurs in the following theorem:
Theorem: (Moebius Inversion Formula):
+\index{\bf{Theorem} Moebius Inversion Formula}
Let f(n) be a function on the positive integers and let F(n)
be defined by
F(n) = \sum_{d  n} f(n)
diff git a/changelog b/changelog
index 4f357f7..38b49c6 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20190204 tpd src/axiomwebsite/patches.html 20190204.01.tpd.patch
+20190204 tpd books/bookvol10.4 add documentation to CRAPACK
20190131 tpd src/axiomwebsite/patches.html 20190131.01.tpd.patch
20190131 tpd books/bookvolbib add references
20181211 tpd src/axiomwebsite/patches.html 20181211.03.tpd.patch
diff git a/patch b/patch
index dce4f9a..071c84f 100644
 a/patch
+++ b/patch
@@ 1,1163 +1,4 @@
books/bookvolbib add references
+books/bookvol10.4 add documentation to CRAPACK
Goal: Proving Axiom Sane
+Goal: Literate Axiom
\index{Castagna, Giuseppe}
\index{Lanvin, Victor}
\index{Petrucciani, Tommaso}
\index{Siek, Jeremy G.}
\begin{chunk}{axiom.bib}
@misc{Cast19,
 author = "Castagna, Giuseppe and Lanvin, Victor and Petrucciani, Tommaso
 and Siek, Jeremy G.",
 title = {{Gradual Typing: A New Perspective}},
 link = "\url{https://www.irif.fr/~gc//papers/popl19.pdf}",
 year = "2019",
 abstract =
 "We define a new, more semantic interpretation of gradual types and use
 it to “gradualize” two forms of polymorphism: subtyping polymorphism
 and implicit parametric polymorphism. In particular, we use the new
 interpretation to define three gradual type systems —HindleyMilner,
 with subtyping, and with union and intersection types— in terms of two
 preorders, subtyping and materialization. These systems are defined
 both declaratively and algorithmically. The declarative presentation
 consists in adding two subsumptionlike rules, one for each preorder,
 to the standard rules of each type system. This yields more
 intelligible and streamlined definitions and shows a direct
 correlation between cast insertion and materialization. For the
 algorithmic presentation, we show how it can be defined by reusing
 existing techniques such as unification and tallying.",
 paper = "Cast19.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Siek, Jeremy, G.}
\index{Taha, Walid}
\begin{chunk}{axiom.bib}
@inproceedings{Siek06,
 author = "Siek, Jeremy, G. and Taha, Walid",
 title = {{Gradual Typing for Functional Languages}},
 booktitle = "Proc. of Scheme and Functional Programming Workshop",
 year = "2006",
 publisher = "ACM",
 pages = "8192",
 abstract =
 "Static and dynamic type systems have wellknown strengths and
 weaknesses, and each is better suited for different programming
 tasks. There have been many efforts to integrate static and dynamic
 typing and thereby combine the benefits of both typing disciplines in
 the same language. The flexibility of static typing can be improved
 by adding a type Dynamic and a typecase form. The safety and
 performance of dynamic typing can be improved by adding optional type
 annotations or by performing type inference (as in soft
 typing). However, there has been little formal work on type systems
 that allow a programmercontrolled migration between dynamic and
 static typing. Thatte proposed QuasiStatic Typing, but it does not
 statically catch all type errors in completely annotated
 programs. Anderson and Drossopoulou defined a nominal type system
 for an objectoriented language with optional type annotations.
 However, developing a sound, gradual type system for functional
 languages with structural types is an open problem.

 In this paper we present a solution based on the intuition that the
 structure of a type may be partially known/unknown at compile time
 and the job of the type system is to catch incompatibilities between
 the known parts of types. We define the static and dynamic semantics
 of a $lambda$calculus with optional type annotations and we prove that
 its type system is sound with respect to the simplytyped λ
 $lambda$calculus for fullyannotated terms. We prove that this
 calculus is type safe and that the cost of dynamism is
 'payasyougo'.",
 paper = "Siek06.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Bauer, Andrej}
\begin{chunk}{axiom.bib}
@misc{Baue19,
 author = "Bauer, Andrej",
 title = {{How to Implement Type Theory in an Hour}},
 year = "2019",
 link = "\url{https://vimeo.com/286652934}",
 comment = "\url{https://github.com/andrejbauer/spartantypetheory}"
}

\end{chunk}

\index{Coquand, Thierry}
\index{Kinoshita, Yoshiki}
\index{Nordstrom, Bengt}
\index{Takeyama, Makoto}
\begin{chunk}{axiom.bib}
@misc{Coqu19,
 author = "Coquand, Thierry and Kinoshita, Yoshiki and Nordstrom, Bengt
 and Takeyama, Makoto",
 title = {{A Simple TypeTheoretic Language: MiniTT}},
 year = "2019",
 link = "\url{http://www.cse.chalmers.se/~bengt/papers/GKminiTT.pdf}",
 abstract =
 "This paper presents a formal description of a small functional
 language with dependent types. The language contains data types,
 mutual re cursive/inductive definitions and a universe of small
 types. The syntax, semantics and type system is specified in such a
 way that the imple mentation of a parser, interpreter and type
 checker is straightforward. The main difficulty is to design the
 conversion algorithm in such a way that it works for open expressions.
 The paper ends with a complete implementation in Haskell (around 400
 lines of code).",
 paper = "Coqu19.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Pfenning, Frank}
\begin{chunk}{axiom.bib}
@misc{Pfen06,
 author = "Pfenning, Frank",
 title = {{Constraint Logic Programming}},
 year = "2006",
 link = "\url{http://www.cs.cmu.edu/~fp/courses/lp/lectures/27clp.pdf}",
 paper = "Pfen06.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Pfenning, Frank}
\begin{chunk}{axiom.bib}
@misc{Pfen07,
 author = "Pfenning, Frank",
 title = {{Logic Programming}},
 year = "2007",
 link = "\url{http://www.cs.cmu.edu/~fp/courses/lp/lectures/lpall.pdf}",
 paper = "Pfen07.pdf"
}

\end{chunk}

\index{Tennant, Neil}
\begin{chunk}{axiom.bib}
@book{Tenn90,
 author = "Tennant, Neil",
 title = {{Natural Logic}},
 publisher = "Edinburgh University Press",
 isbn = "0852245793",
 year = "1990",
 paper = "Tenn90.pdf"
}

\end{chunk}

\index{Vellerman, Daniel J.}
\begin{chunk}{axiom.bib}
@book{Vell06,
 author = "Vellerman, Daniel J.",
 title = {{How To Prove It}},
 publisher = "Cambridge University Press",
 year = "2006",
 isbn = "9780511161162",
 paper = "Vell06.pdf"
}

\end{chunk}

\index{Chiswell, Ian}
\index{Hodges, Wilfrid}
\begin{chunk}{axiom.bib}
@book{Chis07,
 author = "Chiswell, Ian and Hodges, Wilfrid",
 title = {{Mathematical Logic}},
 publisher = "Oxford University Press",
 year = "2007",
 isbn = "9780198571001",
 paper = "Chis07.pdf"
}

\end{chunk}

\index{Bostock, David}
\begin{chunk}{axiom.bib}
@book{Bost97,
 author = "Bostock, David",
 title = {{Intermediate Logic}},
 publisher = "Clarendon Press",
 year = "1997",
 isbn = "0198751419",
 paper = "Bost97.pdf"
}

\end{chunk}

\index{Enderton, Herbert B.}
\begin{chunk}{axiom.bib}
@book{Ende01,
 author = "Enderton, Herbert B.",
 title = {{A Mathematical Introduction to Logic}},
 publisher = "Harcourt Academic Press",
 year = "2001",
 isbn = "0122384520",
 paper = "Ende01.pdf"
}

\end{chunk}

\index{van Dalen, Dirk}
\begin{chunk}{axiom.bib}
@book{Dale08,
 author = "van Dalen, Dirk",
 title = {{Logic and Structure}},
 publisher = "Springer",
 year = "2008",
 isbn = "9783540208792",
 paper = "Dale08.pdf"

}

\end{chunk}

\index{Smith, Peter}
\begin{chunk}{axiom.bib}
@book{Smit13,
 author = "Smith, Peter",
 title = {{An Introduction to Godel's Theorems}},
 publisher = "Cambridge University Press",
 year = "2013",
 isbn = "9781107022843",
 paper = "Smit13.pdf"
}

\end{chunk}

\index{Leary, Christopher C.}
\index{Kristiansen, Lars}
\begin{chunk}{axiom.bib}
@book{Lear15,
 author = "Leary, Christopher C. and Kristiansen, Lars",
 title = {{A Friendly Introduction to Mathematical Logic}},
 publisher = "Milne Library, Geneseo",
 year = "2015",
 isbn = "9781942341321",
 paper = "Lear15.pdf"

}

\end{chunk}

\index{Cutland, Nigel}
\begin{chunk}{axiom.bib}
@book{Cutl80,
 author = "Cutland, Nigel",
 title = {{Computability: An Introduction to Recusive Function Theory}},
 publisher = "Cambridge University Press",
 year = "1980",
 isbn = "0521223849",
 paper = "Cutl80.pdf"
}

\end{chunk}

\index{Hrbacek, Karel}
\index{Jech, Thomas}
\begin{chunk}{axiom.bib}
@book{Hrba99,
 author = "Hrbacek, Karel and Jech, Thomas",
 title = {{Introduction to Set Theory}},
 publisher = "Marcel Dekker, Inc",
 year = "1999",
 isbn = "0824779150",
 paper = "Hrba99.pdf"
}

\end{chunk}

\index{Roitman, Judith}
\begin{chunk}{axiom.bib}
@misc{Roit13,
 author = "Roitman, Judith",
 title = {{Introduction to Modern Set Theory}},
 link = "\url{http://www.math.ku.edu/~roitman/SetTheory.pdf}",
 year = "2013",
 paper = "Roit13.pdf"
}

\end{chunk}

\index{Fitting, Melvin}
\begin{chunk}{axiom.bib}
@book{Fitt69,
 author = "Fitting, Melvin",
 title = {{Intuitionistic Logic Model Theory and Forcing}},
 publisher = "North Holland",
 year = "1969",
 paper = "Fitt69.pdf"
}

\end{chunk}

\index{Popkorn, Sally}
\index{Simmons, Harold}
\begin{chunk}{axiom.bib}
@book{Popk94,
 author = "Popkorn, Sally",
 title = {{First Steps in Modal Logic}},
 publisher = "Cambridge University Press",
 year = "1994",
 isbn = "9780521464826",
 link =
 "\url{https://cs.famaf.unc.edu.ar/~careces/ml18/downloads/popkorn.pdf}",
 paper = "Popk94.pdf"
}

\end{chunk}

\index{Sipser, Michael}
\begin{chunk}{axiom.bib}
@book{Sips13,
 author = "Sipser, Michael",
 title = {{Introduction to the Theory of Computation}},
 publisher = "Cengage Learning",
 year = "2013",
 isbn = "9781133187790",
 link = "\url{https://theswissbay.ch/pdf/Book/Introduction%20to%20the%20theory%20of%20computation_third%20edition%20%20Michael%20Sipser.pdf}",
 paper = "Sips13.pdf"
}

\end{chunk}

\index{Smullyan, Raymond M.}
\begin{chunk}{axiom.bib}
@book{Smul92,
 author = "Smullyan, Raymond M.",
 title = {{Godel's Incompleteness Theorems}},
 publisher = "Oxford University Press",
 year = "1992",
 isbn = "0195046722",
 paper = "Smul92.pdf"
}

\end{chunk}

\index{Smith, Peter}
\begin{chunk}{axiom.bib}
@misc{Smit17,
 author = "Smith, Peter",
 title = {{Teach Yourself Logic 2017: A Study Guide}},
 link =
"\url{https://www.logicmatters.net/resources/pdfs/TeachYourselfLogic2017.pdf}",
 year = "2017",
 paper = "Smit17.pdf"
}

\end{chunk}

\index{Murphy, Robin R.}
\begin{chunk}{axiom.bib}
@book{Murp18,
 author = "Murphy, Robin R.",
 title = {{Robotics Through Science Fiction}},
 publisher = "MIT Press",
 year = "2018",
 link =
 "\url{https://mitpress.mit.edu/books/roboticsthroughsciencefiction}",
 isbn = "9780262536264",
 comment = "verification, validation, and trust"

}

\end{chunk}

\index{Kaminski, Paul}
\begin{chunk}{axiom.bib}
@techreport{Kami12,
 author = "Kaminski, Paul",
 title = {{The Role of Autonomy in DoD Systems}},
 type = "Task Force Report",
 institution = "Defense Science Board, Dept. of Defense",
 year = "2012",
 link = "\url{https://fas.org/irp/agency/dod/dsb/autonomy.pdf}",
 comment = "verification, validation, and trust"

}

\end{chunk}

\index{Siciliano, Bruno}
\index{Oussama, Khatib}
\begin{chunk}{axiom.bib}
@book{Sici16,
 author = "Siciliano, Bruno and Oussama, Khatib",
 title = {{Springer Handbook of Robotics}},
 publisher = "Springer",
 year = "2016",
 abstract =
 "Reaching for the human frontier, robotics is vigorously engaged in
 the growing challenges of new emerging domains. Interacting,
 exploring, and working with humans, the new generation of robots will
 increasingly touch people and their lives. The credible prospect of
 practical robots among humans is the result of the scientific
 endeavour of a half a century of robotic developments that established
 robotics as a modern scientific discipline. The Springer Handbook of
 Robotics brings a widespread and wellstructured compilation of
 classic and emerging application areas of robotics. From the
 foundations to the social and ethical implications of robotics, the
 handbook provides a comprehensive collection of the accomplishments in
 the field, and constitutes a premise of further advances towards new
 challenges in robotics. This handbook, edited by two internationally
 renowned scientists with the support of an outstanding team of seven
 part editors and onehundred sixtyfour authors, is an authoritative
 reference for robotics researchers, newcomers to the field, and
 scholars from related disciplines such as biomechanics, neurosciences,
 virtual simulation, animation, surgery, and sensor networks among
 others.",
 paper = "Sici16.pdf"
}

\end{chunk}

\index{MartinL\"of, P.}
\begin{chunk}{axiom.bib}
@article{Mart84,
 author = "MartinL\"of, P.",
 title = {{Constructive Mathematics and Computer Programming}},
 journal = "Phil. Trans. Royal Society London",
 volume = "312",
 year = "1984",
 pages = "501518",
 link =
 "\url{https://royalsocietypublishing.org/doi/pdf/10.1098/rsta.1984.0073}",
 abstract =
 "If programming is understood not as the writing of instructions for
 this or that computing machine but as the design of methods of
 computation that it is the computer’s duty to execute (a difference
 that Dijkstra has referred to as the difference between computer
 science and computing science), then it no longer seems possible to
 distinguish the discipline of programming from constructive
 mathematics. This explains why the intuitionistic theory of types
 (MartinLof 1975 In Logic Colloquium 1973 (ed. H. E. Rose and
 J. C. Shepherdson), pp. 73  118 . Amsterdam: North Holland), which
 was originally developed as a symbolism for the precise codification
 of constructive mathematics, may equally well be viewed as a
 programming language. As such it provides a precise notation not
 only, like other programming languages, for the programs themselves
 but also for the tasks that the programs are supposed to perform.
 Moreover, the inference rules of the theory of types, which are again
 completely formal, appear as rules of correct program synthesis. Thus
 the correctness of a program written in the theory of types is proved
 formally at the same time as it is being synthesized.",
 paper = "Mart84.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Oberhoff, Sebastian}
\begin{chunk}{axiom.bib}
@misc{Ober18,
 author = "Oberhoff, Sebastian",
 title = {{Incompleteness Ex Machina}}
 year = "2018",
 abstract =
 "In this essay we'll prove Godel's incompleteness theorems
 twice. First, we'll prove them the good oldfashioed way. Then
 we'll repeat the feat in the setting of computation. In the
 process we'll discover that Godel's work, rightly viewed, needs to
 be split into two parts: the transport of computation into the
 arena of arithmetic on the one hand and the actual incompleteness
 theorems on the other. After we're done there will be cake.",
 paper = "Ober18.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Deutsch, David}
\begin{chunk}{axiom.bib}
@article{Deut85,
 author = "Deutsch, David",
 title = {{Quantum Theory, the ChurchTuring Principle and the
 Universal Quantum Computer}},
 journal = "Proc. Royal Society of London",
 volume = "400",
 pages = "97117",
 year = "1985",
 abstract =
 "It is argued that underlying the ChurchTuring hypothesis there
 is an implicit physical assertion. Here, this assertion is
 presented explicitly as a physical principle: 'every finitely
 realizable physical system can be perfectly simulated by a
 universal model computing machine operating by finite
 means'. Classical physics and the universal Turing machine,
 because the former is continuous and the latter discrete, do not
 obey the principle, at leeast in the strong form above. A class of
 model computing machines that is the quantum generalization of the
 class of Turing machines is described, and it is shown that
 quantum theory and the 'universal quantum computer' are compatible
 with the principle. Computing machines resembling the universal
 quantum computer could, in principle, be built and would have many
 remarkable properties not reproducible by any Turing
 machine. These do not include the computation of nonrecursive
 functions, but they do include 'quantum parallelism', a method by
 which certain probabilistic tasks can be performed faster by a
 universal quantum computer than by any classical restriction of
 it. The intuitive explanation of these properties places an
 intolerable strain on all interpretations of quantum theory other
 than Everett's. Some of the numerous connections between the
 quantum theory of computation and the rest of physics are
 explored. Quantum complexity theory allows a physically more
 reasonable definition of the 'complexity' or 'knowledge' in a
 physical system than does classical complexity theory.",
 paper = "Deut85.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Antoy, Sergio}
\index{Peters, Arthur}
\begin{chunk}{axiom.bib}
@article{Anto12,
 author = "Antoy, Sergio and Peters, Arthur",
 title = {{Compiling a Functional Logic Language}},
 booktitle = "11th Int. Symp. on Functional and Logic Programming",
 journal = "LNCS",
 volume = "7294",
 pages = "1731",
 year = "2012",
 abstract =
 "We present the design of a compiler for a functional logic
 programming language and discuss the compiler's implementation.
 The source program is abstracted by a constructor based graph
 rewriting system obtained from a functional logic program after
 syntax desugaring, lambda lifting and similar transformations
 provided by a compiler's frontend. This system is
 nondeterministic and requires a specialized normalization
 strategy. The target program consists of 3 procedures that execute
 graph replacements originating from either rewrite or pulltab
 seps. These procedures are deterministic and easy to encode in an
 ordinary programming language. We describe the generation of the 3
 procedures, discuss the correctness of our approach, highlight
 some key elements of an implementation, and benchmark the
 performance of a proof of concept. Our compilation scheme is
 elegant and simple enough to be presented in one page.",
 paper = "Anto12.pdf",
 keywords = "printed"
}

\end{chunk}

\index{MacQueen, David B.}
\begin{chunk}{axiom.bib}
@misc{Macqxx,
 author = "MacQueen, David B.",
 title = {{Reflections on Standard ML}},
 year = "unknown",
 abstract =
 "Standard ML is one of a number of new programming languages
 developed in the 1980s that are seen as suitable vehicles for
 serious systems and applications programming. It offers an
 excellent ratio of expressiveness to language complexity, and
 provides competitive efficiency. Because of its type and module
 system, Standard ML manages to combine safety, security, and
 robustness with much of the flexibility of dynamically typed
 languages like Lisp. It is also has the most welldeveloped
 scientific foundation of any major language. Here I review the
 strengths and weaknesses of Standard ML and describe some of what
 we have learned through the design, implementation, and use of the
 language.",
 paper = "Macqxx.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Tarver, Mark}
\begin{chunk}{axiom.bib}
@misc{Tarvxx,
 author = "Tarver, Mark",
 title = {{A Language for Implementing Arbitrary Logics}},
 year = "unknown",
 abstract =
 "SEQUEL is a newgeneration functional programming language, which
 allows the specification of types in a notation based on the
 sequent calculus. The sequent calculus notation suffices for the
 construction of types for type checking and for the specification
 of arbitrary logics. Compilation techniques derived from both
 functional and logic programming are used to derive
 highperformance ATPs from these specifications.",
 paper = "Tarvxx.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Collofello, James S.}
\begin{chunk}{axiom.bib}
@techreport{Coll88,
 author = "Collofello, James S.",
 title = {{Introduction to Software Verification and Validation}},
 type = "technical report",
 institution = "Carnegie Mellon University",
 number = "SEICM131.1",
 year = "1988",
 abstract =
 "SEI curriculum modules document and explication software
 engineering topics. They are intended to be useful in a variety of
 situations  in the preparation of courses, in the planning of
 individual lectures, in the design of curricula, and in
 professional selfstudy. Topics do not exist in isolation,
 however, and the question inevitably arises how one module is
 related to another. Because modules are written by different
 authors at different times, the answer could easily be 'not at
 all'. In a young field struggling to define itself, this would be
 an unfortunate situation.

 The SEI deliberately employs a number of mechanisms to achieve
 compatible points of view across curriculum modules and to fill
 the content gaps between them. Modules such as {\sl Introduction
 to Software Verification and Validation} is one of the most
 important devices. In this latest revision, Professor Collofillo
 has more modules to integrate into a coherent picture than when we
 released his first draft more than a year ago  modules on
 quality assurance, unit testing, technical reviews, and formal
 verification, as well as less directly related modules on
 specification, requirements definition, and design. We believe you
 will find this curriculum module interesting and useful, both in
 its own right and by virtue of the understanding of other modules
 that it facilitates.",
 paper = "Coll88.pdf",
 keywords = "printed"

}

\end{chunk}

\index{Gravel, Katherine}
\index{Jananthan, Hayden}
\index{Kepner, Jeremy}
\begin{chunk}{axiom.bib}
@misc{Grav18,
 author = "Gravel, Katherine and Jananthan, Hayden and Kepner, Jeremy",
 title = {{Visually Representing the Landscape of Mathematical Structures}},
 link = "\url{https://arxiv.org/abs/1809.05930}",
 year = "2018",
 abstract =
 "The information technology explosion has dramatically increased
 the application of new mathematical ideas and has led to an
 increasing use of mathematics across a wide range of fields that
 have been traditionally labeled 'pure' or 'theoretical'. There is
 a critical need for tools to make these concepts readily
 accessible to a broader community. This paper details the creation
 of visual representations of mathematical structures commonly
 found in pure mathematics to enable both students and
 professionals to rapidly understand the relationships among and
 between mathematical structures. Ten broad mathematical structures
 were identified and used to make eleven maps, with 187 unique
 structures in total. The paper presents a method and
 implementation for categorizing mathematical structures and for
 drawing relationships between mathematical structures that
 provides insight for a wide audience. The most in dept map is
 available online for public use.",
 comment = "\url{http://www.mit.edu/~kepner/GravelMathMap.pdf}",
 paper = "Grav18.pdf"
}

\end{chunk}

\index{Hoare, C.A.R}
\begin{chunk}{axiom.bib}
@article{Hoar74,
 author = "Hoare, C.A.R",
 title = {{Hints on Programming Language Design}},
 journal = "Computer Systems Reliability",
 volume = "20",
 pages = "505534",
 year = "1974",
 link = "\url{http://flint.cs.yale.edu/cs428/doc/HintsPL.pdf}",
 abstract =
 "This paper presents the view that a programming language
 is a tool that should assist the programmer in the most difficult
 aspects of his art, namely program design, documentation, and
 debugging. It discusses the objective criteria for evaluating a
 language design and illustrates them by application to language
 features of both highlevel languages and machinecode
 programming. It concludes with an annotated reading list,
 recomended for all intending language designers.",
 paper = "Hoar74.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Hemann, Jason}
\index{Friedman, Daniel P.}
\begin{chunk}{axiom.bib}
@misc{Hema13,
 author = "Hemann, Jason and Friedman, Daniel P.",
 title = {{uKanren: A Minimal Functional Core for Relational Programming}},
 year = "2013",
 link = "\url{webyrd.net/scheme2013/papers/HemannMuKanren2013.pdf}",
 abstract =
 "This paper presents $\mu$Kanren, a minimalist language in the
 miniKanren family of relational (logic) programming languages. Its
 implementation comprises fewer than 40 lines of Scheme. We
 motivate the need for a minimalist miniKanren language, and
 iteratively develop a complete search strategy. Finally, we
 demonstrate that through sufficient userlevel features one
 regains much of the expressiveness of other miniKanren
 languages. In our opinion its brevity and simple semantics make
 $\mu$Kanren uniquely elegant.",
 paper = "Hema13.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Cardelli, Luca}
\begin{chunk}{axiom.bib}
@techreport{Card93,
 author = "Cardelli, Luca",
 title = {{Typeful Programmnig}},
 type = "research report",
 year = "1993",
 institution = "Digital Equipment Corporation",
 number = "SRC Research Report 45",
 abstract =
 "There exists an identifiable programming style based on the
 widespread use of type information handled through mechanical
 typechecking techniques.

 This typeful programming style is in a sense independent of the
 language it is embedded in; it adapts equally well to functional,
 imperative, objectoriented, and algebraic programming, and it is
 not incompatible with relational and concurrent programming.

 The main purpose of this paper is to show how typeful programming
 is best supported by sophisticated type systems, and how these
 systems can help in clarifying programming issues and in adding
 power and regularity to languages.

 We start with an introduction to the notions of types, subtypes
 and polymorphism. Then we introduce a general framework, derived
 in part from constructive logic, into which most of the known type
 systems can be accommodated and extended. The main part of the
 paper shows how this framework can be adapted systematically to
 cope with actual programming constructs. For concreteness we
 describe a particular programming language with advanced features;
 the emphasis here is on the combination of subtyping and
 polymorphism. We then discuss how typing concepts apply to large
 programs. We also sketch how typing applies to system programming;
 an area which by nature escapes rigid typing. In summary, we
 compare the most common programming styles, suggesting that many
 of them are compatible with, and benefit from, a typeful discipline.",
 paper = "Card93.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Lamport, Leslie}
\index{Paulson, Lawrence C.}
\begin{chunk}{axiom.bib}
@article{Lamp99,
 author = "Lamport, Leslie and Paulson, Lawrence C.",
 title = {{Should Your Specification Language Be Typed?}},
 journal = "ACM Trans. on Document Formatting",
 volume = "21",
 number = "3",
 year = "1999",
 pages = "502526",
 abstract =
 "Most specification languages have a type system. Type systems are
 hard to get right, and getting them wrong can lead to
 inconsistencies. Set theory can serve as the basis for a
 specification language without types. This possibility, which has
 been widely overlooked, offers many advantages. Untyped set theory
 is simple and is more flexible than any simple typed
 formalism. Polymorphism, overloading, and subtyping can make a
 type system more powerful, but at the cost of increased
 complexity, and such refinements can never attain the flexibility
 of having no types at all. Typed formalisms have advantages too,
 stemming from the power of mechanical type checking. While types
 serve little purpose in hand proofs, they do help with mechanized
 proofs. In the absence of verification, type checking can catch
 errors in specifications. It may be possible to have the best of
 both worlds by adding typing annotations to an untyped
 specification language. We consider only specification languages,
 not programming languages",
 paper = "Lamp99.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Appel, Andrew W.}
\begin{chunk}{axiom.bib}
@article{Appe98a,
 author = "Appel, Andrew W.",
 title = {{SSA is Functional Programming}},
 journal = "SIGPLAN Notices",
 year = "1998",
 abstract =
 "Static SingleAssignment (SSA) form is an intermediate language
 designed to make optimization clean and efficient for imperative
 language (Fortran, C) compilers. LambdaCalculus is an
 intermediate language that makes optimization clean and efficient
 for functional language (Scheme, ML, Haskell) compilers. The SSA
 community draws pictures of graphs with basic blocks and flow
 edges, and the functional language community writes lexically
 nested functions, but (as Richard Kelsey recently pointed out)
 they're both doing exactly the same thing in different notation.",
 paper = "Appe98a.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Cloostermans, Bouke},
\begin{chunk}{axiom.bib}
@misc{Cloo12,
 author = "Cloostermans, Bouke",
 title = {{QuasiLinear GCD Computation and Factoring RSA Moduli}},
 school = "Eindhoven Univ. of Technology",
 comment = "Bachelor Project",
 year = "2012",
 abstract =
 "This bachelor project consists of two parts. First, we describe
 two subquadratic GCD algorithms and test our implementation of
 these algorithms. Both algorithms work in a similar recursive way
 and have a running time of $O(n log^2n log log n)$ where $n$ is
 the amount of digits of the input. Second, we describe and compare
 three algorithms which compute GCD's of more than two numbers. Two
 algorithms use a treelike structure to compute these GCD's and the
 other algorithm builds a coprime base from the input set. The
 algorithms which uses a treelike structure to compute these GCD's
 is faster than building a coprime base although all algorithms are
 quasilinear. The downside of these algorithm is that they only run
 well if few common factors exist in the input set. These
 algorithms have been used to factorize roughly 0.4\% of a 11.1
 million RSA keys dataset. However, this is only possible if the
 keys are badly generated.",
 paper = "Cloo12.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Roessle, Ian}
\index{Verbeek, Freek}
\index{Ravindran, Binoy}
\begin{chunk}{axiom.bib}
@proceedings{Roes19,
 author = "Roessle, Ian and Verbeek, Freek and Ravindran, Binoy",
 title = {{Formally Verified Big Step Semantics out of x8664 Binaries}},
 booktitle = "CPP'19",
 year = "2019",
 publisher = "ACM",
 abstract =
 "This paper presents a methodology for generating formally proven
 equivalence theorems between decompiled x8664 machine code and
 big step semantics. These proofs are built on top of two
 additional contributions. First, a robust and tested formal x8664
 machine model containing small step semantics for 1625
 instructions. Second, a decompilation into logic methodology
 supporting both x8664 assembly and machine code at large
 scale. This work enables blackbox binary verification, i.e.,
 formal verification of a binary where source code is
 unavailable. As such, it can be applied to safetycritical systems
 that consist of legacy components, or components whose source code
 is unavailable due to proprietary reasons. The methodology
 minimizes the trusted code base by leveraging machinelearned
 semantics to build a formal machine model. We apply the
 methodolgoy to several case studies, including binaries that
 heavily rely on the SSE2 floatingpoint instruction set, and
 binaries that are obtained by compiling code that is obtained by
 inlining assembly into C code.",
 paper = "Roes19.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Kaliszyk, Cezary}
\index{Urban, Josef}
\begin{chunk}{axiom.bib}
@misc{Kali14,
 author = "Kaliszyk, Cezary and Urban, Josef",
 title = {{LearningAssisted Automated Reasoning with Flyspeck}},
 comment = "arXiv:1211.7012v3",
 year = "2014",
 abstract =
 "The considerable mathematical knowledge encoded by the Flyspeck
 project is combined with external automated theorem provers (ATPs)
 and machinelearning premise selection methods trained on the
 Flyspeck proofs, producing an AI system capable of proving a wide
 range of mathematical conjectures automatically. The performance
 of this architecture is evaluated in a bootstrapping scenario
 emulating the development of Flyspeck from axioms to the last
 theorem, each time using only the previous theorems and proofs. It
 is shown that 39\% of the 14185 theorems could be proved in a
 pushbutton mode (without any highlevel advice and user
 interaction) in 30 seconds of real time on a fourteen CPU
 workstation.

 The necessary work involves: (i) an implementation of sound
 translations of the HOL Light logic to ATP formalisms: untyped
 firstorder, polymorphic typed firstorder, and typed firstorder,
 (ii) export of the dependency information from HOL Light and ATP
 proofs for the machine learners, and (iii) choice of suitable
 representations and methods for learning from previous proofs, and
 their integration as advisors with HOL Light. This work is
 described and discussed here, and an initial analysis of the body
 of proofs that were found fully automatically is provided.",
 paper = "Kali14.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Mueller, Robert A.}
\index{Page, L. Rex}
\begin{chunk}{axiom.bib}
@book{Muel88,
 author = "Mueller, Robert A. and Page, L. Rex",
 title = {{Symbolic Computing with Lisp and Prolog}},
 publisher = "Wiley",
 year = "1988",
 isbn = "0471607711"
}

\end{chunk}

\index{Stump, Aaron}
\begin{chunk}{axiom.bib}
@misc{Stum18,
 author = "Stump, Aaron",
 title = {{Syntax and Semantics of Cedille}},
 year = "2018",
 comment = "arXiv:1806.04709v1",
 paper = "Stum18.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Geuvers, Herman}
\begin{chunk}{axiom.bib}
@article{Geuv00,
 author = "Geuvers, Herman",
 title = {{Induction Is NOt Derivable in Second Order Dependent Type Theory}},
 journal = "LNCS",
 volume = "2044",
 year = "2000",
 pages = "166181",
 abstract =
 "This paper proves the nonderivability of induction in second
 order dependent type theory ($\lambda{}P2$). This is done by
 providing a model construction for $\lambda{}P2$, based on a
 saturated sets like interpretation of types as sets of terms of a
 weakly extensional combinatory algebra. We give countermodels in
 which the induction principle over natural numbers is not
 valid. The proof does not depend on the specific encoding for
 natural numbers that has been chosen (like e.g. polymorphic Church
 numerals), so in fact we prove that there can not be an encoding
 of natural numbers in $\lambda{}P2$ such that the induction
 principle is satisfied. The method extends immediately to other
 data types, like booleans, lists, trees, etc.

 In the process of the proof we establish some general properties
 of the models, which we think are of independent
 interest. Moreover, we show that the Axiom of Choice is not
 derivable in $\lambda{}P2$.",
 paper = "Geuv00.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Sjoberg, Vilhelm}
\begin{chunk}{axiom.bib}
@phdthesis{Sjob15,
 author = "Sjoberg, Vilhelm",
 title = {{A Dependently Typed Language with NonTermination}},
 school = "University of Pennsylvania",
 year = "2015",
 abstract =
 "We propose a fullspectrum dependently typed programming
 language, {\sl Zombie}, which supports general recursion
 natively. The Zombie implementation is an elaborating
 typechecker. We prove type safety for a large subset of the Zombie
 core language, including features wuch as computational
 irrelevance, CBVreduction, and propositional equality with a
 heterogeneous, completely erased elimination form. Zombie does not
 automatically $\beta$reduce expressions, but instead uses
 congruence closure for proof and type inference. We give a
 specification of a subset of the surface language via a
 bidirectional type system, which works ``uptocongruence'', and
 an algorithm for elaborating expressions in this language to an
 explicitly typed core language. We prove that our elaboration
 algorithm is complete with respect to the source type
 system. Zombie also features an optional terminationchecker,
 allowing nonterminating programs returning proofs as well as
 external proofs about programs.",
 paper = "Sjob15.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Cervesato, Iliano}
\index{Pfenning, Frank}
\begin{chunk}{axiom.bib}
@inproceedings{Cerv96,
 author = "Cervesato, Iliano and Pfenning, Frank",
 paper = {{A Linear Logical Framework}},
 booktitle = "Logic in Computer Science",
 publisher = "IEEE",
 year = "1996",
 abstract =
 "We present the linear type theory LLF as the formal basis for a
 conservative extension of the LF logical framework. LLF combines
 the expressive power of dependent types with linear logic to
 permit the natural and concise represention of a whole new class
 of deductive systems, names those dealing with state. As an
 example we encode a version of MiniML with references including
 its type system, its operational semantics, and a proof of type
 preservation. Another example is the encoding of a sequent
 calculus for classical linear logic and its cut elimination
 theorem. LLF can also be given an operational interpretation as a
 logic programming language under which the representations above
 can be used for type inference, evaluation and cutelimination.",
 paper = "Cerv96.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Cervesato, Iliano}
\index{Pfenning, Frank}
\begin{chunk}{axiom.bib}
@article{Cerv00,
 author = "Cervesato, Iliano and Pfenning, Frank",
 title = {{A Linear Logic Framework}},
 journal = "Information and Computation",
 volume = "179",
 number = "1",
 pages = "1975",
 link = "\url{http://www.cs.cmu.edu/~fp/papers/llf00.pdf}",
 year = "2002",
 abstract =
 "We present the linear type theory $\labmda^{\PIo\&\top}$ as the
 formal basis for LLF, a conservative extension of the logical
 framework LF. LLF combines the expressive power of dependent types
 with linear logic to permit the natural and concise representation
 of a whole new class of deductive systems, namely those dealing
 with state. As an example we encode a version of MiniML with
 mutable references including its type system and its operational
 semantics, and describe how to take practical advantage of the
 representation of its computations.",
 paper = "Cerv00.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Girard, JeanYves}
\begin{chunk}{axiom.bib}
@book{Gira95,
 author = "Girard, JeanYves",
 title = {{Linear Logic: Its Syntax and Semantics}},
 publisher = "Cambridge University Press",
 year = "1995",
 link = "\url{http://girard.perso.math.cnrs.fr/Synsem.pdf}",
 isbn = "9780521559614",
 paper = "Gira95.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Girard, JeanYves}
\begin{chunk}{axiom.bib}
@article{Gira87,
 author = "Girard, JeanYves",
 title = {{Linear Logic}},
 journal = "Theoretical Computer Science",
 volume = "50",
 year = "1987",
 pages = "1102"
 abstract =
 "The familiar connective of negation is broken into two
 operations: linear negation which is the purely negative part of
 negation and the modality ``of course'' which has the meaning of a
 reaffirmation. Following this basic discovery, a completely new
 approach to the whole area between constructive logics and
 programmation is initiated.",
 paper = "Gira87.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Knill, Oliver}
\begin{chunk}{axiom.bib}
@misc{Knil18,
 author = "Knill, Oliver",
 title = {{Some Fundamental Theorems in Mathematics}}
 link = "\url{https://arxiv.org/pdf/1807.08416.pdf}",
 year = "2018",
 abstract =
 "An expository hitchhikers guide to some theorems in mathematics",
 paper = "Knil18.pdf"
}

\end{chunk}

\index{Martzloff, J.C.}
\begin{chunk}{axiom.bib}
@book{Mart97a,
 author = "Martzloff, J.C.",
 title = {{A History of Chinese Mathematics}},
 publisher = "Springer Verlag",
 year = "1997"
}

\end{chunk}

\index{Ding, C.}
\index{Pei, D.}
\index{Salomaa, A.}
\begin{chunk}{axiom.bib}
@book{Ding96,
 author = "Ding, C. and Pei, D. and Salomaa, A.",
 title = {{Chinese Remainder Theorem, Applications in Computing,
 Coding Cryptography}},
 publisher = "World Scientific",
 year = "1996"
}

\end{chunk}

\index{Knill, Oliver}
\begin{chunk}{axiom.bib}
@misc{Knil12,
 author = "Knill, Oliver",
 title = {{A Multivariate Chinese Remainder Theorem}},
 link = "\url{https://arxiv.org/abs/1206.5114}",
 year = "2012"
 abstract =
 "Using an adaptation of Qin Jiushao's method from the 13th
 century, it is possible to prove that a system of linear modular
 equations $a(i,1)x(i)+a(i,n)x(n)=b(i)\bmod m(i),i=1,\ldots,n$ has
 integer solutions if $m(i)>1$ are pairwise relatively prime and in
 each row, at least one matrix element $a(i,j)$ is relatively prime
 to $m(i)$. The Chinese remainder theorem is a special case, where
 $A$ has only one column.",
 paper = "Knil12.pdf"
}

\end{chunk}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index ea9d912..1e37502 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5977,7 +5977,9 @@ books/bookvol13 add section
20181211.02.tpd.patch
src/input/kernel.input
20190131.01.tpd.patch
books/bookvolbib add references
+books/bookvolbib add references
+20190204.01.tpd.patch
+books/bookvol10.4 add documentation to CRAPACK

1.9.1