From 81b381a8e2536b4adac15cc5cad0b89a6fcfdf48 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Sun, 24 Dec 2017 19:26:26 -0500
Subject: [PATCH] books/bookvolbib adding references
Goal: Proving Axiom Correct
\index{Pfenning, Frank}
\begin{chunk}{axiom.bib}
@inproceedings{Pfen88,
author = "Pfenning, Frank",
title = {{Partial Polymorphic Type Inference and Higher-Order Unification}},
booktitle = "Proc 1988 ACM Conf. on Lisp and Functional Programming",
pages = "153-163",
year = "1988",
publisher = "ACM",
isbn = "0-89791-273-X",
abstract =
"We show that the problem of partial type inference in the $n$-th
order polymorphic $\lambda$-calculus is equivalent to $n$-th order
unification. On the one hand, this means that partial type inference
in polymorphic $\lambda$-calculi of order 2 or higher is
undecidable. On the other hand, higher-order unification is often
tractable in practice, and our translation entails a very useful
algorithm for partial type inference in the $omega$-order polymorphic
$\lambda$-calculus. We present an implementation in $\lambda$Prolog in
full.",
paper = "Pfen88.pdf"
}
\end{chunk}
\index{Chlipala, Adam}
\begin{chunk}{axiom.bib}
@book{Chli17,
author = "Chlipala, Adam",
title = {{Formal Reasoning About Programs}},
year = "2017",
publisher = "MIT",
link = "\url{http://adam.chlipala.net/frap/frap_book.pdf}",
abstract =
"Briefly, this book is about an approach to bringing software
engineering up to speed with more traditional engineering disciplines,
providing a mathematical foundation for rigorous analysis of realistic
computer systems. As civil engineers apply their mathematical canon to
reach high certainty that bridges will not fall down, the software
engineer should apply a different canon to argue that programs behave
properly. As other engineering disciplines have their computer-aided
design tools, computer science has proof assistants, IDEs for logical
arguments. We will learn how to apply these tools to certify that
programs behave as expected.
More specifically: Introductions to two intertangled subjects: the Coq
proof assistant, a tool for machine-checked mathematical theorem
proving; and formal logical reasoning about the correctness of
programs.",
paper = "Chli17.pdf"
}
\end{chunk}
\index{van Atten, Mark}
\index{Sundholm, Goran}
\begin{chunk}{axiom.bib}
@misc{Atte15,
author = "van Atten, Mark and Sundholm, Goran",
title = {{L.E.J. Brouwer's 'Unrelability of the Logical Principles'
translation}},
year = "2015",
link = "\url{https://arxiv.org/pdf/1511.01113.pdf}",
abstract =
"We present a new English translation of L.E.J. Brouwer's paper 'De
onbetrouwbaarheid der logische principes' (The unreliability of the
logical principles) of 1908, together with a philosophical and
historical introduction. In this paper Brouwer for the first time
objected to the idea that the Principle of the Excluded Middle is
valid. We discuss the circumstances under which the manuscript was
submitted and accepted, Brouwer's ideas on the principle of the
excluded middle, and its consistency and partial validity, and his
argument against the possibility of absolutely undecidable
propositions. We not that principled objections to the general
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"
}
\end{chunk}
\begin{chunk}{axiom.bib}
@misc{Cyph17,
author = "Cypherpunks",
title = {{Chapter 4: Verification Techniques}},
link = "\url{http://www.cypherpunks.to/~peter/04_verif_techniques.pdf}",
year = "2017",
abstract = "Wherein existing methods for building secure systems are
examined and found wanting",
paper = "Cyph17.pdf"
}
\end{chunk}
---
books/axiom.bib | 79 ++++++++++++++++++++++++++++++++++
books/bookvolbib.pamphlet | 95 +++++++++++++++++++++++++++++++++++++++++
changelog | 2 +
patch | 97 +++++++++++++++++++++++++++++++++++++++++-
src/axiom-website/patches.html | 2 +
5 files changed, 273 insertions(+), 2 deletions(-)
diff --git a/books/axiom.bib b/books/axiom.bib
index 0ec17da..81a33a0 100644
--- a/books/axiom.bib
+++ b/books/axiom.bib
@@ -6947,6 +6947,64 @@ paper = "Brea89.pdf"
paper = "Yous04.pdf"
}
+@misc{Atte15,
+ author = "van Atten, Mark and Sundholm, Goran",
+ title = {{L.E.J. Brouwer's 'Unrelability of the Logical Principles'
+ translation}},
+ year = "2015",
+ link = "\url{https://arxiv.org/pdf/1511.01113.pdf}",
+ abstract =
+ "We present a new English translation of L.E.J. Brouwer's paper 'De
+ onbetrouwbaarheid der logische principes' (The unreliability of the
+ logical principles) of 1908, together with a philosophical and
+ historical introduction. In this paper Brouwer for the first time
+ objected to the idea that the Principle of the Excluded Middle is
+ valid. We discuss the circumstances under which the manuscript was
+ submitted and accepted, Brouwer's ideas on the principle of the
+ excluded middle, and its consistency and partial validity, and his
+ argument against the possibility of absolutely undecidable
+ propositions. We not that principled objections to the general
+ 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"
+}
+
+@book{Chli17,
+ author = "Chlipala, Adam",
+ title = {{Formal Reasoning About Programs}},
+ year = "2017",
+ publisher = "MIT",
+ link = "\url{http://adam.chlipala.net/frap/frap_book.pdf}",
+ abstract =
+ "Briefly, this book is about an approach to bringing software
+ engineering up to speed with more traditional engineering disciplines,
+ providing a mathematical foundation for rigorous analysis of realistic
+ computer systems. As civil engineers apply their mathematical canon to
+ reach high certainty that bridges will not fall down, the software
+ engineer should apply a different canon to argue that programs behave
+ properly. As other engineering disciplines have their computer-aided
+ design tools, computer science has proof assistants, IDEs for logical
+ arguments. We will learn how to apply these tools to certify that
+ programs behave as expected.
+
+ More specifically: Introductions to two intertangled subjects: the Coq
+ proof assistant, a tool for machine-checked mathematical theorem
+ proving; and formal logical reasoning about the correctness of
+ programs.",
+ paper = "Chli17.pdf"
+}
+
+@misc{Cyph17,
+ author = "Cypherpunks",
+ title = {{Chapter 4: Verification Techniques}},
+ link = "\url{http://www.cypherpunks.to/~peter/04_verif_techniques.pdf}",
+ year = "2017",
+ abstract = "Wherein existing methods for building secure systems are
+ examined and found wanting",
+ paper = "Cyph17.pdf"
+}
+
@article{Cons85a,
author = "Constable, R.L. and Knoblock, T.B. and Gates, J.L.",
title = {{Writing Programs that Construct Proofs}},
@@ -11709,6 +11767,27 @@ paper = "Brea89.pdf"
paper = "Pell91.pdf"
}
+@inproceedings{Pfen88,
+ author = "Pfenning, Frank",
+ title = {{Partial Polymorphic Type Inference and Higher-Order Unification}},
+ booktitle = "Proc 1988 ACM Conf. on Lisp and Functional Programming",
+ pages = "153-163",
+ year = "1988",
+ publisher = "ACM",
+ isbn = "0-89791-273-X",
+ abstract =
+ "We show that the problem of partial type inference in the $n$-th
+ order polymorphic $\lambda$-calculus is equivalent to $n$-th order
+ unification. On the one hand, this means that partial type inference
+ in polymorphic $\lambda$-calculi of order 2 or higher is
+ undecidable. On the other hand, higher-order unification is often
+ tractable in practice, and our translation entails a very useful
+ algorithm for partial type inference in the $omega$-order polymorphic
+ $\lambda$-calculus. We present an implementation in $\lambda$Prolog in
+ full.",
+ paper = "Pfen88.pdf"
+}
+
@techreport{Pfen89,
author = "Pfenning, Frank and Paulin-Mohring, Christine",
title = {{Inductively Defined Types in the Calculus of Constructions}},
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index f0e5fb8..3bbe9ee 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -9448,6 +9448,76 @@ when shown in factored form.
\section{Proving Axiom Correct -- The Project} %%%%%%%%%%%%%%%%%%%%
+\index{van Atten, Mark}
+\index{Sundholm, Goran}
+\begin{chunk}{axiom.bib}
+@misc{Atte15,
+ author = "van Atten, Mark and Sundholm, Goran",
+ title = {{L.E.J. Brouwer's 'Unrelability of the Logical Principles'
+ translation}},
+ year = "2015",
+ link = "\url{https://arxiv.org/pdf/1511.01113.pdf}",
+ abstract =
+ "We present a new English translation of L.E.J. Brouwer's paper 'De
+ onbetrouwbaarheid der logische principes' (The unreliability of the
+ logical principles) of 1908, together with a philosophical and
+ historical introduction. In this paper Brouwer for the first time
+ objected to the idea that the Principle of the Excluded Middle is
+ valid. We discuss the circumstances under which the manuscript was
+ submitted and accepted, Brouwer's ideas on the principle of the
+ excluded middle, and its consistency and partial validity, and his
+ argument against the possibility of absolutely undecidable
+ propositions. We not that principled objections to the general
+ 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"
+}
+
+\end{chunk}
+
+\index{Chlipala, Adam}
+\begin{chunk}{axiom.bib}
+@book{Chli17,
+ author = "Chlipala, Adam",
+ title = {{Formal Reasoning About Programs}},
+ year = "2017",
+ publisher = "MIT",
+ link = "\url{http://adam.chlipala.net/frap/frap_book.pdf}",
+ abstract =
+ "Briefly, this book is about an approach to bringing software
+ engineering up to speed with more traditional engineering disciplines,
+ providing a mathematical foundation for rigorous analysis of realistic
+ computer systems. As civil engineers apply their mathematical canon to
+ reach high certainty that bridges will not fall down, the software
+ engineer should apply a different canon to argue that programs behave
+ properly. As other engineering disciplines have their computer-aided
+ design tools, computer science has proof assistants, IDEs for logical
+ arguments. We will learn how to apply these tools to certify that
+ programs behave as expected.
+
+ More specifically: Introductions to two intertangled subjects: the Coq
+ proof assistant, a tool for machine-checked mathematical theorem
+ proving; and formal logical reasoning about the correctness of
+ programs.",
+ paper = "Chli17.pdf"
+}
+
+\end{chunk}
+
+\begin{chunk}{axiom.bib}
+@misc{Cyph17,
+ author = "Cypherpunks",
+ title = {{Chapter 4: Verification Techniques}},
+ link = "\url{http://www.cypherpunks.to/~peter/04_verif_techniques.pdf}",
+ year = "2017",
+ abstract = "Wherein existing methods for building secure systems are
+ examined and found wanting",
+ paper = "Cyph17.pdf"
+}
+
+\end{chunk}
+
\index{Constable, R.L.}
\index{Knoblock, T.B.}
\index{Gates, J.L.}
@@ -15564,6 +15634,31 @@ when shown in factored form.
\end{chunk}
\index{Pfenning, Frank}
+\begin{chunk}{axiom.bib}
+@inproceedings{Pfen88,
+ author = "Pfenning, Frank",
+ title = {{Partial Polymorphic Type Inference and Higher-Order Unification}},
+ booktitle = "Proc 1988 ACM Conf. on Lisp and Functional Programming",
+ pages = "153-163",
+ year = "1988",
+ publisher = "ACM",
+ isbn = "0-89791-273-X",
+ abstract =
+ "We show that the problem of partial type inference in the $n$-th
+ order polymorphic $\lambda$-calculus is equivalent to $n$-th order
+ unification. On the one hand, this means that partial type inference
+ in polymorphic $\lambda$-calculi of order 2 or higher is
+ undecidable. On the other hand, higher-order unification is often
+ tractable in practice, and our translation entails a very useful
+ algorithm for partial type inference in the $omega$-order polymorphic
+ $\lambda$-calculus. We present an implementation in $\lambda$Prolog in
+ full.",
+ paper = "Pfen88.pdf"
+}
+
+\end{chunk}
+
+\index{Pfenning, Frank}
\index{Paulin-Mohring, Christine}
\begin{chunk}{axiom.bib}
@techreport{Pfen89,
diff --git a/changelog b/changelog
index 3cf5b68..36360f7 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20171224 tpd src/axiom-website/patches.html 20171224.01.tpd.patch
+20171224 tpd books/bookvolbib add references
20171217 tpd src/axiom-website/patches.html 20171217.01.tpd.patch
20171217 tpd books/bookvol5 fix typos
20171216 tpd src/axiom-website/patches.html 20171216.02.tpd.patch
diff --git a/patch b/patch
index a02e70d..e130d3d 100644
--- a/patch
+++ b/patch
@@ -1,5 +1,98 @@
-books/bookvol5 fix typos
+books/bookvolbib adding references
-Goal: Axiom Literate Programming
+Goal: Proving Axiom Correct
+\index{Pfenning, Frank}
+\begin{chunk}{axiom.bib}
+@inproceedings{Pfen88,
+ author = "Pfenning, Frank",
+ title = {{Partial Polymorphic Type Inference and Higher-Order Unification}},
+ booktitle = "Proc 1988 ACM Conf. on Lisp and Functional Programming",
+ pages = "153-163",
+ year = "1988",
+ publisher = "ACM",
+ isbn = "0-89791-273-X",
+ abstract =
+ "We show that the problem of partial type inference in the $n$-th
+ order polymorphic $\lambda$-calculus is equivalent to $n$-th order
+ unification. On the one hand, this means that partial type inference
+ in polymorphic $\lambda$-calculi of order 2 or higher is
+ undecidable. On the other hand, higher-order unification is often
+ tractable in practice, and our translation entails a very useful
+ algorithm for partial type inference in the $omega$-order polymorphic
+ $\lambda$-calculus. We present an implementation in $\lambda$Prolog in
+ full.",
+ paper = "Pfen88.pdf"
+}
+\end{chunk}
+
+\index{Chlipala, Adam}
+\begin{chunk}{axiom.bib}
+@book{Chli17,
+ author = "Chlipala, Adam",
+ title = {{Formal Reasoning About Programs}},
+ year = "2017",
+ publisher = "MIT",
+ link = "\url{http://adam.chlipala.net/frap/frap_book.pdf}",
+ abstract =
+ "Briefly, this book is about an approach to bringing software
+ engineering up to speed with more traditional engineering disciplines,
+ providing a mathematical foundation for rigorous analysis of realistic
+ computer systems. As civil engineers apply their mathematical canon to
+ reach high certainty that bridges will not fall down, the software
+ engineer should apply a different canon to argue that programs behave
+ properly. As other engineering disciplines have their computer-aided
+ design tools, computer science has proof assistants, IDEs for logical
+ arguments. We will learn how to apply these tools to certify that
+ programs behave as expected.
+
+ More specifically: Introductions to two intertangled subjects: the Coq
+ proof assistant, a tool for machine-checked mathematical theorem
+ proving; and formal logical reasoning about the correctness of
+ programs.",
+ paper = "Chli17.pdf"
+}
+
+\end{chunk}
+
+\index{van Atten, Mark}
+\index{Sundholm, Goran}
+\begin{chunk}{axiom.bib}
+@misc{Atte15,
+ author = "van Atten, Mark and Sundholm, Goran",
+ title = {{L.E.J. Brouwer's 'Unrelability of the Logical Principles'
+ translation}},
+ year = "2015",
+ link = "\url{https://arxiv.org/pdf/1511.01113.pdf}",
+ abstract =
+ "We present a new English translation of L.E.J. Brouwer's paper 'De
+ onbetrouwbaarheid der logische principes' (The unreliability of the
+ logical principles) of 1908, together with a philosophical and
+ historical introduction. In this paper Brouwer for the first time
+ objected to the idea that the Principle of the Excluded Middle is
+ valid. We discuss the circumstances under which the manuscript was
+ submitted and accepted, Brouwer's ideas on the principle of the
+ excluded middle, and its consistency and partial validity, and his
+ argument against the possibility of absolutely undecidable
+ propositions. We not that principled objections to the general
+ 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"
+}
+
+\end{chunk}
+
+\begin{chunk}{axiom.bib}
+@misc{Cyph17,
+ author = "Cypherpunks",
+ title = {{Chapter 4: Verification Techniques}},
+ link = "\url{http://www.cypherpunks.to/~peter/04_verif_techniques.pdf}",
+ year = "2017",
+ abstract = "Wherein existing methods for building secure systems are
+ examined and found wanting",
+ paper = "Cyph17.pdf"
+}
+
+\end{chunk}
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 784b4b8..3d10bd1 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5874,6 +5874,8 @@ books/bookvol9 railroad syntax diagrams fix v9Expression

src/interp/i-output.lisp document CHARYBDIS

20171217.01.tpd.patch
books/bookvol5 fix typos

+20171224.01.tpd.patch
+books/bookvolbib add references

--
1.9.1