From 8a9d0dffa873207d2caaab4be3b73906a83330a5 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Fri, 19 Jan 2018 19:14:45 -0500
Subject: [PATCH] books/bookvolbib add references
Goal: Proving Axiom Correct
\index{Lakatos, Imre}
\begin{chunk}{axiom.bib}
@book{Laka76,
author = "Lakatos, Imre",
title = {{Proofs and Refutations}},
year = "1976",
publisher = "Cambridge University Press",
isbn = "978-1-107-53405-6"
}
\end{chunk}
\index{Hall, Condelia V.}
\begin{chunk}{axiom.bib}
@inproceedings{Hall94,
author = "Hall, Condelia V.",
title =
{{Using Hindley-Milner Type Inference to Optimize List Representation}},
booktitle = "LFP'94 Lisp and Functional Programming",
publisher = "ACM",
year = "1994",
pages = "162-172",
abstract =
"Lists are a pervasive data structure in functional programs. The
generality and simplicity of their structure makes them expensive.
Hindley-Mllner type inference and partial evalua- tion are all that is
needed to optimise this structure, yielding considerable improvements
in space and time consumption for some interesting programs. This
framework is applica- ble to many data types and their optimised
representations, such as lists and parallel implementations of bags,
or arrays and quadtrees.",
paper = "Hall94.pdf"
}
\end{chunk}
---
books/axiom.bib | 63 +++++++++++++++++++++++++++----------
books/bookvolbib.pamphlet | 71 ++++++++++++++++++++++++++++++++----------
changelog | 2 ++
patch | 40 ++++++++++++++++++++++--
src/axiom-website/patches.html | 2 ++
5 files changed, 142 insertions(+), 36 deletions(-)
diff --git a/books/axiom.bib b/books/axiom.bib
index 0812108..09cee7e 100644
--- a/books/axiom.bib
+++ b/books/axiom.bib
@@ -1270,7 +1270,7 @@ paper = "Brea89.pdf"
volume = "146",
year = "1969",
pages = "29-60",
- paper = "Hind69.pdf"
+ paper = "Hind69.pdf, printed"
}
@article{Hodg95,
@@ -2255,7 +2255,7 @@ paper = "Brea89.pdf"
avoiding anomalies in the interaction of implicit conversions and
generic operators. The definition of a simple imperative language
(without any binding mechanisms) is used as an example.",
- paper = "Reyn80.pdf"
+ paper = "Reyn80.pdf, printed"
}
@inproceedings{Reyn84,
@@ -7207,7 +7207,7 @@ paper = "Brea89.pdf"
exculded middle similar to Brouwer's had been advanced in print by
Jules Molk two years before. Finally, we discuss the influence on
George Griss' negationless mathematics",
- paper = "Atte15.pdf"
+ paper = "Atte15.pdf, printed"
}
@article{Bate85,
@@ -7446,7 +7446,7 @@ paper = "Brea89.pdf"
proof assistant, a tool for machine-checked mathematical theorem
proving; and formal logical reasoning about the correctness of
programs.",
- paper = "Chli17.pdf"
+ paper = "Chli17.pdf, printed"
}
@article{Coen04,
@@ -7596,7 +7596,7 @@ paper = "Brea89.pdf"
"We present an extensive set of mathematical propositions and proofs
in order to demonstrate the power of expression of the theory of
constructions.",
- paper = "Coqu85.pdf"
+ paper = "Coqu85.pdf, printed"
}
@misc{Cyph17,
@@ -7776,6 +7776,14 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@book{Laka76,
+ author = "Lakatos, Imre",
+ title = {{Proofs and Refutations}},
+ year = "1976",
+ publisher = "Cambridge University Press",
+ isbn = "978-1-107-53405-6"
+}
+
@incollection{Lams00,
author = "van Lamsweerde, Axel",
title = {{Formal Specification: A Roadmap}},
@@ -7868,6 +7876,26 @@ paper = "Brea89.pdf"
paper = "Luox13.pdf"
}
+@inproceedings{Hall94,
+ author = "Hall, Condelia V.",
+ title =
+ {{Using Hindley-Milner Type Inference to Optimize List Representation}},
+ booktitle = "LFP'94 Lisp and Functional Programming",
+ publisher = "ACM",
+ year = "1994",
+ pages = "162-172",
+ abstract =
+ "Lists are a pervasive data structure in functional programs. The
+ generality and simplicity of their structure makes them expensive.
+ Hindley-Mllner type inference and partial evalua- tion are all that is
+ needed to optimise this structure, yielding considerable improvements
+ in space and time consumption for some interesting programs. This
+ framework is applica- ble to many data types and their optimised
+ representations, such as lists and parallel implementations of bags,
+ or arrays and quadtrees.",
+ paper = "Hall94.pdf, printed"
+}
+
@article{Mann78,
author = "Manna, Zohar and Waldinger, Richard",
title = {{The Logic of Computer Programming}},
@@ -7887,7 +7915,7 @@ paper = "Brea89.pdf"
limitations of each technique as a practial programming aid are
assessed and attempts to implement these methods in experimental
systems are discussed.",
- paper = "Mann78.pdf"
+ paper = "Mann78.pdf, printed"
}
@misc{Mann80,
@@ -7895,7 +7923,8 @@ paper = "Brea89.pdf"
title = {{Lectures on the Logic of Computer Programming}},
publisher = "Society for Industrial and Applied Mathematics",
year = "1980",
- paper = "Mann80.tgz"
+ paper = "Mann80.tgz",
+ keywords = "printed"
}
@inproceedings{Mart73,
@@ -8102,7 +8131,7 @@ paper = "Brea89.pdf"
application nodes. We motivate our design choices by a statistical
analysis of the uses of type inference in a sizable body of existing
ML code.",
- paper = "Pier97.pdf"
+ paper = "Pier97.pdf, printed"
}
@misc{Reid17,
@@ -8165,7 +8194,7 @@ paper = "Brea89.pdf"
several principles (called search principles) which are applicable to
the design of efficient proof-procedures employing resolution as the
basic logical process.",
- paper = "Robi65.pdf"
+ paper = "Robi65.pdf, printed"
}
@article{Ruzi89,
@@ -10991,7 +11020,7 @@ paper = "Brea89.pdf"
abstract =
"The Hindley-Milner algorithm is described and an implementation in
Standard ML is presented.",
- paper = "Gran11.pdf"
+ paper = "Gran11.pdf, printed"
}
@book{Grie81,
@@ -13079,7 +13108,7 @@ paper = "Brea89.pdf"
proceed step by step or automatically and so on. The environment
enhances the effectiveness and flexibility of the reasoners of the
Theorema system.",
- paper = "Piro05.pdf"
+ paper = "Piro05.pdf, printed"
}
@article{Plot77,
@@ -31060,7 +31089,7 @@ paper = "Brea89.pdf"
their problems. The system can be further extended in other to support
more constructs and increase its flexibility.",
paper = "Sant95.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, printed"
}
@inproceedings{Sant96,
@@ -32816,7 +32845,7 @@ paper = "Brea89.pdf"
but even type checking is undecidable for relevant cases occurring in
computer algebra.",
paper = "Webe93b.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, printed"
}
@inproceedings{Webe05,
@@ -36749,7 +36778,7 @@ paper = "Brea89.pdf"
frameworks, focusing on their sort disciplines and assessing their
strengths and weaknesses for practical applications. Familiarity with
the basic notions of algebraic specification is assumed.",
- paper = "Moss93.pdf"
+ paper = "Moss93.pdf, printed"
}
@article{Muld97,
@@ -37209,7 +37238,7 @@ paper = "Brea89.pdf"
applied to any language represented in Mmt. A plugin interface permits
injecting syntactic and semantic idiosyncrasies of individual formal
languages.",
- paper = "Rabe13a.pdf"
+ paper = "Rabe13a.pdf, printed"
}
@article{Rabe16,
@@ -37245,7 +37274,7 @@ paper = "Brea89.pdf"
the ideas behind and the results about Mmt. It focuses on showing how
Mmt. provides a theoretical and practical framework for the future of
logic.",
- paper = "Rabe16.pdf",
+ paper = "Rabe16.pdf, printed",
}
@article{Rabe17,
@@ -37268,7 +37297,7 @@ paper = "Brea89.pdf"
colimits. Our approach is based on the Mmt language, which lets us
combine formalist declarative representations (and thus the associated
tool support) with abstract categorical conceptualizations.",
- paper = "Rabe17.pdf"
+ paper = "Rabe17.pdf, printed"
}
@phdthesis{Rave91,
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 3f392ad..dd2df56 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -1905,7 +1905,7 @@ paper = "Brea89.pdf"
volume = "146",
year = "1969",
pages = "29-60",
- paper = "Hind69.pdf"
+ paper = "Hind69.pdf, printed"
}
\end{chunk}
@@ -3183,7 +3183,7 @@ paper = "Brea89.pdf"
avoiding anomalies in the interaction of implicit conversions and
generic operators. The definition of a simple imperative language
(without any binding mechanisms) is used as an example.",
- paper = "Reyn80.pdf"
+ paper = "Reyn80.pdf, printed"
}
\end{chunk}
@@ -9782,7 +9782,7 @@ when shown in factored form.
exculded middle similar to Brouwer's had been advanced in print by
Jules Molk two years before. Finally, we discuss the influence on
George Griss' negationless mathematics",
- paper = "Atte15.pdf"
+ paper = "Atte15.pdf, printed"
}
\end{chunk}
@@ -10057,7 +10057,7 @@ when shown in factored form.
proof assistant, a tool for machine-checked mathematical theorem
proving; and formal logical reasoning about the correctness of
programs.",
- paper = "Chli17.pdf"
+ paper = "Chli17.pdf, printed"
}
\end{chunk}
@@ -10243,7 +10243,7 @@ when shown in factored form.
"We present an extensive set of mathematical propositions and proofs
in order to demonstrate the power of expression of the theory of
constructions.",
- paper = "Coqu85.pdf"
+ paper = "Coqu85.pdf, printed"
}
\end{chunk}
@@ -10468,6 +10468,18 @@ when shown in factored form.
\end{chunk}
+\index{Lakatos, Imre}
+\begin{chunk}{axiom.bib}
+@book{Laka76,
+ author = "Lakatos, Imre",
+ title = {{Proofs and Refutations}},
+ year = "1976",
+ publisher = "Cambridge University Press",
+ isbn = "978-1-107-53405-6"
+}
+
+\end{chunk}
+
\index{van Lamsweerde, Axel}
\begin{chunk}{axiom.bib}
@incollection{Lams00,
@@ -10582,6 +10594,30 @@ when shown in factored form.
\end{chunk}
+\index{Hall, Condelia V.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Hall94,
+ author = "Hall, Condelia V.",
+ title =
+ {{Using Hindley-Milner Type Inference to Optimize List Representation}},
+ booktitle = "LFP'94 Lisp and Functional Programming",
+ publisher = "ACM",
+ year = "1994",
+ pages = "162-172",
+ abstract =
+ "Lists are a pervasive data structure in functional programs. The
+ generality and simplicity of their structure makes them expensive.
+ Hindley-Mllner type inference and partial evalua- tion are all that is
+ needed to optimise this structure, yielding considerable improvements
+ in space and time consumption for some interesting programs. This
+ framework is applica- ble to many data types and their optimised
+ representations, such as lists and parallel implementations of bags,
+ or arrays and quadtrees.",
+ paper = "Hall94.pdf, printed"
+}
+
+\end{chunk}
+
\index{Manna, Zohar}
\index{Waldinger, Richard}
\begin{chunk}{axiom.bib}
@@ -10604,7 +10640,7 @@ when shown in factored form.
limitations of each technique as a practial programming aid are
assessed and attempts to implement these methods in experimental
systems are discussed.",
- paper = "Mann78.pdf"
+ paper = "Mann78.pdf, printed"
}
\end{chunk}
@@ -10616,7 +10652,8 @@ when shown in factored form.
title = {{Lectures on the Logic of Computer Programming}},
publisher = "Society for Industrial and Applied Mathematics",
year = "1980",
- paper = "Mann80.tgz"
+ paper = "Mann80.tgz",
+ keywords = "printed"
}
\end{chunk}
@@ -10849,7 +10886,7 @@ when shown in factored form.
application nodes. We motivate our design choices by a statistical
analysis of the uses of type inference in a sizable body of existing
ML code.",
- paper = "Pier97.pdf"
+ paper = "Pier97.pdf, printed"
}
\end{chunk}
@@ -10924,7 +10961,7 @@ when shown in factored form.
several principles (called search principles) which are applicable to
the design of efficient proof-procedures employing resolution as the
basic logical process.",
- paper = "Robi65.pdf"
+ paper = "Robi65.pdf, printed"
}
\end{chunk}
@@ -14617,7 +14654,7 @@ when shown in factored form.
abstract =
"The Hindley-Milner algorithm is described and an implementation in
Standard ML is presented.",
- paper = "Gran11.pdf"
+ paper = "Gran11.pdf, printed"
}
\end{chunk}
@@ -17230,7 +17267,7 @@ when shown in factored form.
proceed step by step or automatically and so on. The environment
enhances the effectiveness and flexibility of the reasoners of the
Theorema system.",
- paper = "Piro05.pdf"
+ paper = "Piro05.pdf, printed"
}
\end{chunk}
@@ -44722,7 +44759,7 @@ J. of Symbolic Computation 36 pp 513-533 (2003)
their problems. The system can be further extended in other to support
more constructs and increase its flexibility.",
paper = "Sant95.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, printed"
}
\end{chunk}
@@ -47648,7 +47685,7 @@ IBM Research Division Technical Report RC19530 May 1994
but even type checking is undecidable for relevant cases occurring in
computer algebra.",
paper = "Webe93b.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, printed"
}
\end{chunk}
@@ -54550,7 +54587,7 @@ SIAM J. Numer. Anal. 10 241--256. 1973
frameworks, focusing on their sort disciplines and assessing their
strengths and weaknesses for practical applications. Familiarity with
the basic notions of algebraic specification is assumed.",
- paper = "Moss93.pdf"
+ paper = "Moss93.pdf, printed"
}
\end{chunk}
@@ -55453,7 +55490,7 @@ ACM Transactions on Mathematical Software, 32(2):180-194, June 2006.
applied to any language represented in Mmt. A plugin interface permits
injecting syntactic and semantic idiosyncrasies of individual formal
languages.",
- paper = "Rabe13a.pdf"
+ paper = "Rabe13a.pdf, printed"
}
\end{chunk}
@@ -55493,7 +55530,7 @@ ACM Transactions on Mathematical Software, 32(2):180-194, June 2006.
the ideas behind and the results about Mmt. It focuses on showing how
Mmt. provides a theoretical and practical framework for the future of
logic.",
- paper = "Rabe16.pdf",
+ paper = "Rabe16.pdf, printed",
}
\end{chunk}
@@ -55520,7 +55557,7 @@ ACM Transactions on Mathematical Software, 32(2):180-194, June 2006.
colimits. Our approach is based on the Mmt language, which lets us
combine formalist declarative representations (and thus the associated
tool support) with abstract categorical conceptualizations.",
- paper = "Rabe17.pdf"
+ paper = "Rabe17.pdf, printed"
}
\end{chunk}
diff --git a/changelog b/changelog
index 1d13db9..f11b756 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20180119 tpd src/axiom-website/patches.html 20180119.02.tpd.patch
+20180119 tpd books/bookvolbib add references
20180119 tpd src/axiom-website/patches.html 20180119.01.tpd.patch
20180119 tpd src/axiom-website/documentation.html add hrefs to Daly book
20180114 tpd src/axiom-website/patches.html 20180114.01.tpd.patch
diff --git a/patch b/patch
index bb16460..6fcaa36 100644
--- a/patch
+++ b/patch
@@ -1,3 +1,39 @@
-src/axiom-website/documentation.html add hrefs to Daly book
+books/bookvolbib add references
-Goal: Axiom Documentation
+Goal: Proving Axiom Correct
+
+\index{Lakatos, Imre}
+\begin{chunk}{axiom.bib}
+@book{Laka76,
+ author = "Lakatos, Imre",
+ title = {{Proofs and Refutations}},
+ year = "1976",
+ publisher = "Cambridge University Press",
+ isbn = "978-1-107-53405-6"
+}
+
+\end{chunk}
+
+\index{Hall, Condelia V.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Hall94,
+ author = "Hall, Condelia V.",
+ title =
+ {{Using Hindley-Milner Type Inference to Optimize List Representation}},
+ booktitle = "LFP'94 Lisp and Functional Programming",
+ publisher = "ACM",
+ year = "1994",
+ pages = "162-172",
+ abstract =
+ "Lists are a pervasive data structure in functional programs. The
+ generality and simplicity of their structure makes them expensive.
+ Hindley-Mllner type inference and partial evalua- tion are all that is
+ needed to optimise this structure, yielding considerable improvements
+ in space and time consumption for some interesting programs. This
+ framework is applica- ble to many data types and their optimised
+ representations, such as lists and parallel implementations of bags,
+ or arrays and quadtrees.",
+ paper = "Hall94.pdf"
+}
+
+\end{chunk}
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index d225f5b..6d44be2 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5896,6 +5896,8 @@ books/bookvolbib add references

books/bookvol13 review Hoar87

20180119.01.tpd.patch
src/axiom-website/documentation.html add hrefs to Daly book
+20180119.02.tpd.patch
+books/bookvolbib add references

--
1.9.1