From 9bfbcda2f480699a8a134d99caabb800d82af676 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Mon, 22 May 2017 02:57:03 0400
Subject: [PATCH] bookvolbib type inferencing papers
Goal: Proving Axiom Correct
\index{Gentzen, Gerhard}
\begin{chunk}{axiom.bib}
@misc{Gent35,
author = "Gentzen, Gerhard",
title = "Investigations into Logical Deduction",
year = "1935",
pages = "68131",
paper = "Gent35.pdf"
}
\end{chunk}
\index{Gentzen, Gerhard}
\begin{chunk}{axiom.bib}
@article{Gent64,
author = "Gentzen, Gerhard",
title = "Investigations into Logical Deduction",
journal = "American Philosophical Quarterly",
volume = "1",
number = "4",
year = "1964",
pages = "288306",
paper = "Gent64.pdf"
}
\end{chunk}
\index{Gentzen, Gerhard}
\begin{chunk}{axiom.bib}
@article{Gent65,
author = "Gentzen, Gerhard",
title = "Investigations into Logical Deduction: II",
journal = "American Philosophical Quarterly",
volume = "2",
number = "3",
year = "1965",
pages = "204218",
paper = "Gent65.pdf"
}
\end{chunk}
\index{Howard, W. A.}
\begin{chunk}{axiom.bib}
@misc{Howa80,
author = "Howard, W. A.",
title = "The FormulaeasTypes Notion of Construction",
link = "\url{http://lecomte.al.free.fr/ressources/PARIS8_LSL/Howard80.pdf}",
year = "1980",
abstract =
"The following consists of notes which were privately circulated in
1969. Since they have been referred to a few times in the literature,
it seems worth while to publish them. They have been rearranged for
easier reading, and some inessential corrections have been made.
The ultimate goal was to develop a notion of construction suitable for
the interpretation of intuitionistic mathematics. The notion of
construction developed in the notes is certainly too crude for that,
so the use of the word {\sl construction} is not very appropriate.
However, the terminology has been kept in order to preserve the
original title and also to preserve the character of the notes. The
title has a second defect; namely, the {\sl type} should be regarded
as a abstract object whereas a {\sl formula} is the name of a type.",
paper = "Howa80.pdf"
}
\end{chunk}

books/bookvolbib.pamphlet  68 ++++++++++++++++++++++++++
changelog  2 +
patch  103 ++++++++++++++++++++++++
src/axiomwebsite/patches.html  2 +
4 files changed, 135 insertions(+), 40 deletions()
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index d8a82d6..51b2e55 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 6926,6 +6926,48 @@ Calculemus (2011) Springer
\subsection{G} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Gentzen, Gerhard}
+\begin{chunk}{axiom.bib}
+@misc{Gent35,
+ author = "Gentzen, Gerhard",
+ title = "Investigations into Logical Deduction",
+ year = "1935",
+ pages = "68131",
+ paper = "Gent35.pdf"
+}
+
+\end{chunk}
+
+\index{Gentzen, Gerhard}
+\begin{chunk}{axiom.bib}
+@article{Gent64,
+ author = "Gentzen, Gerhard",
+ title = "Investigations into Logical Deduction",
+ journal = "American Philosophical Quarterly",
+ volume = "1",
+ number = "4",
+ year = "1964",
+ pages = "288306",
+ paper = "Gent64.pdf"
+}
+
+\end{chunk}
+
+\index{Gentzen, Gerhard}
+\begin{chunk}{axiom.bib}
+@article{Gent65,
+ author = "Gentzen, Gerhard",
+ title = "Investigations into Logical Deduction: II",
+ journal = "American Philosophical Quarterly",
+ volume = "2",
+ number = "3",
+ year = "1965",
+ pages = "204218",
+ paper = "Gent65.pdf"
+}
+
+\end{chunk}
+
\index{Geuvers, Herman}
\begin{chunk}{axiom.bib}
@misc{Geuv92,
@@ 7235,6 +7277,32 @@ Calculemus (2011) Springer
\end{chunk}
+\index{Howard, W. A.}
+\begin{chunk}{axiom.bib}
+@misc{Howa80,
+ author = "Howard, W. A.",
+ title = "The FormulaeasTypes Notion of Construction",
+ link = "\url{http://lecomte.al.free.fr/ressources/PARIS8_LSL/Howard80.pdf}",
+ year = "1980",
+ abstract =
+ "The following consists of notes which were privately circulated in
+ 1969. Since they have been referred to a few times in the literature,
+ it seems worth while to publish them. They have been rearranged for
+ easier reading, and some inessential corrections have been made.
+
+ The ultimate goal was to develop a notion of construction suitable for
+ the interpretation of intuitionistic mathematics. The notion of
+ construction developed in the notes is certainly too crude for that,
+ so the use of the word {\sl construction} is not very appropriate.
+ However, the terminology has been kept in order to preserve the
+ original title and also to preserve the character of the notes. The
+ title has a second defect; namely, the {\sl type} should be regarded
+ as a abstract object whereas a {\sl formula} is the name of a type.",
+ paper = "Howa80.pdf"
+}
+
+\end{chunk}
+
\index{Huet, G\'erard}
\begin{chunk}{axiom.bib}
@inproceedings{Huet87,
diff git a/changelog b/changelog
index 5cca925..ca7b069 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20170520 tpd src/axiomwebsite/patches.html 20170521.01.tpd.patch
+20170521 tpd bookvolbib type inferencing papers
20170520 tpd src/axiomwebsite/patches.html 20170520.02.tpd.patch
20170520 tpd bookvolbib type inferencing for Common Lisp
20170520 tpd src/axiomwebsite/patches.html 20170520.01.tpd.patch
diff git a/patch b/patch
index 7ae8830..77dd5a9 100644
 a/patch
+++ b/patch
@@ 1,48 +1,71 @@
bookvolbib type inferencing for Common Lisp
+bookvolbib type inferencing papers
Goal: Proving Axiom Correct
\index{Baker, Henry G.}
+\index{Gentzen, Gerhard}
\begin{chunk}{axiom.bib}
@misc{Bake90,
 author = "Baker, Henry G.",
 title = "The Nimble Type Inferencer for Common Lisp84",
 link = "\url{http://home.pipeline.com/~hbaker1/TInference.html}",
 year = "1990",
 abstract =
 "We describe a framework and an algorithm for doing type inference
 analysis on programs written in full Common Lisp84 (Common Lisp
 without the CLOS objectoriented extensions). The objective of type
 inference is to determine tight lattice upper bounds on the range of
 runtime data types for Common Lisp program variables and
 temporaries. Depending upon the lattice used, type inference can also
 provide range analysis information for numeric variables. This lattice
 upper bound information can be used by an optimizing compiler to
 choose more restrictive, and hence more efficient, representations for
 these program variables. Our analysis also produces tighter control
 flow information, which can be used to eliminate redundant tests which
 result in dead code. The overall goal of type inference is to
 mechanically extract from Common Lisp programs the same degree of
 representation information that is usually provided by the programmer
 in traditional stronglytyped languages. In this way, we can provide
 some classes of Common Lisp programs execution time efficiency
 expected only for more stronglytyped compiled languages.

 The Nimble type inference system follows the traditional
 lattice/algebraic data flow techniques [Kaplan80], rather than the
 logical/theoremproving unification techniques of ML [Milner78]. It
 can handle polymorphic variables and functions in a natural way, and
 provides for ``casebased'' analysis that is quite similar to that used
 intuitively by programmers. Additionally, this inference system can
 deduce the termination of some simple loops, thus providing
 surprisingly tight upper lattice bounds for many loop variables.
+@misc{Gent35,
+ author = "Gentzen, Gerhard",
+ title = "Investigations into Logical Deduction",
+ year = "1935",
+ pages = "68131",
+ paper = "Gent35.pdf"
+}
+
+\end{chunk}
+
+\index{Gentzen, Gerhard}
+\begin{chunk}{axiom.bib}
+@article{Gent64,
+ author = "Gentzen, Gerhard",
+ title = "Investigations into Logical Deduction",
+ journal = "American Philosophical Quarterly",
+ volume = "1",
+ number = "4",
+ year = "1964",
+ pages = "288306",
+ paper = "Gent64.pdf"
+}
+
+\end{chunk}
+
+\index{Gentzen, Gerhard}
+\begin{chunk}{axiom.bib}
+@article{Gent65,
+ author = "Gentzen, Gerhard",
+ title = "Investigations into Logical Deduction: II",
+ journal = "American Philosophical Quarterly",
+ volume = "2",
+ number = "3",
+ year = "1965",
+ pages = "204218",
+ paper = "Gent65.pdf"
+}
+
+\end{chunk}
+
+\index{Howard, W. A.}
+\begin{chunk}{axiom.bib}
+@misc{Howa80,
+ author = "Howard, W. A.",
+ title = "The FormulaeasTypes Notion of Construction",
+ link = "\url{http://lecomte.al.free.fr/ressources/PARIS8_LSL/Howard80.pdf}",
+ year = "1980",
+ abstract =
+ "The following consists of notes which were privately circulated in
+ 1969. Since they have been referred to a few times in the literature,
+ it seems worth while to publish them. They have been rearranged for
+ easier reading, and some inessential corrections have been made.
 By using a higher resolution lattice, more precise typing of primitive
 functions, polymorphic types and case analysis, the Nimble type
 inference algorithm can often produce sharper bounds than
 unificationbased type inference techniques. At the present time,
 however, our treatment of higherorder data structures and functions
 is not as elegant as that of the unification techniques."
+ The ultimate goal was to develop a notion of construction suitable for
+ the interpretation of intuitionistic mathematics. The notion of
+ construction developed in the notes is certainly too crude for that,
+ so the use of the word {\sl construction} is not very appropriate.
+ However, the terminology has been kept in order to preserve the
+ original title and also to preserve the character of the notes. The
+ title has a second defect; namely, the {\sl type} should be regarded
+ as a abstract object whereas a {\sl formula} is the name of a type.",
+ paper = "Howa80.pdf"
}
\end{chunk}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 70e2b9d..97915aa 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5736,6 +5736,8 @@ download.html update download table for BSD, ubuntu, ubuntu64
bookvolbib cylindrical algorithmic decomposition references
20170520.02.tpd.patch
bookvolbib type inferencing for Common Lisp
+20170521.01.tpd.patch
+bookvolbib type inferencing papers

1.7.5.4