From 743b54c8516bc036abf5918aae021f037c316c0a Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Sun, 21 Jan 2018 21:17:18 0500
Subject: [PATCH] books/bookvolbib add references
Goal: Proving Axiom Correct
\index{Harper, Robert}
\begin{chunk}{axiom.bib}
@book{Harp11,
author = "Harper, Robert",
title = {{Programming in Standard ML}},
year = "2011",
publisher = "CMU",
keywords = "printed"
}
\end{chunk}
\index{Zippel, Richard}
\begin{chunk}{axiom.bib}
@book{Zipp92,
author = "Zippel, Richard",
title = {{Algebraic Computation}},
publisher = "Cornell University",
comment = "Unpublished",
year = "1992",
keywords = "axiomref, printed"
}
\end{chunk}
\index{Schwarz, Fritz}
\begin{chunk}{axiom.bib}
@article{Schw88,
author = "Schwarz, Fritz",
title = {{Symmetries of Differential Equations: From Sophus Lie to
Computer Algebra}},
journal = "SIAM Review",
volume = "30",
number = "3",
year = "1988",
abstract =
"The topic of this article is the symmetry analysis of
differential equations and the applications of computer algebra to
th extensive analytical calculations which are usually involved in
it. The whole area naturally decomposes into two parts depending
on whether ordinary or partial differential equations are
considered. We show how a symmetry may be applied to lower the
order of an ordinary differential equation or to obtain similarity
solutions of partial differential equations. The computer algebra
packages SODE and SPDE, respectively, which have been developed to
perform almost all algebraic manipulations necessary to determine
the symmetry group of a given differential equation, are
presented. Futhermore it is argued that the application of
computer algebra systems has qualitatively changed this area of
applied mathematics",
keywords = "axiomref, printed"
}
\end{chunk}
\index{Garcia, Ronald}
\index{Clark, Alison M.}
\index{Tanter, Eric}
\begin{chunk}{axiom.bib}
@inproceedings{Garc16,
author = "Garcia, Ronald and Clark, Alison M. and Tanter, Eric",
title = {{Abstracting Gradual Typing}},
booktitle = "POPL 16",
publisher = "ACM",
year = "2016",
pages = "429442",
abstract =
"Language researchers and designers have extended a wide variety
of type systems to support {\sl gradual typing}, which enables
languages to seemlessly combine dynamic and static checking. These
efforts consistently demonstrate that designing a satisfactory
gradual counterpart to a static type system is challenging, and
this challenge only increases with the sophistication of the type
system. Graudal type system designers need more formal tools to
help them conceptualize, structure, and evaluate their designs.
In this paper, we propose a new formal foundation for graudal
typing, drawing on principles from abstract interpretation to give
gradual types a semantics in terms of preexisting static
types. Abstracting Gradual Typing (AGT for short) yields a formal
account of {\sl consistency}  one of the cornerstones of the
gradual typing approach  that subsumes existing notions of
consistency, which were developed through intuition and ad hoc
reasoning.
Given a syntaxdirected static typing judgment, the AGT approach
induces a corresponding gradual typing judgment. Then the type
safety proof for the underlying static discipline induces a
dynamic semantics for gradual programs defined over
sourcelanguage typing derivations. The AGT approach does not
resort to an externally justified cast calculus; instead, runtime
check naturally arise by deducing evidence for consistent
judgements during proof reduction.
To illustrate the approach, we develop a novel graduallytyped
counterpart for a language with record subtyping. Gradual
languages designed with the AGT approach satisfy {\sl by
construction} the refined criteria for gradual typing set forth by
Siek and colleagues.",
keywords = "printed"
}
\end{chunk}
\index{Garcia, Ronald}
\index{Cimini, Matteo}
\begin{chunk}{axiom.bib}
@inproceedings{Garc17,
author = "Garcia, Ronald and Cimini, Matteo",
title = {{Principal Type Schemes for Gradual Programs}},
booktitle = "POPL 15",
comment = "Updated paper",
year = "2017",
abstract =
"Gradual typing is a discipline for integrating dynamic checking
into a static type system. Since its introduction in functional
languages, it has been adapted to a variety of type systems,
including objectoriented, security, and substructural. This work
studies its application to implictly typed languages based on type
inference. Siek and Vachharajani designed a gradual type inference
system and algorithm that infers gradual types but still rejects
illtyped static programs. However, the type system requires local
reasoning about type substitutions, an imperative inference
algorithm, and a subtle correctness statement.
This paper introduces a new approach to gradual type inference,
driven by the principle that gradual inference should only produce
static types. We present a static implicitly typed language, its
gradual counterpart, and a type inference procedure. The gradual
system types the same programs as Siek and Vachharajani, but has a
modular structure amenable to extension. The language admits
letpolymorphism, and its dynamics are defined by translation to
the Polymorphic Blame Calculus (Ahmed et al. 2009, 2011).
The principal types produced by our initial type system mask the
distinction between static parametric polymorphism and
polymorphism that can be attributed to gradual typing. To expose
this difference, we distinguish static type parameters from
gradual type parameters and reinterpret gradual type consistency
accordingly. The resulting extension enables programs to be
interpreted using either the polymorphic or monomorphic Blame
Calculi.",
keywords = "printed"
}
\end{chunk}
\index{Brady, Edwin}
\begin{chunk}{axiom.bib}
@article{Brad13,
author = "Brady, Edwin",
title = {{Idris, a General Purpose Dependently Typed Programming
Language: Design and Implementation}},
journal = "J. Functional Programming",
volume = "23",
number = "5",
year = "2013",
pages = "552593",
abstract =
"Many components of a dependently typed programming language are by
now well understood, for example, the underlying type theory, type
checking, unification and evaluation. How to combine these components
into a realistic and usable highlevel language is, however, folklore,
discovered anew by successive language implementors. In this paper, I
describe the implementation of Idris, a new dependently typed
functional programming language. Idris is intended to be a
generalpurpose programming language and as such provides highlevel
concepts such as implicit syntax, type classes and do notation. I
describe the highlevel language and the underlying type theory, and
present a tacticbased method for elaborating concrete highlevel
syntax with implicit arguments and type classes into a fully explicit
type theory. Furthermore, I show how this method facilitates the
implementation of new highlevel language constructs.",
keywords = "printed"
}
\end{chunk}

books/axiom.bib  390 +++++++++++++++++++++++++++++++
books/bookvolbib.pamphlet  418 +++++++++++++++++++++++++++++++++
changelog  2 +
patch  179 +++++++++++++++++
src/axiomwebsite/patches.html  2 +
5 files changed, 846 insertions(+), 145 deletions()
diff git a/books/axiom.bib b/books/axiom.bib
index 09cee7e..d376861 100644
 a/books/axiom.bib
+++ b/books/axiom.bib
@@ 843,7 +843,8 @@ paper = "Brea89.pdf"
number = "478",
institution = "Laboratoire de Recherche en Informatique",
link = "\url{http://www.cs.tau.ac.il/~nachum/papers/surveydraft.pdf}",
 paper = "Ders89.pdf"
+ paper = "Ders89.pdf",
+ keywords = "printed"
}
@book{Ehri85,
@@ 928,7 +929,8 @@ paper = "Brea89.pdf"
System. The paper also proposes a general mathematics laboratory that
combines the functionality of current symbolic computation systems
with the facilities of a theorem proving system like IMPS.",
 paper = "Farm95.pdf"
+ paper = "Farm95.pdf",
+ keywords = "printed"
}
@misc{Farm95a,
@@ 1712,7 +1714,7 @@ paper = "Brea89.pdf"
be solved within a single CAS, or may be organised into a system for
distributed parallel computations.",
paper = "Lint10.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
@article{Loos72,
@@ 1862,7 +1864,8 @@ paper = "Brea89.pdf"
publisher = "Lab for Foundations of Computer Science, Univ. Edinburgh",
link = "\url{http://smlfamily.org/sml97defn.pdf}",
year = "1997",
 paper = "Miln97.pdf"
+ paper = "Miln97.pdf",
+ keywords = "printed"
}
@book{Miln91,
@@ 1871,7 +1874,8 @@ paper = "Brea89.pdf"
publisher = "Lab for Foundations of Computer Science, Univ. Edinburgh",
link = "\url{https://pdfs.semanticscholar.org/d199/16cbbda01c06b6eafa0756416e8b6f15ff44.pdf}",
year = "1991",
 paper = "Miln91.pdf"
+ paper = "Miln91.pdf",
+ keywords = "printed"
}
@article{Mitc91,
@@ 2663,7 +2667,8 @@ paper = "Brea89.pdf"
not sufficient. One needs to preprocess the (closed, quantified)
conjectured formula and postprocess the resulting CADstructure after
the call of the QE algorithm.",
 paper = "Vajd09.pdf"
+ paper = "Vajd09.pdf",
+ keywords = "printed"
}
@techreport{Volp91,
@@ 3570,7 +3575,8 @@ paper = "Brea89.pdf"
journal = "Mathematics of Computation",
volume = "19",
number = "04",
 year = "1965"
+ year = "1965",
+ keywords = "printed"
}
@article{Dave17,
@@ 5943,7 +5949,7 @@ paper = "Brea89.pdf"
represented by potentially infinite lists of binary digits, and
interpreted as sums of negative powers of the golden ratio.",
paper = "Kels00.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
@article{Knus98,
@@ 6915,7 +6921,8 @@ paper = "Brea89.pdf"
some of these analogies precise using the concept of ``closed
symmetric monodial category''. We assume no prior knowledge of
category theory, proof theory or computer science.",
 paper = "Baez09.pdf"
+ paper = "Baez09.pdf",
+ keywords = "printed"
}
@misc{Meij91,
@@ 7045,7 +7052,8 @@ paper = "Brea89.pdf"
Provers, and is not self contained . In particular, it requires good
acquaintance with Type Theory and functional programming
languages.",
 paper = "Aspe09.pdf"
+ paper = "Aspe09.pdf",
+ keywords = "printed"
}
@article{Aspe09a,
@@ 7535,7 +7543,8 @@ paper = "Brea89.pdf"
investigate the relationship between the two translations, identifying
the amount of proof structure preserved by compilation and
regeneration of declarative scripts.",
 paper = "Coen10.pdf"
+ paper = "Coen10.pdf",
+ keywords = "printed"
}
@inproceedings{Coen11,
@@ 7873,7 +7882,8 @@ paper = "Brea89.pdf"
is adequate for type theories with canonical objects while the latter
is not. An improved implementation of coercive subtyping is done in
the proof assistant Plastic.",
 paper = "Luox13.pdf"
+ paper = "Luox13.pdf",
+ keywords = "printed"
}
@inproceedings{Hall94,
@@ 8557,7 +8567,8 @@ paper = "Brea89.pdf"
programs (for Algebraic Topology) by using the Isabelle proof
assistant. To ease the understanding of our techniques, they are
illustrated by means of examples in elementary arithmetic.",
 paper = "Aran05.pdf"
+ paper = "Aran05.pdf",
+ keywords = "printed"
}
@inproceedings{Arch93,
@@ 9524,7 +9535,8 @@ paper = "Brea89.pdf"
synthesis of an algorithm for the construction of Groebner Bases) and
gives an overview on some reasoners and organizational tools for
theory exploration developed in the Theorema project.",
 paper = "Buch06.pdf"
+ paper = "Buch06.pdf",
+ keywords = "printed"
}
@misc{Buch03,
@@ 9584,7 +9596,8 @@ paper = "Brea89.pdf"
her preferred flavour of doing math. The new implementation of the
system, which we refer to as Theorema 2.0, is opensource and
available through GitHub.",
 paper = "Buch16.pdf"
+ paper = "Buch16.pdf",
+ keywords = "printed"
}
@article{Bulo04,
@@ 9840,7 +9853,8 @@ paper = "Brea89.pdf"
frame work is robust with respect to interface extension and can
process requests for abstract services, where the server interface is
not fully specified.",
 paper = "Care11b.pdf"
+ paper = "Care11b.pdf",
+ keywords = "printed"
}
@article{Chli10,
@@ 9940,7 +9954,9 @@ paper = "Brea89.pdf"
a series of three lemmas that lead to a proof of Weierstrass's
example of a continuous nowhere differentiable function. Each of
the lemmas in the latter example is proved completely
 automatically."
+ automatically.",
+ paper = "Clar93.pdf",
+ keywords = "printed"
}
@article{Clem91,
@@ 10228,7 +10244,7 @@ paper = "Brea89.pdf"
comment = "BPR presentation, Cambridge, England",
video = "Dave17a.mp4",
paper = "Dave17a.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
@article{Dela05,
@@ 10255,7 +10271,8 @@ paper = "Brea89.pdf"
and can be very easily extended to get other Maple functions (in
addition to the four functions we have imported and used in the
examples given here).",
 paper = "Dela05.pdf"
+ paper = "Dela05.pdf",
+ keywords = "printed"
}
@article{Demi79,
@@ 10454,7 +10471,7 @@ paper = "Brea89.pdf"
available and describe the changes which would need to be made to
the compiler to make use of this technology.",
paper = "Duns00.pdf",
 keywords = "axiomref"
+ keywords = "axiomref, printed"
}
@InProceedings{Duns98,
@@ 10473,7 +10490,7 @@ paper = "Brea89.pdf"
methodology for Aldor program analysis and verification. There are
examples of abstract specifications of Axiom primitives.",
paper = "Duns98.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@phdthesis{Duns99a,
@@ 10493,7 +10510,7 @@ paper = "Brea89.pdf"
generator and review our implementation of a prototype verification
condition generator for Larch/Aldor.",
paper = "Duns99a.pdf",
 keywords = "axiomref"
+ keywords = "axiomref, printed"
}
@InProceedings{Duns99,
@@ 10513,7 +10530,7 @@ paper = "Brea89.pdf"
case study of abstract specifications of AXIOM primitives, and provide
an interface between these abstractions and Aldor code.",
paper = "Duns99.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@article{Farm92a,
@@ 10789,7 +10806,8 @@ paper = "Brea89.pdf"
number = "4",
year = "1964",
pages = "288306",
 paper = "Gent64.pdf"
+ paper = "Gent64.pdf",
+ keywords = "printed"
}
@article{Gent65,
@@ 10860,7 +10878,7 @@ paper = "Brea89.pdf"
practice. Apart rom the inheritance and reuse of properties, the
algebraic hierarchy has proven very useful for reusing notations.",
paper = "Geuv02.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@misc{Gime16,
@@ 11095,6 +11113,14 @@ paper = "Brea89.pdf"
paper = "Hard14.pdf"
}
+@book{Harp11,
+ author = "Harper, Robert",
+ title = {{Programming in Standard ML}},
+ year = "2011",
+ publisher = "CMU",
+ keywords = "printed"
+}
+
@misc{Harp13,
author = "Harper, Robert",
title = {{15.819 Homotopy Type Theory Course}},
@@ 11242,7 +11268,8 @@ paper = "Brea89.pdf"
well suited to the kind of work we describe. We hope also to convince
the reader that the kind of mathematics needed for applications is
well within the abilities of current theorem proving technology.",
 paper = "Harr96.pdf"
+ paper = "Harr96.pdf",
+ keywords = "printed"
}
@misc{Harr06a,
@@ 11488,7 +11515,7 @@ paper = "Brea89.pdf"
discusses the appropriateness of this foundation, and the extent to
which the work relied on it.",
paper = "Jack95.pdf",
 keyword = "axiomref, CASProof"
+ keyword = "axiomref, CASProof, printed"
}
@book{Jone93,
@@ 11680,7 +11707,8 @@ paper = "Brea89.pdf"
volume = "22",
number = "7",
year = "1979",
 paper = "Kowa79.pdf"
+ paper = "Kowa79.pdf",
+ keywords = "printed"
}
@inproceedings{Koun90,
@@ 11922,7 +11950,8 @@ paper = "Brea89.pdf"
implementations in Intel’s math library automatically. Prior to this
work, these implementations could only be verified with significant
manual effort.",
 paper = "Wony18.pdf"
+ paper = "Wony18.pdf",
+ keywords = "printed"
}
@misc{Lond74,
@@ 12032,7 +12061,8 @@ paper = "Brea89.pdf"
this is heavily inspired by the Isabelle proof assistant, we in
particular also highlight the differences between Isabelle and our
approach.",
 paper = "Male17.pdf"
+ paper = "Male17.pdf",
+ keywords = "printed"
}
@article{Male16,
@@ 12306,7 +12336,8 @@ paper = "Brea89.pdf"
title = {{Term rewriting, Equationional Reasoning, Automatic proofs}},
link = "\url{ftp://ftp.botik.ru/pub/local/Mechveliani/dumatel/1.02/}",
year = "2005",
 paper = "Mesh05.pdf"
+ paper = "Mesh05.pdf",
+ keywords = "printed"
}
@misc{Mesh13,
@@ 13203,7 +13234,7 @@ paper = "Brea89.pdf"
a prototype implementation of a modified typechecking system written
in Haskell.",
paper = "P0ll00.pdf",
 keywords = "axiomref"
+ keywords = "axiomref, printed"
}
@InProceedings{Poll00a,
@@ 13254,7 +13285,7 @@ paper = "Brea89.pdf"
into OCAML and COQ, our target languages for the computational part
and the proof checking, respectively.",
paper = "Prev02.pdf",
 keywords = "axiomref"
+ keywords = "axiomref, printed"
}
#InCollection{Rect89,
@@ 13402,7 +13433,7 @@ paper = "Brea89.pdf"
given algorithm a set of theorems that imply the correctness of this
algorithm.",
paper = "Schw97.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@techreport{Sege91,
@@ 13702,7 +13733,8 @@ paper = "Brea89.pdf"
it satisfies. Every function of the same type satisfies the same
theorem. This provides a free source of useful theorems, courtesy of
Reynolds' abstraction theorem for the polymorphic lambda calculus.",
 paper = "Wadl89.pdf"
+ paper = "Wadl89.pdf",
+ keywords = "printed"
}
@misc{Wadl14,
@@ 14312,7 +14344,8 @@ paper = "Brea89.pdf"
its search for solutions in the monoid. It is both very efficient and
easily verifiable. Some applications of this algorithm are shown in
the appendix.",
 paper = "Fort87.pdf"
+ paper = "Fort87.pdf",
+ keywords = "printed"
}
@inproceedings{Cavi76,
@@ 15088,6 +15121,32 @@ paper = "Brea89.pdf"
year = "1953"
}
+@article{Mose71,
+ author = "Moses, Joel",
+ title = {{Symbolic Integration: The Stormy Decade}},
+ journal = "CACM",
+ year = "1971",
+ volume = "14",
+ number = "8",
+ pages = "548560",
+ link =
+ "\url{http://wwwinst.eecs.berkeley.edu/~cs282/sp02/readings/mosesint.pdf}",
+ abstract =
+ "Three approaches to symbolic integration in the 1960's are
+ described. The first, from artificial intelligence, led to Slagle's
+ SAINT and to a large degree to Moses' SIN. The second, from algebraic
+ manipulation, led to Monove's implementation and to Horowitz' and
+ Tobey's reexamination of the Hermite algorithm for integrating
+ rational functions. The third, from mathematics, led to Richardson's
+ proof of the unsolvability of the problem for a class of functions and
+ for Risch's decision procedure for the elementary functions.
+ Generalizations of Risch's algorithm to a class of special
+ functions and programs for solving differential equations and for
+ finding the definite integral are also described.",
+ paper = "Mos71a.pdf",
+ keywords = "printed"
+}
+
@article{Ngxx74,
author = "Ng, Edward W.",
title = {{Symbolic Integration of a Class of Algebraic Functions}},
@@ 15838,7 +15897,8 @@ paper = "Brea89.pdf"
problem is far harder, and several major questions remain to be
answered. Nevertheless, the last few years have seen substantial
improvements, and such factorisations are now possible",
 paper = "Abbo87.pdf"
+ paper = "Abbo87.pdf",
+ keywords = "printed"
}
@InProceedings{Bern97a,
@@ 23504,7 +23564,7 @@ paper = "Brea89.pdf"
year = "1987",
pages = "211",
paper = "Calm87.pdf",
 keywords = "axiomref"
+ keywords = "axiomref, printed"
}
@article{Calm97,
@@ 24344,7 +24404,8 @@ paper = "Brea89.pdf"
title = {{A Small OpenMath Type System}},
year = "1999",
link = "\url{https://www.openmath.org/standard/sts.pdf}",
 paper = "Dave99.pdf"
+ paper = "Dave99.pdf",
+ keywords = "printed"
}
@book{Dave05,
@@ 25324,7 +25385,7 @@ paper = "Brea89.pdf"
isbn = "1581130732",
link = "\url{http://www.acm.org/citation.cfm?id=309944}",
paper = "Doye99.pdf",
 keywords = "axiomref",
+ keywords = "axiomref, printed",
beebe = "Doye:1999:ACA"
}
@@ 27839,7 +27900,7 @@ paper = "Brea89.pdf"
a highlevel programming language, both for the formal description of
mathematical algorithms and their efficient implementation.",
paper = "Jenk74.pdf",
 keywords = "axiomref",
+ keywords = "axiomref, printed",
beebe = "Jenks:1974:SL"
}
@@ 28103,7 +28164,7 @@ paper = "Brea89.pdf"
polymorphic packages of functions that may create datatypes. The use
of categories makes these facilities as general as possible.",
paper = "Jenk86.pdf",
 keywords = "axiomref",
+ keywords = "axiomref, printed",
beebe = "Jenks:1986:SIA"
}
@@ 29193,7 +29254,7 @@ paper = "Brea89.pdf"
shown how some complex problems in homologicial algebra were solved
through the use of this system.",
paper = "Lamb92.pdf",
 keywords = "axiomref",
+ keywords = "axiomref, printed",
beebe = "Lambe:1994:NGC"
}
@@ 29450,7 +29511,7 @@ paper = "Brea89.pdf"
year = "1996",
link = "\url{http://lecerf.perso.math.cnrs.fr/software/drc/drc.ps}",
paper = "Lece96.pdf",
 keywords = "axiomref"
+ keywords = "axiomref, printed"
}
@article{Leeu94,
@@ 30218,6 +30279,27 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@misc{Miss94,
+ author = "Missura, Stephan A. and Weber, Andreas",
+ title = {{Using Commutativity Properties for Controlling Coercions}},
+ link = "\url{http://cg.cs.unibonn.de/personalpages/weber/publications/pdf/WeberA/MissuraWeber94a.pdf}",
+ abstract =
+ "This paper investigates some soundness conditions which have to be
+ fulfilled in systems with coercions and generic operators. A result of
+ Reynolds on unrestricted generic operators is extended to generic
+ operators which obey certain constraints. We get natural conditions
+ for such operators, which are expressed within the theoretic framework
+ of category theory. However, in the context of computer algebra, there
+ arise examples of coercions and generic operators which do not fulfil
+ these conditions. We describe a framework  relaxing the above
+ conditions  that allows distinguishing between cases of ambiguities
+ which can be resolved in a quite natural sense and those which
+ cannot. An algorithm is presented that detects such unresolvable
+ ambiguities in expressions.",
+ paper = "Miss94.pdf",
+ keywords = "axiomref, printed"
+}
+
@inproceedings{Mona93,
author = "Monagan, Michael B.",
title = {{Gauss: a parameterized domain of computation system with
@@ 30469,7 +30551,7 @@ paper = "Brea89.pdf"
pages = "1220",
year = "1975",
comment = "IBM T.J. Watson Research RC4998",
 keywords = "axiomref"
+ keywords = "axiomref, printed"
}
@misc{Norm94,
@@ 31110,7 +31192,7 @@ paper = "Brea89.pdf"
concepts. The full calculus has been implemented and tested with our
LA compiler which generates executable files.",
paper = "Sant96.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@book{Sant05,
@@ 31184,7 +31266,7 @@ paper = "Brea89.pdf"
differential equations and the Scratchpad package SPDE which
abbreviates Symmetries of Partial Differential Equations.",
paper = "Schw87.pdf",
 keywords = "axiomref",
+ keywords = "axiomref, printed",
beebe = "Schwarz:1988:PAD"
}
@@ 31848,7 +31930,7 @@ paper = "Brea89.pdf"
conveniently define a quote function, thus facilitating the use of
reflective techniques.",
paper = "Spit11.pdf",
 keywords = "axiomref"
+ keywords = "axiomref, printed"
}
@InProceedings{Schu92,
@@ 32868,7 +32950,7 @@ paper = "Brea89.pdf"
computer algebra whose coercion relations cannot be captured by a
finite set of firstorder rewrite rules.",
paper = "Webe05.pdf",
 keywords = "axiomref, coercion"
+ keywords = "axiomref, coercion, printed"
}
@Inproceedings{Webe94,
@@ 33272,6 +33354,15 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@book{Zipp92a,
+ author = "Zippel, Richard",
+ title = {{Algebraic Computation}},
+ publisher = "Cornell University",
+ comment = "Unpublished",
+ year = "1992",
+ keywords = "axiomref, printed"
+}
+
@misc{Zipp89,
author = "Zippel, Richard",
title = {{The Weyl Computer Algebra Substrate}},
@@ 33370,6 +33461,14 @@ paper = "Brea89.pdf"
comment = "STD1815A1983"
}
+@misc{Adam17,
+ author = "Adamchik, Victor",
+ title = {{Modern Computer Algebra}},
+ comment = "Carnegie Mellon SCS 15355",
+ year = "2017",
+ keywords = "printed"
+}
+
@book{Altm05,
author = "Altmann, Simon L.",
title = {{Rotations, Quaternions, and Double Groups}},
@@ 33763,7 +33862,8 @@ paper = "Brea89.pdf"
volume = "1158",
year = "1995",
pages = "3646",
 paper = "Berg95.pdf"
+ paper = "Berg95.pdf",
+ keywords = "printed"
}
@misc{Bern85,
@@ 33931,6 +34031,33 @@ paper = "Brea89.pdf"
year = "1992"
}
+@article{Brad13,
+ author = "Brady, Edwin",
+ title = {{Idris, a General Purpose Dependently Typed Programming
+ Language: Design and Implementation}},
+ journal = "J. Functional Programming",
+ volume = "23",
+ number = "5",
+ year = "2013",
+ pages = "552593",
+ abstract =
+ "Many components of a dependently typed programming language are by
+ now well understood, for example, the underlying type theory, type
+ checking, unification and evaluation. How to combine these components
+ into a realistic and usable highlevel language is, however, folklore,
+ discovered anew by successive language implementors. In this paper, I
+ describe the implementation of Idris, a new dependently typed
+ functional programming language. Idris is intended to be a
+ generalpurpose programming language and as such provides highlevel
+ concepts such as implicit syntax, type classes and do notation. I
+ describe the highlevel language and the underlying type theory, and
+ present a tacticbased method for elaborating concrete highlevel
+ syntax with implicit arguments and type classes into a fully explicit
+ type theory. Furthermore, I show how this method facilitates the
+ implementation of new highlevel language constructs.",
+ keywords = "printed"
+}
+
@article{Bram02a,
author = "Braman, Karen and Byers, Ralph and Mathias, Roy",
title = {{The MultiShift QR Algorithm Part I: Maintaining Well Focused
@@ 33975,6 +34102,13 @@ paper = "Brea89.pdf"
}
+@misc{Bren10,
+ author = "Brent, Richard P. and Zimmermann, Paul",
+ title = {{Modern Computer Arithmetic}},
+ year = "2010",
+ keywords = "printed"
+}
+
@misc{Bron95,
author = "Bronstein, Manuel",
title = {{On radical solutions of linear ordinary differential equations}},
@@ 34111,7 +34245,8 @@ paper = "Brea89.pdf"
geometrical theorem proving, primary decompsotion of implicitly
defined geometrical objects). The paper starts with a brief summary of
the Groebner bases method.",
 paper = "Buch87.pdf"
+ paper = "Buch87.pdf",
+ keywords = "printed"
}
@inproceedings{Buch97a,
@@ 34582,7 +34717,8 @@ paper = "Brea89.pdf"
error situations. The soundness and meaning of the major concepts
involed in rewriting systems are reviewed when applied to such
structures.",
 paper = "Cunn85.pdf"
+ paper = "Cunn85.pdf",
+ keywords = "printed"
}
@misc{Dave80b,
@@ 34668,7 +34804,8 @@ paper = "Brea89.pdf"
effective quantier elimination and simplication of quantierfree
formulas, REDLOG is intended and designed as an allpurpose system.
REDLOG is freely available to the scientic community.",
 paper = "Dolz96.pdf"
+ paper = "Dolz96.pdf",
+ keywords = "printed"
}
@article{Dolz97b,
@@ 34743,7 +34880,7 @@ paper = "Brea89.pdf"
booktitle = "Proc. Calculemus, 2001",
year = "2001",
paper = "Duns01.pdf",
 keywords = "axiomref, CASproof"
+ keywords = "axiomref, CASproof, printed"
}
@article{Dute96,
@@ 35085,6 +35222,87 @@ paper = "Brea89.pdf"
paper = "Fult08.pdf"
}
+@inproceedings{Garc16,
+ author = "Garcia, Ronald and Clark, Alison M. and Tanter, Eric",
+ title = {{Abstracting Gradual Typing}},
+ booktitle = "POPL 16",
+ publisher = "ACM",
+ year = "2016",
+ pages = "429442",
+ abstract =
+ "Language researchers and designers have extended a wide variety
+ of type systems to support {\sl gradual typing}, which enables
+ languages to seemlessly combine dynamic and static checking. These
+ efforts consistently demonstrate that designing a satisfactory
+ gradual counterpart to a static type system is challenging, and
+ this challenge only increases with the sophistication of the type
+ system. Graudal type system designers need more formal tools to
+ help them conceptualize, structure, and evaluate their designs.
+
+ In this paper, we propose a new formal foundation for graudal
+ typing, drawing on principles from abstract interpretation to give
+ gradual types a semantics in terms of preexisting static
+ types. Abstracting Gradual Typing (AGT for short) yields a formal
+ account of {\sl consistency}  one of the cornerstones of the
+ gradual typing approach  that subsumes existing notions of
+ consistency, which were developed through intuition and ad hoc
+ reasoning.
+
+ Given a syntaxdirected static typing judgment, the AGT approach
+ induces a corresponding gradual typing judgment. Then the type
+ safety proof for the underlying static discipline induces a
+ dynamic semantics for gradual programs defined over
+ sourcelanguage typing derivations. The AGT approach does not
+ resort to an externally justified cast calculus; instead, runtime
+ check naturally arise by deducing evidence for consistent
+ judgements during proof reduction.
+
+ To illustrate the approach, we develop a novel graduallytyped
+ counterpart for a language with record subtyping. Gradual
+ languages designed with the AGT approach satisfy {\sl by
+ construction} the refined criteria for gradual typing set forth by
+ Siek and colleagues.",
+ keywords = "printed"
+}
+
+@inproceedings{Garc17,
+ author = "Garcia, Ronald and Cimini, Matteo",
+ title = {{Principal Type Schemes for Gradual Programs}},
+ booktitle = "POPL 15",
+ comment = "Updated paper",
+ year = "2017",
+ abstract =
+ "Gradual typing is a discipline for integrating dynamic checking
+ into a static type system. Since its introduction in functional
+ languages, it has been adapted to a variety of type systems,
+ including objectoriented, security, and substructural. This work
+ studies its application to implictly typed languages based on type
+ inference. Siek and Vachharajani designed a gradual type inference
+ system and algorithm that infers gradual types but still rejects
+ illtyped static programs. However, the type system requires local
+ reasoning about type substitutions, an imperative inference
+ algorithm, and a subtle correctness statement.
+
+ This paper introduces a new approach to gradual type inference,
+ driven by the principle that gradual inference should only produce
+ static types. We present a static implicitly typed language, its
+ gradual counterpart, and a type inference procedure. The gradual
+ system types the same programs as Siek and Vachharajani, but has a
+ modular structure amenable to extension. The language admits
+ letpolymorphism, and its dynamics are defined by translation to
+ the Polymorphic Blame Calculus (Ahmed et al. 2009, 2011).
+
+ The principal types produced by our initial type system mask the
+ distinction between static parametric polymorphism and
+ polymorphism that can be attributed to gradual typing. To expose
+ this difference, we distinguish static type parameters from
+ gradual type parameters and reinterpret gradual type consistency
+ accordingly. The resulting extension enables programs to be
+ interpreted using either the polymorphic or monomorphic Blame
+ Calculi.",
+ keywords = "printed"
+}
+
@misc{Gari09,
author = "Garillot, Francois and Gonthier, Georges and Mahboubi, Assia and
Rideau, Laurence",
@@ 35141,7 +35359,9 @@ paper = "Brea89.pdf"
title = {{Proofs and Types}},
publisher = "Cambridge University Press",
link = "\url{http://www.paultaylor.eu/stable/prot.pdf}",
 year = "2003"
+ year = "2003",
+ paper = "Gira03.pdf",
+ keywords = "printed"
}
@misc{Gode16,
@@ 35261,7 +35481,8 @@ paper = "Brea89.pdf"
semantics. These extensions provide a purely equational proof system
to prove properties of functional programs over userdefinable data
types.",
 paper = "Gues87.pdf"
+ paper = "Gues87.pdf",
+ keywords = "printed"
}
@techreport{Gutt91,
@@ 35341,7 +35562,8 @@ paper = "Brea89.pdf"
type classes, and supports further applications, such as code
generation and export of theories and theorems to environments without
type classes.",
 paper = "Haft06.pdf"
+ paper = "Haft06.pdf",
+ keywords = "printed"
}
@misc{Hall17,
@@ 35379,7 +35601,8 @@ paper = "Brea89.pdf"
declarative and procedural styles for proofs in pure mathematics and
for verification applications. We conclude with a brief summary of
our own experiments in trying to combine both approaches.",
 paper = "Harr06.pdf"
+ paper = "Harr06.pdf",
+ keywords = "printed"
}
@inproceedings{Harr07,
@@ 36235,7 +36458,8 @@ paper = "Brea89.pdf"
volume = "296",
year = "1987",
pages = "3851",
 paper = "Lesc97.pdf"
+ paper = "Lesc87.pdf",
+ keywords = "printed"
}
@misc{Leop03,
@@ 36711,7 +36935,7 @@ paper = "Brea89.pdf"
of the Prosper project and provides a summary of the technical
approach taken and some of the lessons learned.",
paper = "Melh02.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
@article{Mill68,
@@ 36727,7 +36951,8 @@ paper = "Brea89.pdf"
to display mathematical expressions on typewriterlike devices such as
line printers, teletypes, and scopes which display lines of characters,
as well as typewriters.",
 paper = "Mill68.pdf"
+ paper = "Mill68.pdf",
+ keywords = "printed"
}
@book{Mine88,
@@ 36985,7 +37210,8 @@ paper = "Brea89.pdf"
formally constructed. Isabelle proof procedures are described. The
logic appears suitable for general mathematics as well as
computational problems.",
 paper = "Paul90.pdf"
+ paper = "Paul90.pdf",
+ keywords = "printed"
}
@book{Pear56,
@@ 37444,7 +37670,8 @@ paper = "Brea89.pdf"
give some thoughts on possible combinations of all three methods to
obtain algorithms benefitting from the specific strength of either
method.",
 paper = "Rump88.pdf"
+ paper = "Rump88.pdf",
+ keywords = "printed"
}
@inproceedings{Rush00,
@@ 37600,6 +37827,43 @@ paper = "Brea89.pdf"
paper = "Schr14.pdf"
}
+@article{Schw85,
+ author = "Schwarz, Fritz",
+ title = {{An Algorithm for Determining Polynomial First Integrals of
+ Autonomous Systems of Ordinary Differential Equations}},
+ journal = "J. Symbolic Computation",
+ volume = "1",
+ year = "1985",
+ pages = "229233",
+ paper = "Schw85.pdf"
+}
+
+@article{Schw88,
+ author = "Schwarz, Fritz",
+ title = {{Symmetries of Differential Equations: From Sophus Lie to
+ Computer Algebra}},
+ journal = "SIAM Review",
+ volume = "30",
+ number = "3",
+ year = "1988",
+ abstract =
+ "The topic of this article is the symmetry analysis of
+ differential equations and the applications of computer algebra to
+ th extensive analytical calculations which are usually involved in
+ it. The whole area naturally decomposes into two parts depending
+ on whether ordinary or partial differential equations are
+ considered. We show how a symmetry may be applied to lower the
+ order of an ordinary differential equation or to obtain similarity
+ solutions of partial differential equations. The computer algebra
+ packages SODE and SPDE, respectively, which have been developed to
+ perform almost all algebraic manipulations necessary to determine
+ the symmetry group of a given differential equation, are
+ presented. Futhermore it is argued that the application of
+ computer algebra systems has qualitatively changed this area of
+ applied mathematics",
+ keywords = "axiomref, printed"
+}
+
@misc{SCSCP,
author = "The SCSCP development team",
title = {{Symbolic Computation Software Composability Protocol}},
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index dd2df56..1cedf33 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 1340,7 +1340,8 @@ paper = "Brea89.pdf"
number = "478",
institution = "Laboratoire de Recherche en Informatique",
link = "\url{http://www.cs.tau.ac.il/~nachum/papers/surveydraft.pdf}",
 paper = "Ders89.pdf"
+ paper = "Ders89.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 1449,7 +1450,8 @@ paper = "Brea89.pdf"
System. The paper also proposes a general mathematics laboratory that
combines the functionality of current symbolic computation systems
with the facilities of a theorem proving system like IMPS.",
 paper = "Farm95.pdf"
+ paper = "Farm95.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 2487,7 +2489,7 @@ paper = "Brea89.pdf"
be solved within a single CAS, or may be organised into a system for
distributed parallel computations.",
paper = "Lint10.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
\end{chunk}
@@ 2694,7 +2696,8 @@ paper = "Brea89.pdf"
publisher = "Lab for Foundations of Computer Science, Univ. Edinburgh",
link = "\url{http://smlfamily.org/sml97defn.pdf}",
year = "1997",
 paper = "Miln97.pdf"
+ paper = "Miln97.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 2708,7 +2711,8 @@ paper = "Brea89.pdf"
publisher = "Lab for Foundations of Computer Science, Univ. Edinburgh",
link = "\url{https://pdfs.semanticscholar.org/d199/16cbbda01c06b6eafa0756416e8b6f15ff44.pdf}",
year = "1991",
 paper = "Miln91.pdf"
+ paper = "Miln91.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 3712,7 +3716,8 @@ paper = "Brea89.pdf"
not sufficient. One needs to preprocess the (closed, quantified)
conjectured formula and postprocess the resulting CADstructure after
the call of the QE algorithm.",
 paper = "Vajd09.pdf"
+ paper = "Vajd09.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 5034,7 +5039,8 @@ when shown in factored form.
journal = "Mathematics of Computation",
volume = "19",
number = "04",
 year = "1965"
+ year = "1965",
+ keywords = "printed"
}
\end{chunk}
@@ 8114,7 +8120,7 @@ when shown in factored form.
represented by potentially infinite lists of binary digits, and
interpreted as sums of negative powers of the golden ratio.",
paper = "Kels00.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
\end{chunk}
@@ 9402,7 +9408,8 @@ when shown in factored form.
some of these analogies precise using the concept of ``closed
symmetric monodial category''. We assume no prior knowledge of
category theory, proof theory or computer science.",
 paper = "Baez09.pdf"
+ paper = "Baez09.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 9578,7 +9585,8 @@ when shown in factored form.
Provers, and is not self contained . In particular, it requires good
acquaintance with Type Theory and functional programming
languages.",
 paper = "Aspe09.pdf"
+ paper = "Aspe09.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 10166,7 +10174,8 @@ when shown in factored form.
investigate the relationship between the two translations, identifying
the amount of proof structure preserved by compilation and
regeneration of declarative scripts.",
 paper = "Coen10.pdf"
+ paper = "Coen10.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 10589,7 +10598,8 @@ when shown in factored form.
is adequate for type theories with canonical objects while the latter
is not. An improved implementation of coercive subtyping is done in
the proof assistant Plastic.",
 paper = "Luox13.pdf"
+ paper = "Luox13.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 11444,7 +11454,8 @@ when shown in factored form.
programs (for Algebraic Topology) by using the Isabelle proof
assistant. To ease the understanding of our techniques, they are
illustrated by means of examples in elementary arithmetic.",
 paper = "Aran05.pdf"
+ paper = "Aran05.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 12667,7 +12678,8 @@ when shown in factored form.
synthesis of an algorithm for the construction of Groebner Bases) and
gives an overview on some reasoners and organizational tools for
theory exploration developed in the Theorema project.",
 paper = "Buch06.pdf"
+ paper = "Buch06.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 12751,7 +12763,8 @@ when shown in factored form.
her preferred flavour of doing math. The new implementation of the
system, which we refer to as Theorema 2.0, is opensource and
available through GitHub.",
 paper = "Buch16.pdf"
+ paper = "Buch16.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 13096,7 +13109,8 @@ when shown in factored form.
frame work is robust with respect to interface extension and can
process requests for abstract services, where the server interface is
not fully specified.",
 paper = "Care11b.pdf"
+ paper = "Care11b.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 13225,7 +13239,9 @@ when shown in factored form.
a series of three lemmas that lead to a proof of Weierstrass's
example of a continuous nowhere differentiable function. Each of
the lemmas in the latter example is proved completely
 automatically."
+ automatically.",
+ paper = "Clar93.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 13619,7 +13635,7 @@ when shown in factored form.
comment = "BPR presentation, Cambridge, England",
video = "Dave17a.mp4",
paper = "Dave17a.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
\end{chunk}
@@ 13651,7 +13667,8 @@ when shown in factored form.
and can be very easily extended to get other Maple functions (in
addition to the four functions we have imported and used in the
examples given here).",
 paper = "Dela05.pdf"
+ paper = "Dela05.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 13913,7 +13930,7 @@ when shown in factored form.
available and describe the changes which would need to be made to
the compiler to make use of this technology.",
paper = "Duns00.pdf",
 keywords = "axiomref"
+ keywords = "axiomref, printed"
}
\end{chunk}
@@ 13939,7 +13956,7 @@ when shown in factored form.
methodology for Aldor program analysis and verification. There are
examples of abstract specifications of Axiom primitives.",
paper = "Duns98.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 13963,7 +13980,7 @@ when shown in factored form.
generator and review our implementation of a prototype verification
condition generator for Larch/Aldor.",
paper = "Duns99a.pdf",
 keywords = "axiomref"
+ keywords = "axiomref, printed"
}
\end{chunk}
@@ 13990,7 +14007,7 @@ when shown in factored form.
case study of abstract specifications of AXIOM primitives, and provide
an interface between these abstractions and Aldor code.",
paper = "Duns99.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 14357,7 +14374,8 @@ when shown in factored form.
number = "4",
year = "1964",
pages = "288306",
 paper = "Gent64.pdf"
+ paper = "Gent64.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 14443,7 +14461,7 @@ when shown in factored form.
practice. Apart rom the inheritance and reuse of properties, the
algebraic hierarchy has proven very useful for reusing notations.",
paper = "Geuv02.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 14765,6 +14783,18 @@ when shown in factored form.
\index{Harper, Robert}
\begin{chunk}{axiom.bib}
+@book{Harp11,
+ author = "Harper, Robert",
+ title = {{Programming in Standard ML}},
+ year = "2011",
+ publisher = "CMU",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Harper, Robert}
+\begin{chunk}{axiom.bib}
@misc{Harp13,
author = "Harper, Robert",
title = {{15.819 Homotopy Type Theory Course}},
@@ 14934,7 +14964,8 @@ when shown in factored form.
well suited to the kind of work we describe. We hope also to convince
the reader that the kind of mathematics needed for applications is
well within the abilities of current theorem proving technology.",
 paper = "Harr96.pdf"
+ paper = "Harr96.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 15234,7 +15265,7 @@ when shown in factored form.
discusses the appropriateness of this foundation, and the extent to
which the work relied on it.",
paper = "Jack95.pdf",
 keyword = "axiomref, CASProof"
+ keyword = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 15481,7 +15512,8 @@ when shown in factored form.
volume = "22",
number = "7",
year = "1979",
 paper = "Kowa79.pdf"
+ paper = "Kowa79.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 15790,7 +15822,8 @@ when shown in factored form.
implementations in Intel’s math library automatically. Prior to this
work, these implementations could only be verified with significant
manual effort.",
 paper = "Wony18.pdf"
+ paper = "Wony18.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 15922,7 +15955,8 @@ when shown in factored form.
this is heavily inspired by the Isabelle proof assistant, we in
particular also highlight the differences between Isabelle and our
approach.",
 paper = "Male17.pdf"
+ paper = "Male17.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 16271,7 +16305,8 @@ when shown in factored form.
title = {{Term rewriting, Equationional Reasoning, Automatic proofs}},
link = "\url{ftp://ftp.botik.ru/pub/local/Mechveliani/dumatel/1.02/}",
year = "2005",
 paper = "Mesh05.pdf"
+ paper = "Mesh05.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 17385,7 +17420,7 @@ when shown in factored form.
a prototype implementation of a modified typechecking system written
in Haskell.",
paper = "P0ll00.pdf",
 keywords = "axiomref"
+ keywords = "axiomref, printed"
}
\end{chunk}
@@ 17450,7 +17485,7 @@ when shown in factored form.
into OCAML and COQ, our target languages for the computational part
and the proof checking, respectively.",
paper = "Prev02.pdf",
 keywords = "axiomref"
+ keywords = "axiomref, printed"
}
\end{chunk}
@@ 17632,7 +17667,7 @@ when shown in factored form.
given algorithm a set of theorems that imply the correctness of this
algorithm.",
paper = "Schw97.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 18023,7 +18058,8 @@ when shown in factored form.
it satisfies. Every function of the same type satisfies the same
theorem. This provides a free source of useful theorems, courtesy of
Reynolds' abstraction theorem for the polymorphic lambda calculus.",
 paper = "Wadl89.pdf"
+ paper = "Wadl89.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 19163,7 +19199,8 @@ J. Symbolic COmputations 36 pp 855889
its search for solutions in the monoid. It is both very efficient and
easily verifiable. Some applications of this algorithm are shown in
the appendix.",
 paper = "Fort87.pdf"
+ paper = "Fort87.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 20703,14 +20740,19 @@ ACM Proc. 1976 annual conference pp425428
\end{chunk}
\index{Moses, Joel}
\begin{chunk}{ignore}
\bibitem[Moses 71a]{Mos71a} Moses, Joel
+\begin{chunk}{axiom.bib}
+@article{Mose71,
+ author = "Moses, Joel",
title = {{Symbolic Integration: The Stormy Decade}},
CACM Aug 1971 Vol 14 No 8 pp548560
 link = "\url{http://wwwinst.eecs.berkeley.edu/~cs282/sp02/readings/mosesint.pdf}",
 ref = "00017",
 abstract = "
 Three approaches to symbolic integration in the 1960's are
+ journal = "CACM",
+ year = "1971",
+ volume = "14",
+ number = "8",
+ pages = "548560",
+ link =
+ "\url{http://wwwinst.eecs.berkeley.edu/~cs282/sp02/readings/mosesint.pdf}",
+ abstract =
+ "Three approaches to symbolic integration in the 1960's are
described. The first, from artificial intelligence, led to Slagle's
SAINT and to a large degree to Moses' SIN. The second, from algebraic
manipulation, led to Monove's implementation and to Horowitz' and
@@ 20721,7 +20763,9 @@ CACM Aug 1971 Vol 14 No 8 pp548560
Generalizations of Risch's algorithm to a class of special
functions and programs for solving differential equations and for
finding the definite integral are also described.",
 paper = "Mos71a.pdf"
+ paper = "Mos71a.pdf",
+ keywords = "printed"
+}
\end{chunk}
@@ 22100,7 +22144,8 @@ Proc ISSAC 97 pp172175 (1997)
problem is far harder, and several major questions remain to be
answered. Nevertheless, the last few years have seen substantial
improvements, and such factorisations are now possible",
 paper = "Abbo87.pdf"
+ paper = "Abbo87.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 32436,7 +32481,7 @@ Universit{\"a}t Karsruhe, Karlsruhe, Germany 1994
year = "1987",
pages = "211",
paper = "Calm87.pdf",
 keywords = "axiomref"
+ keywords = "axiomref, printed"
}
\end{chunk}
@@ 33731,7 +33776,8 @@ April 89, 2013 Portland Oregon
title = {{A Small OpenMath Type System}},
year = "1999",
link = "\url{https://www.openmath.org/standard/sts.pdf}",
 paper = "Dave99.pdf"
+ paper = "Dave99.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 35341,7 +35387,7 @@ ISBN 1581130732 LCCN QA76.95.I57 1999
isbn = "1581130732",
link = "\url{http://www.acm.org/citation.cfm?id=309944}",
paper = "Doye99.pdf",
 keywords = "axiomref",
+ keywords = "axiomref, printed",
beebe = "Doye:1999:ACA"
}
@@ 39283,7 +39329,7 @@ Watson Research Center, Yorktown Heights, NY, USA, 1969 RC2968 July 1970
a highlevel programming language, both for the formal description of
mathematical algorithms and their efficient implementation.",
paper = "Jenk74.pdf",
 keywords = "axiomref",
+ keywords = "axiomref, printed",
beebe = "Jenks:1974:SL"
}
@@ 39702,7 +39748,7 @@ SIGPLAN Notices, New York: Association for Computing Machiner, Nov 1981
polymorphic packages of functions that may create datatypes. The use
of categories makes these facilities as general as possible.",
paper = "Jenk86.pdf",
 keywords = "axiomref",
+ keywords = "axiomref, printed",
beebe = "Jenks:1986:SIA"
}
@@ 41444,7 +41490,7 @@ SIGSAM Communications in Computer Algebra, 157 2006
shown how some complex problems in homologicial algebra were solved
through the use of this system.",
paper = "Lamb92.pdf",
 keywords = "axiomref",
+ keywords = "axiomref, printed",
beebe = "Lambe:1994:NGC"
}
@@ 41882,7 +41928,7 @@ PhD thesis, Nov 2008 Florida State University
year = "1996",
link = "\url{http://lecerf.perso.math.cnrs.fr/software/drc/drc.ps}",
paper = "Lece96.pdf",
 keywords = "axiomref"
+ keywords = "axiomref, printed"
}
\end{chunk}
@@ 43123,12 +43169,13 @@ SpringerVerlag, Berlin, Germany / Heildelberg, Germany / London, UK / etc.,
\index{Missura, Stephan A.}
\index{Weber, Andreas}
\begin{chunk}{ignore}
\bibitem[Missura 94]{Miss94} Missura, Stephan A.; Weber, Andreas
+\begin{chunk}{axiom.bib}
+@misc{Miss94,
+ author = "Missura, Stephan A. and Weber, Andreas",
title = {{Using Commutativity Properties for Controlling Coercions}},
link = "\url{http://cg.cs.unibonn.de/personalpages/weber/publications/pdf/WeberA/MissuraWeber94a.pdf}",
 abstract = "
 This paper investigates some soundness conditions which have to be
+ abstract =
+ "This paper investigates some soundness conditions which have to be
fulfilled in systems with coercions and generic operators. A result of
Reynolds on unrestricted generic operators is extended to generic
operators which obey certain constraints. We get natural conditions
@@ 43141,7 +43188,8 @@ SpringerVerlag, Berlin, Germany / Heildelberg, Germany / London, UK / etc.,
cannot. An algorithm is presented that detects such unresolvable
ambiguities in expressions.",
paper = "Miss94.pdf",
 keywords = "axiomref"
+ keywords = "axiomref, printed"
+}
\end{chunk}
@@ 43630,7 +43678,7 @@ Invited Presentation in Milestones in Computer Algebra, May 2008, Tobago
pages = "1220",
year = "1975",
comment = "IBM T.J. Watson Research RC4998",
 keywords = "axiomref"
+ keywords = "axiomref, printed"
}
\end{chunk}
@@ 44784,7 +44832,7 @@ J. of Symbolic Computation 36 pp 513533 (2003)
concepts. The full calculus has been implemented and tested with our
LA compiler which generates executable files.",
paper = "Sant96.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 44884,7 +44932,7 @@ Kognitive Systeme, Universit\"t Karlsruhe 1992
differential equations and the Scratchpad package SPDE which
abbreviates Symmetries of Partial Differential Equations.",
paper = "Schw87.pdf",
 keywords = "axiomref",
+ keywords = "axiomref, printed",
beebe = "Schwarz:1988:PAD"
}
@@ 46068,7 +46116,7 @@ Kognitive Systeme, Universit\"t Karlsruhe 1992
conveniently define a quote function, thus facilitating the use of
reflective techniques.",
paper = "Spit11.pdf",
 keywords = "axiomref"
+ keywords = "axiomref, printed"
}
\end{chunk}
@@ 47733,7 +47781,7 @@ IBM Research Division Technical Report RC19530 May 1994
computer algebra whose coercion relations cannot be captured by a
finite set of firstorder rewrite rules.",
paper = "Webe05.pdf",
 keywords = "axiomref, coercion"
+ keywords = "axiomref, coercion, printed"
}
\end{chunk}
@@ 48415,11 +48463,15 @@ Oxford University Press (2000) ISBN0195125169
\end{chunk}
\index{Zippel, Richard}
\begin{chunk}{ignore}
\bibitem[Zip92]{Zip92} Zippel, Richard
+\begin{chunk}{axiom.bib}
+@book{Zipp92a,
+ author = "Zippel, Richard",
title = {{Algebraic Computation}},
(unpublished) Cornell University Ithaca, NY Sept 1992
 keywords = "axiomref"
+ publisher = "Cornell University",
+ comment = "Unpublished",
+ year = "1992",
+ keywords = "axiomref, printed"
+}
\end{chunk}
@@ 48581,6 +48633,18 @@ Dover Publications. (1968)
\end{chunk}
+\index{Adamchik, Victor}
+\begin{chunk}{axiom.bib}
+@misc{Adam17,
+ author = "Adamchik, Victor",
+ title = {{Modern Computer Algebra}},
+ comment = "Carnegie Mellon SCS 15355",
+ year = "2017",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Altmann, Simon L.}
\begin{chunk}{axiom.bib}
@book{Altm05,
@@ 49157,7 +49221,6 @@ Comm. ACM. 17, 6 319320. (1974)
\end{chunk}

\index{Beauzamy, Bernard}
\begin{chunk}{ignore}
\bibitem[Beauzamy 92]{Bea92} Beauzamy, Bernard
@@ 49222,7 +49285,8 @@ J. Symbolic Computation (1993) 15, 393413
volume = "1158",
year = "1995",
pages = "3646",
 paper = "Berg95.pdf"
+ paper = "Berg95.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 49488,6 +49552,37 @@ J. Symbolic Computation (1993) 16, 131145
\end{chunk}
+\index{Brady, Edwin}
+\begin{chunk}{axiom.bib}
+@article{Brad13,
+ author = "Brady, Edwin",
+ title = {{Idris, a General Purpose Dependently Typed Programming
+ Language: Design and Implementation}},
+ journal = "J. Functional Programming",
+ volume = "23",
+ number = "5",
+ year = "2013",
+ pages = "552593",
+ abstract =
+ "Many components of a dependently typed programming language are by
+ now well understood, for example, the underlying type theory, type
+ checking, unification and evaluation. How to combine these components
+ into a realistic and usable highlevel language is, however, folklore,
+ discovered anew by successive language implementors. In this paper, I
+ describe the implementation of Idris, a new dependently typed
+ functional programming language. Idris is intended to be a
+ generalpurpose programming language and as such provides highlevel
+ concepts such as implicit syntax, type classes and do notation. I
+ describe the highlevel language and the underlying type theory, and
+ present a tacticbased method for elaborating concrete highlevel
+ syntax with implicit arguments and type classes into a fully explicit
+ type theory. Furthermore, I show how this method facilitates the
+ implementation of new highlevel language constructs.",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Braman, K.}
\index{Byers, R.}
\index{Mathias, R.}
@@ 49544,6 +49639,18 @@ J. Symbolic Computation (1993) 16, 131145
\end{chunk}
+\index{Brent, Richard P.}
+\index{Zimmermann, Paul}
+\begin{chunk}{axiom.bib}
+@misc{Bren10,
+ author = "Brent, Richard P. and Zimmermann, Paul",
+ title = {{Modern Computer Arithmetic}},
+ year = "2010",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Brent, R. P.}
\begin{chunk}{ignore}
\bibitem[Brent 75]{Bre75} Brent, R. P.
@@ 49774,7 +49881,8 @@ ISBN 3764359013 (1998)
geometrical theorem proving, primary decompsotion of implicitly
defined geometrical objects). The paper starts with a brief summary of
the Groebner bases method.",
 paper = "Buch87.pdf"
+ paper = "Buch87.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 50599,7 +50707,8 @@ J. Inst. Math. Appl. 21 135143. (1978)
error situations. The soundness and meaning of the major concepts
involed in rewriting systems are reviewed when applied to such
structures.",
 paper = "Cunn85.pdf"
+ paper = "Cunn85.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 50867,7 +50976,8 @@ SIAM J. Numer. Anal. 19 12861304. (1982)
effective quantier elimination and simplication of quantierfree
formulas, REDLOG is intended and designed as an allpurpose system.
REDLOG is freely available to the scientic community.",
 paper = "Dolz96.pdf"
+ paper = "Dolz96.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 51073,7 +51183,7 @@ A.E.R.E. Report R.8730. HMSO. (1977)
booktitle = "Proc. Calculemus, 2001",
year = "2001",
paper = "Duns01.pdf",
 keywords = "axiomref, CASproof"
+ keywords = "axiomref, CASproof, printed"
}
\end{chunk}
@@ 51608,6 +51718,98 @@ AddisonWesley. 181187. (1965)
\subsection{G} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Garcia, Ronald}
+\index{Clark, Alison M.}
+\index{Tanter, Eric}
+\begin{chunk}{axiom.bib}
+@inproceedings{Garc16,
+ author = "Garcia, Ronald and Clark, Alison M. and Tanter, Eric",
+ title = {{Abstracting Gradual Typing}},
+ booktitle = "POPL 16",
+ publisher = "ACM",
+ year = "2016",
+ pages = "429442",
+ abstract =
+ "Language researchers and designers have extended a wide variety
+ of type systems to support {\sl gradual typing}, which enables
+ languages to seemlessly combine dynamic and static checking. These
+ efforts consistently demonstrate that designing a satisfactory
+ gradual counterpart to a static type system is challenging, and
+ this challenge only increases with the sophistication of the type
+ system. Graudal type system designers need more formal tools to
+ help them conceptualize, structure, and evaluate their designs.
+
+ In this paper, we propose a new formal foundation for graudal
+ typing, drawing on principles from abstract interpretation to give
+ gradual types a semantics in terms of preexisting static
+ types. Abstracting Gradual Typing (AGT for short) yields a formal
+ account of {\sl consistency}  one of the cornerstones of the
+ gradual typing approach  that subsumes existing notions of
+ consistency, which were developed through intuition and ad hoc
+ reasoning.
+
+ Given a syntaxdirected static typing judgment, the AGT approach
+ induces a corresponding gradual typing judgment. Then the type
+ safety proof for the underlying static discipline induces a
+ dynamic semantics for gradual programs defined over
+ sourcelanguage typing derivations. The AGT approach does not
+ resort to an externally justified cast calculus; instead, runtime
+ check naturally arise by deducing evidence for consistent
+ judgements during proof reduction.
+
+ To illustrate the approach, we develop a novel graduallytyped
+ counterpart for a language with record subtyping. Gradual
+ languages designed with the AGT approach satisfy {\sl by
+ construction} the refined criteria for gradual typing set forth by
+ Siek and colleagues.",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Garcia, Ronald}
+\index{Cimini, Matteo}
+\begin{chunk}{axiom.bib}
+@inproceedings{Garc17,
+ author = "Garcia, Ronald and Cimini, Matteo",
+ title = {{Principal Type Schemes for Gradual Programs}},
+ booktitle = "POPL 15",
+ comment = "Updated paper",
+ year = "2017",
+ abstract =
+ "Gradual typing is a discipline for integrating dynamic checking
+ into a static type system. Since its introduction in functional
+ languages, it has been adapted to a variety of type systems,
+ including objectoriented, security, and substructural. This work
+ studies its application to implictly typed languages based on type
+ inference. Siek and Vachharajani designed a gradual type inference
+ system and algorithm that infers gradual types but still rejects
+ illtyped static programs. However, the type system requires local
+ reasoning about type substitutions, an imperative inference
+ algorithm, and a subtle correctness statement.
+
+ This paper introduces a new approach to gradual type inference,
+ driven by the principle that gradual inference should only produce
+ static types. We present a static implicitly typed language, its
+ gradual counterpart, and a type inference procedure. The gradual
+ system types the same programs as Siek and Vachharajani, but has a
+ modular structure amenable to extension. The language admits
+ letpolymorphism, and its dynamics are defined by translation to
+ the Polymorphic Blame Calculus (Ahmed et al. 2009, 2011).
+
+ The principal types produced by our initial type system mask the
+ distinction between static parametric polymorphism and
+ polymorphism that can be attributed to gradual typing. To expose
+ this difference, we distinguish static type parameters from
+ gradual type parameters and reinterpret gradual type consistency
+ accordingly. The resulting extension enables programs to be
+ interpreted using either the polymorphic or monomorphic Blame
+ Calculi.",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Garcia, A.}
\index{Stichtenoth, H.}
\begin{chunk}{ignore}
@@ 51910,7 +52112,9 @@ Report SOL 866R. Department of Operations Research, Stanford University. 1986
title = {{Proofs and Types}},
publisher = "Cambridge University Press",
link = "\url{http://www.paultaylor.eu/stable/prot.pdf}",
 year = "2003"
+ year = "2003",
+ paper = "Gira03.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 52179,7 +52383,8 @@ Grove, IL, USA and Oxford, UK, 1992
semantics. These extensions provide a purely equational proof system
to prove properties of functional programs over userdefinable data
types.",
 paper = "Gues87.pdf"
+ paper = "Gues87.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 52286,7 +52491,8 @@ Grove, IL, USA and Oxford, UK, 1992
type classes, and supports further applications, such as code
generation and export of theories and theorems to environments without
type classes.",
 paper = "Haft06.pdf"
+ paper = "Haft06.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 52363,7 +52569,8 @@ Methuen. (1967)
declarative and procedural styles for proofs in pure mathematics and
for verification applications. We conclude with a brief summary of
our own experiments in trying to combine both approaches.",
 paper = "Harr06.pdf"
+ paper = "Harr06.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 53724,7 +53931,8 @@ PrenticeHall. (1974)
volume = "296",
year = "1987",
pages = "3851",
 paper = "Lesc97.pdf"
+ paper = "Lesc87.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 54428,7 +54636,7 @@ Mathematical Surveys. 3 Am. Math. Soc., Providence, RI. (1966)
of the Prosper project and provides a summary of the technical
approach taken and some of the lessons learned.",
paper = "Melh02.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
\end{chunk}
@@ 54480,7 +54688,8 @@ J. Res. Natl. Inst. Stand. Technol. (NIST) V105 No4 JulyAug 2000 pp589590
to display mathematical expressions on typewriterlike devices such as
line printers, teletypes, and scopes which display lines of characters,
as well as typewriters.",
 paper = "Mill68.pdf"
+ paper = "Mill68.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 54991,7 +55200,8 @@ Science of Computer Programming V25 No.1 Oct 1995 pp4161 Elesevier
formally constructed. Isabelle proof procedures are described. The
logic appears suitable for general mathematics as well as
computational problems.",
 paper = "Paul90.pdf"
+ paper = "Paul90.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 55896,7 +56106,8 @@ April 2007
give some thoughts on possible combinations of all three methods to
obtain algorithms benefitting from the specific strength of either
method.",
 paper = "Rump88.pdf"
+ paper = "Rump88.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 56155,6 +56366,51 @@ Software Practice and Experience. 6(1) (1976)
\end{chunk}
+\index{Schwarz, Fritz}
+\begin{chunk}{axiom.bib}
+@article{Schw85,
+ author = "Schwarz, Fritz",
+ title = {{An Algorithm for Determining Polynomial First Integrals of
+ Autonomous Systems of Ordinary Differential Equations}},
+ journal = "J. Symbolic Computation",
+ volume = "1",
+ year = "1985",
+ pages = "229233",
+ paper = "Schw85.pdf"
+}
+
+\end{chunk}
+
+\index{Schwarz, Fritz}
+\begin{chunk}{axiom.bib}
+@article{Schw88,
+ author = "Schwarz, Fritz",
+ title = {{Symmetries of Differential Equations: From Sophus Lie to
+ Computer Algebra}},
+ journal = "SIAM Review",
+ volume = "30",
+ number = "3",
+ year = "1988",
+ abstract =
+ "The topic of this article is the symmetry analysis of
+ differential equations and the applications of computer algebra to
+ th extensive analytical calculations which are usually involved in
+ it. The whole area naturally decomposes into two parts depending
+ on whether ordinary or partial differential equations are
+ considered. We show how a symmetry may be applied to lower the
+ order of an ordinary differential equation or to obtain similarity
+ solutions of partial differential equations. The computer algebra
+ packages SODE and SPDE, respectively, which have been developed to
+ perform almost all algebraic manipulations necessary to determine
+ the symmetry group of a given differential equation, are
+ presented. Futhermore it is argued that the application of
+ computer algebra systems has qualitatively changed this area of
+ applied mathematics",
+ keywords = "axiomref, printed"
+}
+
+\end{chunk}
+
\begin{chunk}{axiom.bib}
@misc{SCSCP,
author = "The SCSCP development team",
diff git a/changelog b/changelog
index 80bdb31..fcbf79a 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20180121 tpd src/axiomwebsite/patches.html 20180121.01.tpd.patch
+20180121 tpd books/bookvolbib add references
20180119 tpd src/axiomwebsite/patches.html 20180119.03.tpd.patch
20180119 tpd books/bookvol13 add Berg95
20180119 tpd src/axiomwebsite/patches.html 20180119.02.tpd.patch
diff git a/patch b/patch
index 2120633..c8781e5 100644
 a/patch
+++ b/patch
@@ 1,4 +1,181 @@
books/bookvol13 add Berg95
+books/bookvolbib add references
Goal: Proving Axiom Correct
+\index{Harper, Robert}
+\begin{chunk}{axiom.bib}
+@book{Harp11,
+ author = "Harper, Robert",
+ title = {{Programming in Standard ML}},
+ year = "2011",
+ publisher = "CMU",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Zippel, Richard}
+\begin{chunk}{axiom.bib}
+@book{Zipp92,
+ author = "Zippel, Richard",
+ title = {{Algebraic Computation}},
+ publisher = "Cornell University",
+ comment = "Unpublished",
+ year = "1992",
+ keywords = "axiomref, printed"
+}
+
+\end{chunk}
+
+\index{Schwarz, Fritz}
+\begin{chunk}{axiom.bib}
+@article{Schw88,
+ author = "Schwarz, Fritz",
+ title = {{Symmetries of Differential Equations: From Sophus Lie to
+ Computer Algebra}},
+ journal = "SIAM Review",
+ volume = "30",
+ number = "3",
+ year = "1988",
+ abstract =
+ "The topic of this article is the symmetry analysis of
+ differential equations and the applications of computer algebra to
+ th extensive analytical calculations which are usually involved in
+ it. The whole area naturally decomposes into two parts depending
+ on whether ordinary or partial differential equations are
+ considered. We show how a symmetry may be applied to lower the
+ order of an ordinary differential equation or to obtain similarity
+ solutions of partial differential equations. The computer algebra
+ packages SODE and SPDE, respectively, which have been developed to
+ perform almost all algebraic manipulations necessary to determine
+ the symmetry group of a given differential equation, are
+ presented. Futhermore it is argued that the application of
+ computer algebra systems has qualitatively changed this area of
+ applied mathematics",
+ keywords = "axiomref, printed"
+}
+
+\end{chunk}
+
+\index{Garcia, Ronald}
+\index{Clark, Alison M.}
+\index{Tanter, Eric}
+\begin{chunk}{axiom.bib}
+@inproceedings{Garc16,
+ author = "Garcia, Ronald and Clark, Alison M. and Tanter, Eric",
+ title = {{Abstracting Gradual Typing}},
+ booktitle = "POPL 16",
+ publisher = "ACM",
+ year = "2016",
+ pages = "429442",
+ abstract =
+ "Language researchers and designers have extended a wide variety
+ of type systems to support {\sl gradual typing}, which enables
+ languages to seemlessly combine dynamic and static checking. These
+ efforts consistently demonstrate that designing a satisfactory
+ gradual counterpart to a static type system is challenging, and
+ this challenge only increases with the sophistication of the type
+ system. Graudal type system designers need more formal tools to
+ help them conceptualize, structure, and evaluate their designs.
+
+ In this paper, we propose a new formal foundation for graudal
+ typing, drawing on principles from abstract interpretation to give
+ gradual types a semantics in terms of preexisting static
+ types. Abstracting Gradual Typing (AGT for short) yields a formal
+ account of {\sl consistency}  one of the cornerstones of the
+ gradual typing approach  that subsumes existing notions of
+ consistency, which were developed through intuition and ad hoc
+ reasoning.
+
+ Given a syntaxdirected static typing judgment, the AGT approach
+ induces a corresponding gradual typing judgment. Then the type
+ safety proof for the underlying static discipline induces a
+ dynamic semantics for gradual programs defined over
+ sourcelanguage typing derivations. The AGT approach does not
+ resort to an externally justified cast calculus; instead, runtime
+ check naturally arise by deducing evidence for consistent
+ judgements during proof reduction.
+
+ To illustrate the approach, we develop a novel graduallytyped
+ counterpart for a language with record subtyping. Gradual
+ languages designed with the AGT approach satisfy {\sl by
+ construction} the refined criteria for gradual typing set forth by
+ Siek and colleagues.",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Garcia, Ronald}
+\index{Cimini, Matteo}
+\begin{chunk}{axiom.bib}
+@inproceedings{Garc17,
+ author = "Garcia, Ronald and Cimini, Matteo",
+ title = {{Principal Type Schemes for Gradual Programs}},
+ booktitle = "POPL 15",
+ comment = "Updated paper",
+ year = "2017",
+ abstract =
+ "Gradual typing is a discipline for integrating dynamic checking
+ into a static type system. Since its introduction in functional
+ languages, it has been adapted to a variety of type systems,
+ including objectoriented, security, and substructural. This work
+ studies its application to implictly typed languages based on type
+ inference. Siek and Vachharajani designed a gradual type inference
+ system and algorithm that infers gradual types but still rejects
+ illtyped static programs. However, the type system requires local
+ reasoning about type substitutions, an imperative inference
+ algorithm, and a subtle correctness statement.
+
+ This paper introduces a new approach to gradual type inference,
+ driven by the principle that gradual inference should only produce
+ static types. We present a static implicitly typed language, its
+ gradual counterpart, and a type inference procedure. The gradual
+ system types the same programs as Siek and Vachharajani, but has a
+ modular structure amenable to extension. The language admits
+ letpolymorphism, and its dynamics are defined by translation to
+ the Polymorphic Blame Calculus (Ahmed et al. 2009, 2011).
+
+ The principal types produced by our initial type system mask the
+ distinction between static parametric polymorphism and
+ polymorphism that can be attributed to gradual typing. To expose
+ this difference, we distinguish static type parameters from
+ gradual type parameters and reinterpret gradual type consistency
+ accordingly. The resulting extension enables programs to be
+ interpreted using either the polymorphic or monomorphic Blame
+ Calculi.",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Brady, Edwin}
+\begin{chunk}{axiom.bib}
+@article{Brad13,
+ author = "Brady, Edwin",
+ title = {{Idris, a General Purpose Dependently Typed Programming
+ Language: Design and Implementation}},
+ journal = "J. Functional Programming",
+ volume = "23",
+ number = "5",
+ year = "2013",
+ pages = "552593",
+ abstract =
+ "Many components of a dependently typed programming language are by
+ now well understood, for example, the underlying type theory, type
+ checking, unification and evaluation. How to combine these components
+ into a realistic and usable highlevel language is, however, folklore,
+ discovered anew by successive language implementors. In this paper, I
+ describe the implementation of Idris, a new dependently typed
+ functional programming language. Idris is intended to be a
+ generalpurpose programming language and as such provides highlevel
+ concepts such as implicit syntax, type classes and do notation. I
+ describe the highlevel language and the underlying type theory, and
+ present a tacticbased method for elaborating concrete highlevel
+ syntax with implicit arguments and type classes into a fully explicit
+ type theory. Furthermore, I show how this method facilitates the
+ implementation of new highlevel language constructs.",
+ keywords = "printed"
+}
+
+\end{chunk}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index f097387..fc0f73b 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5900,6 +5900,8 @@ src/axiomwebsite/documentation.html add hrefs to Daly book
books/bookvolbib add references
20180119.03.tpd.patch
books/bookvol13 add Berg95
+20180121.01.tpd.patch
+books/bookvolbib add references

1.9.1