From b593d54281dbe94bc1d918f6b9b27213d9e869f1 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Wed, 23 Aug 2017 21:31:41 0400
Subject: [PATCH] books/bookvolbib Add proof references
Goal: Axiom references
\index{Pfenning, Frank}
\begin{chunk}{axiom.bib}
@misc{Pfen97,
author = "Pfenning, Frank",
title = "Computation and Deduction",
link = "\url{www.cs.cmu.edu/~twelf/notes/cd.pdf}",
paper = "Pfen97.pdf"
}
\end{chunk}

books/bookvolbib.pamphlet  11 +++++
changelog  2 +
patch  101 +++
src/axiomwebsite/patches.html  2 +
4 files changed, 21 insertions(+), 95 deletions()
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 22ad8e5..b4d8ad1 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 37882,6 +37882,17 @@ New York, NY 10036, USA, 1971. LCCN QA76.5.S94 1971
\end{chunk}
+\index{Pfenning, Frank}
+\begin{chunk}{axiom.bib}
+@misc{Pfen97,
+ author = "Pfenning, Frank",
+ title = "Computation and Deduction",
+ link = "\url{www.cs.cmu.edu/~twelf/notes/cd.pdf}",
+ paper = "Pfen97.pdf"
+}
+
+\end{chunk}
+
\index{Pinch, R.G.E.}
\begin{chunk}{ignore}
\bibitem[Pinch 93]{Pin93} Pinch, R.G.E.
diff git a/changelog b/changelog
index 76bd8ef..60181a6 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20170823 tpd src/axiomwebsite/patches.html 20170823.02.tpd.patch
+20170823 tpd books/bookvolbib Add proof references
20170823 tpd src/axiomwebsite/patches.html 20170823.01.tpd.patch
20170823 tpd books/bookvolbib Add proof references
20170819 tpd src/axiomwebsite/patches.html 20170819.01.tpd.patch
diff git a/patch b/patch
index 2d37cbd..51553d1 100644
 a/patch
+++ b/patch
@@ 2,102 +2,13 @@ books/bookvolbib Add proof references
Goal: Axiom references
\index{Melquiond, Guillaume}
+\index{Pfenning, Frank}
\begin{chunk}{axiom.bib}
@article{Melq12,
 author = "Melquiond, Guillaume",
 title = "Floatingpoint arithmetic in the Coq system",
 journal = "Information and Computation",
 volume = "216",
 pages = "1423",
 year = "2012",
 link = "\url{https://www.lri.fr/~melquion/doc/08mc8article.pdf}",
 abstract =
 "The process of proving some mathematical theorems can be greatly
 reduced by relying on numericallyintensive computations with a
 certified arithmetic. This article presents a formalization of
 floatingpoint arithmetic that makes it possible to efficiently
 compute inside the proofs of the Coq system. This certified library is
 a multiradix and multiprecision implementation free from underflow
 and overflow. It provides the basic arithmetic operators and a few
 elementary functions.",
 paper = "Melq12.pdf"
+@misc{Pfen97,
+ author = "Pfenning, Frank",
+ title = "Computation and Deduction",
+ link = "\url{www.cs.cmu.edu/~twelf/notes/cd.pdf}",
+ paper = "Pfen97.pdf"
}
\end{chunk}

\index{Akers, Robert Lawrence}
\begin{chunk}{axiom.bib}
@phdthesis{Aker93,
 author = "Akers, Robert Lawrence",
 title = "Strong Static Type Checking for Functional Common Lisp",
 school = "Univerity of Texas at Austin",
 year = "1995",
 link = "\url{ftp://www.cs.utexas.edu/pub/boyer/clireports/096.pdf}",
 abstract =
 "This thesis presents a type system which supports the strong static
 type checking of programs developed in an applicative subset of the
 Common Lisp language. The Lisp subset is augmented with a guard
 construct for function definitions, which allows type restrictions to
 be placed on the arguments. Guards support the analysis and safe use
 of partial functions, like CAR, which are welldefined only for
 arguments of a certain type.

 A language of type descriptors characterizes the type
 domain. Descriptors are composed into function signatures which
 characterize the guard and which map various combinations of actual
 parameter types to possible result types. From a base of signatures
 for a small collection of primitive functions, the system infers
 signatures for newly submitted functions.

 The system includes a type inference algorithm which handles
 constructs beyond the constraints of MLstyle systems. Most notable
 are the free use of CONS to construct objects of undeclared type and
 the use of IF forms whose two result components have unrelated types,
 resulting in ad hoc polymorphism. Accordingly, the type descriptor
 language accommodates disjunction, unrestricted CONS, recursive type
 forms, and ad hoc polymorphic function signatures. As with traditional
 type inference systems, unification is a central algorithm, but the
 richness of our type language complicates many component algorithms,
 including unification. Special treatment is given to recognizer
 functions, which are predicates determining whether an object is of a
 particular type. Type inference in this setting is undecidable, so the
 algorithm is heuristic and is not complete.

 The semantics of the system are in terms of a function which
 determines whether values satisfy descriptors with respect to a
 binding of type variables. The soundness of each signature emitted by
 the system is validated by a signature checker, whose properties are
 formally specified with respect to the formal semantics and proven to
 hold. The checker algorithm is substantially simpler than the
 inference algorithm, as it need not perform operations such as
 discovering closed recursive forms. Thus, its proof is both more
 straightforward to construct and easier to validate than a direct
 proof of the inference algorithm would be.",
 paper = "Aker93.pdf"
}

\end{chunk}

\index{Byrd, William}
\begin{chunk}{axiom.bib}
@misc{Byrd17,
 author = "Byrd, William",
 title = "The Most Beautiful Program Ever Written",
 link = "\url{https://www.youtube.com/watch?v=OyfBQmvr2Hc}",
 comment = "See miniKanren and Barliman (program synthesis with proof)"
}

\end{chunk}

\begin{chunk}{axiom.bib}
@misc{Unkn13,
 author = "Unknown",
 title = "HindleyMilner Type Inference",
 link = "\url{https://www7.in.tum.de/um/courses/seminar/sove/SS2013/final/hindleymilner.slides.pdf}",
 paper = "Unkn13.pdf"

}

\end{chunk}

diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 8fddb5a..4d79d9f 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5800,6 +5800,8 @@ books/bookvolbib Add references
books/bookvolbib Add references
20170823.01.tpd.patch
books/bookvolbib Add proof references
+20170823.02.tpd.patch
+books/bookvolbib Add proof references

1.9.1