From 37748bd5240074fbd6a2c7c55b43bd5bc479632e Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Thu, 12 Jan 2017 15:49:36 -0500
Subject: [PATCH] books/bookvolbib References on Program Proofs
Goal: Proving Axiom Correct
\index{Bauer, Andrej}
\begin{chunk}{axiom.bib}
@article{Baue16,
author = "Bauer, Andrej",
title = "Five Stages of Accepting Constructive Mathematics",
year = "2016",
journal = "Bull. of the American Mathematical Society",
link = "\url{http://dx.doi.org/10.1090/bull/1556}",
abstract =
"On the odd day, a mathematician might wonder what constructive
mathematics is all about. They may have heard arguments in favor of
constructivism but are not at all convinced by them, and in any case
they may care little about philosophy. A typical introductory text
about constructivism spends a great deal of time explaining the
principles and contains only trivial mathematics, while advanced
constructive texts are impenetrable, like all unfamiliar mathematics.
How then can a mathematician find out what constructive mathematics
feels like? What new and relevant ideas does constructive mathematics
have to offer, if any? I shall attempt to answer these questions.",
paper = "Baue16.pdf"
}
\end{chunk}
\index{Bertot, Yves}
\index{Cast\'eran, Pierre}
\begin{chunk}{axiom.bib}
@book{Bert04,
author = {Bertot, Yves Cast\'eran, Pierre},
title = "Interactive Theorem Proving and Program Development",
publisher = "Springer",
year = "2004",
isbn = "3-540-20854-2",
abstract = "
Coq is an interactive proof assistant for the development of
mathematical theories and formally certified software. It is based on
a theory called the calculus of inductive constructions, a variant of
type theory.
This book provides a pragmatic introduction to the development of
proofs and certified programs using Coq. With its large collection of
examples and exercies it is an invaluable tool for researchers,
students, and engineers interested in formal methods and the
development of zero-fault software."
}
\end{chunk}
\index{Huet, G\'erard}
\index{Kahn, Gilles}
\index{Paulin-Mohring, Christine}
\begin{chunk}{axiom.bib}
@misc{Heut16,
author = {Huet, G\'erard and Kahn, Gilles and Paulin-Mohring, Christine},
title = "The COQ Proof Assistant. A Tutorial",
year = "2016",
link = "\url{https://coq.inria.fr/distrib/current/files/Tutorial.pdf}",
paper = "Heut16.pdf"
}
\end{chunk}
\index{Gimenez, Eduardo}
\index{Casteran, Pierre}
\begin{chunk}{axiom.bib}
@misc{Gime16,
author = "Gimenez, Eduardo and Casteran, Pierre",
title = "A Tutorial on [Co-]Inductive Types in Coq",
year = "2016",
link = "\url{https://coq.inria.fr/distrib/current/files/RecTutorial.pdf}",
abstract =
"This document is an introduction to the definition and use of
inductive and co-inductive types in the {\sl Coq} proof environment.
It explains how types like natural numbers and infinite streams are
defined in {\sl Coq}, and the kind of proof techniques that can be
used to reason about them (case analysis, induction, inversion of
predicates, co-induction, etc.) Each technique is illustrated
through an executable and self-contained {\sl Coq} script.",
paper = "Gime16.pdf"
}
\end{chunk}
\index{de Moura, Leonardo}
\index{Avigad, Jeremy}
\index{Kong, Soonho}
\index{Roux, Cody}
\begin{chunk}{axiom.bib}
@misc{Mour16,
author = "de Moura, Leonardo and Avigad, Jeremy and Kong, Soonho and
Roux, Cody",
title = "Elaboration in Dependent Type Theory",
year = "2016",
link = "\url{http://leodemoura.github.io/files/elaboration.pdf}",
abstract =
"We describe the elaboration algorithm that is used in {\sl Lean}, a
new interactive theorem prover based on dependent type theory. To be
practical, interactive theorem provers must provide mechanisms to
resolve ambiguities and infer implicit type information, thereby
supporting convenient input of expressions and proofs. Lean's
elaborator supports higher-order unification, ad-hoc overloading,
insertion of coercions, type class inference, the use of tactics, and
the computational reduction of terms. The interactions between these
components are subtle and complex, and Lean's elaborator has been
carefully designed to balance efficiency and usability.",
paper = "Mour16.pdf"
}
\end{chunk}
\index{Coquand, Thierry}
\index{Huet, G\'erard}
\index{Paulin, Christine}
\begin{chunk}{axiom.bib}
@misc{COQR16,
author = {Coquand, Thierry and Huet, G\'erard and Paulin, Christine},
title = "The COQ Proof Assistant Reference Manual",
year = "2016",
link="\url{https://coq.inria.fr/distrib/current/files/Reference-Manual.pdf}",
paper = "COQR16.pdf"
}
\end{chunk}
\index{Chlipala, Adam}
\index{Braibant, Thomas}
\index{Cuellar, Santiago}
\index{Delaware, Benjamin}
\index{Gross, Jason}
\index{Malecha, Gregory}
\index{Pit Clement,-Claudel}
\index{Wang, Peng}
\begin{chunk}{axiom.bib}
@misc{Chli14,
author = "Chlipala, Adam and Braibant, Thomas and Cuellar, Santiago and
Delaware, Benjamin and Gross, Jason and Malecha, Gregory, and
Clement,-Claudel, Pit and Wang, Peng",
title = "Bedrock: A Software Development Ecosystem Inside a Proof Assistant",
year = "2014",
link = "\url{https://www.youtube.com/watch?v=BSyrp-iYBMo}",
abstract =
"The benefits of formal correctness proofs for software are clear
intuitively, but the high human costs of proof construction have
generally been viewed as prohibitive. To support that integration, we
need to rethink the familiar programming toolchains. The new world
needn't be all about doing prodigious extra work to achieve the virtue
of correct programs; formal methods also suggest new programming
approaches that better support abstraction and modularity than do
coarser-grained specification styles like normal static types. This
talk overviews Bedrock, a framework for certified programming inside
of the Coq proof assistant. Bedrock programs are implemented,
specified, verified, and compiled inside of Coq. A single program may
be divided into modules with formal interfaces, written in different
programming languages and verified with different proof styles. The
common foundation is an assembly language with an operational
semantics (serving as the trusted code base) and a semantic module
system (orchestrating linking of code and proofs across source
languages). A few different programming styles have been connects to
the shared foundation, including a C-like language with an ``array of
bytes'' memory model, higher-level more C++-like languages with ``array
of abstract data types'' memory models, a domain-specific language for
XML processing, standard Coq functional programs, and even declarative
specifications that are refined automatically into assembly code with
correctness proofs. The talk will present Bedrock's shared foundation
and sketch the pieces that go into refining declarative specifications
into closed assembly programs, covering joint work with Thomas
Braibant, Santiago Cuellar, Benjamin Delaware, Jason Gross, Gregory
Malecha, Clement Pit-Claudel, and Peng Wang."
}
\end{chunk}
---
books/bookvolbib.pamphlet | 116 ++++++++++++++++++++++++++-
changelog | 3 +
patch | 176 +++++++++++++++++++++++++++++++++++++++-
src/axiom-website/patches.html | 2 +
4 files changed, 293 insertions(+), 4 deletions(-)
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 84b0e09..324de65 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -5514,6 +5514,30 @@ Martin, U.
\end{chunk}
+\index{Bauer, Andrej}
+\begin{chunk}{axiom.bib}
+@article{Baue16,
+ author = "Bauer, Andrej",
+ title = "Five Stages of Accepting Constructive Mathematics",
+ year = "2016",
+ journal = "Bull. of the American Mathematical Society",
+ link = "\url{http://dx.doi.org/10.1090/bull/1556}",
+ abstract =
+ "On the odd day, a mathematician might wonder what constructive
+ mathematics is all about. They may have heard arguments in favor of
+ constructivism but are not at all convinced by them, and in any case
+ they may care little about philosophy. A typical introductory text
+ about constructivism spends a great deal of time explaining the
+ principles and contains only trivial mathematics, while advanced
+ constructive texts are impenetrable, like all unfamiliar mathematics.
+ How then can a mathematician find out what constructive mathematics
+ feels like? What new and relevant ideas does constructive mathematics
+ have to offer, if any? I shall attempt to answer these questions.",
+ paper = "Baue16.pdf"
+}
+
+\end{chunk}
+
\index{Beeson, Michael}
\begin{chunk}{axiom.bib}
@misc{Beesxx,
@@ -5540,9 +5564,12 @@ Martin, U.
\index{Bertot, Yves}
\index{Cast\'eran, Pierre}
-\begin{chunk}{ignore}
-\bibitem[Bertot 04]{Bert04} Bertot, Yves; Cast\'eran, Pierre
+\begin{chunk}{axiom.bib}
+@book{Bert04,
+ author = {Bertot, Yves Cast\'eran, Pierre},
title = "Interactive Theorem Proving and Program Development",
+ publisher = "Springer",
+ year = "2004",
isbn = "3-540-20854-2",
abstract = "
Coq is an interactive proof assistant for the development of
@@ -5555,6 +5582,7 @@ Martin, U.
examples and exercies it is an invaluable tool for researchers,
students, and engineers interested in formal methods and the
development of zero-fault software."
+}
\end{chunk}
@@ -5704,6 +5732,55 @@ Martin, U.
\end{chunk}
+\index{Chlipala, Adam}
+\index{Braibant, Thomas}
+\index{Cuellar, Santiago}
+\index{Delaware, Benjamin}
+\index{Gross, Jason}
+\index{Malecha, Gregory}
+\index{Pit Clement,-Claudel}
+\index{Wang, Peng}
+\begin{chunk}{axiom.bib}
+@misc{Chli14,
+ author = "Chlipala, Adam and Braibant, Thomas and Cuellar, Santiago and
+ Delaware, Benjamin and Gross, Jason and Malecha, Gregory, and
+ Clement,-Claudel, Pit and Wang, Peng",
+ title = "Bedrock: A Software Development Ecosystem Inside a Proof Assistant",
+ year = "2014",
+ link = "\url{https://www.youtube.com/watch?v=BSyrp-iYBMo}",
+ abstract =
+ "The benefits of formal correctness proofs for software are clear
+ intuitively, but the high human costs of proof construction have
+ generally been viewed as prohibitive. To support that integration, we
+ need to rethink the familiar programming toolchains. The new world
+ needn't be all about doing prodigious extra work to achieve the virtue
+ of correct programs; formal methods also suggest new programming
+ approaches that better support abstraction and modularity than do
+ coarser-grained specification styles like normal static types. This
+ talk overviews Bedrock, a framework for certified programming inside
+ of the Coq proof assistant. Bedrock programs are implemented,
+ specified, verified, and compiled inside of Coq. A single program may
+ be divided into modules with formal interfaces, written in different
+ programming languages and verified with different proof styles. The
+ common foundation is an assembly language with an operational
+ semantics (serving as the trusted code base) and a semantic module
+ system (orchestrating linking of code and proofs across source
+ languages). A few different programming styles have been connects to
+ the shared foundation, including a C-like language with an ``array of
+ bytes'' memory model, higher-level more C++-like languages with ``array
+ of abstract data types'' memory models, a domain-specific language for
+ XML processing, standard Coq functional programs, and even declarative
+ specifications that are refined automatically into assembly code with
+ correctness proofs. The talk will present Bedrock's shared foundation
+ and sketch the pieces that go into refining declarative specifications
+ into closed assembly programs, covering joint work with Thomas
+ Braibant, Santiago Cuellar, Benjamin Delaware, Jason Gross, Gregory
+ Malecha, Clement Pit-Claudel, and Peng Wang."
+
+}
+
+\end{chunk}
+
\index{Coquand, Thierry}
\index{Huet, G\'erard}
\begin{chunk}{axiom.bib}
@@ -6211,6 +6288,27 @@ Calculemus (2011) Springer
\end{chunk}
+\index{Gimenez, Eduardo}
+\index{Casteran, Pierre}
+\begin{chunk}{axiom.bib}
+@misc{Gime16,
+ author = "Gimenez, Eduardo and Casteran, Pierre",
+ title = "A Tutorial on [Co-]Inductive Types in Coq",
+ year = "2016",
+ link = "\url{https://coq.inria.fr/distrib/current/files/RecTutorial.pdf}",
+ abstract =
+ "This document is an introduction to the definition and use of
+ inductive and co-inductive types in the {\sl Coq} proof environment.
+ It explains how types like natural numbers and infinite streams are
+ defined in {\sl Coq}, and the kind of proof techniques that can be
+ used to reason about them (case analysis, induction, inversion of
+ predicates, co-induction, etc.) Each technique is illustrated
+ through an executable and self-contained {\sl Coq} script.",
+ paper = "Gime16.pdf"
+}
+
+\end{chunk}
+
\index{Gottlieben, Hanne}
\index{Kelsey, Tom}
\index{Martin, Ursula}
@@ -6334,6 +6432,20 @@ Calculemus (2011) Springer
\end{chunk}
+\index{Huet, G\'erard}
+\index{Kahn, Gilles}
+\index{Paulin-Mohring, Christine}
+\begin{chunk}{axiom.bib}
+@misc{Heut16,
+ author = {Huet, G\'erard and Kahn, Gilles and Paulin-Mohring, Christine},
+ title = "The COQ Proof Assistant. A Tutorial",
+ year = "2016",
+ link = "\url{https://coq.inria.fr/distrib/current/files/Tutorial.pdf}",
+ paper = "Heut16.pdf"
+}
+
+\end{chunk}
+
\index{Jackson, Paul Bernard}
\begin{chunk}{axiom.bib}
@phdthesis{Jack95,
diff --git a/changelog b/changelog
index a4d3919..d753837 100644
--- a/changelog
+++ b/changelog
@@ -1,7 +1,10 @@
+20170112 tpd src/axiom-website/patches.html 20170112.01.tpd.patch
+20170112 tpd books/bookvolbib References on Program Proofs
20170109 tpd src/axiom-website/patches.html 20170109.01.tpd.patch
20170109 tpd books/bookheader.tex add Wolfgang Brehm to credit list
20170109 tpd books/bookvol10.4 add Wolfgang Brehm to credit list
20170109 tpd books/bookvol5 add Wolfgang Brehm to credit list
+20170109 tpd books/bookvolbib cleanup broken links
20170109 tpd src/input/unittest1.input add Wolfgang Brehm to credit list
20170109 tpd readme add Wolfgang Brehm to credit list
20170105 tpd src/axiom-website/patches.html 20170105.01.tpd.patch
diff --git a/patch b/patch
index b85bd93..0e1d038 100644
--- a/patch
+++ b/patch
@@ -1,4 +1,176 @@
-readme add Wolfgang Brehm to credit list
+books/bookvolbib References on Program Proofs
-Goal: Axiom Credit List
+Goal: Proving Axiom Correct
+\index{Bauer, Andrej}
+\begin{chunk}{axiom.bib}
+@article{Baue16,
+ author = "Bauer, Andrej",
+ title = "Five Stages of Accepting Constructive Mathematics",
+ year = "2016",
+ journal = "Bull. of the American Mathematical Society",
+ link = "\url{http://dx.doi.org/10.1090/bull/1556}",
+ abstract =
+ "On the odd day, a mathematician might wonder what constructive
+ mathematics is all about. They may have heard arguments in favor of
+ constructivism but are not at all convinced by them, and in any case
+ they may care little about philosophy. A typical introductory text
+ about constructivism spends a great deal of time explaining the
+ principles and contains only trivial mathematics, while advanced
+ constructive texts are impenetrable, like all unfamiliar mathematics.
+ How then can a mathematician find out what constructive mathematics
+ feels like? What new and relevant ideas does constructive mathematics
+ have to offer, if any? I shall attempt to answer these questions.",
+ paper = "Baue16.pdf"
+}
+
+\end{chunk}
+
+\index{Bertot, Yves}
+\index{Cast\'eran, Pierre}
+\begin{chunk}{axiom.bib}
+@book{Bert04,
+ author = {Bertot, Yves Cast\'eran, Pierre},
+ title = "Interactive Theorem Proving and Program Development",
+ publisher = "Springer",
+ year = "2004",
+ isbn = "3-540-20854-2",
+ abstract = "
+ Coq is an interactive proof assistant for the development of
+ mathematical theories and formally certified software. It is based on
+ a theory called the calculus of inductive constructions, a variant of
+ type theory.
+
+ This book provides a pragmatic introduction to the development of
+ proofs and certified programs using Coq. With its large collection of
+ examples and exercies it is an invaluable tool for researchers,
+ students, and engineers interested in formal methods and the
+ development of zero-fault software."
+}
+
+\end{chunk}
+
+\index{Huet, G\'erard}
+\index{Kahn, Gilles}
+\index{Paulin-Mohring, Christine}
+\begin{chunk}{axiom.bib}
+@misc{Heut16,
+ author = {Huet, G\'erard and Kahn, Gilles and Paulin-Mohring, Christine},
+ title = "The COQ Proof Assistant. A Tutorial",
+ year = "2016",
+ link = "\url{https://coq.inria.fr/distrib/current/files/Tutorial.pdf}",
+ paper = "Heut16.pdf"
+}
+
+\end{chunk}
+
+\index{Gimenez, Eduardo}
+\index{Casteran, Pierre}
+\begin{chunk}{axiom.bib}
+@misc{Gime16,
+ author = "Gimenez, Eduardo and Casteran, Pierre",
+ title = "A Tutorial on [Co-]Inductive Types in Coq",
+ year = "2016",
+ link = "\url{https://coq.inria.fr/distrib/current/files/RecTutorial.pdf}",
+ abstract =
+ "This document is an introduction to the definition and use of
+ inductive and co-inductive types in the {\sl Coq} proof environment.
+ It explains how types like natural numbers and infinite streams are
+ defined in {\sl Coq}, and the kind of proof techniques that can be
+ used to reason about them (case analysis, induction, inversion of
+ predicates, co-induction, etc.) Each technique is illustrated
+ through an executable and self-contained {\sl Coq} script.",
+ paper = "Gime16.pdf"
+}
+
+\end{chunk}
+
+\index{de Moura, Leonardo}
+\index{Avigad, Jeremy}
+\index{Kong, Soonho}
+\index{Roux, Cody}
+\begin{chunk}{axiom.bib}
+@misc{Mour16,
+ author = "de Moura, Leonardo and Avigad, Jeremy and Kong, Soonho and
+ Roux, Cody",
+ title = "Elaboration in Dependent Type Theory",
+ year = "2016",
+ link = "\url{http://leodemoura.github.io/files/elaboration.pdf}",
+ abstract =
+ "We describe the elaboration algorithm that is used in {\sl Lean}, a
+ new interactive theorem prover based on dependent type theory. To be
+ practical, interactive theorem provers must provide mechanisms to
+ resolve ambiguities and infer implicit type information, thereby
+ supporting convenient input of expressions and proofs. Lean's
+ elaborator supports higher-order unification, ad-hoc overloading,
+ insertion of coercions, type class inference, the use of tactics, and
+ the computational reduction of terms. The interactions between these
+ components are subtle and complex, and Lean's elaborator has been
+ carefully designed to balance efficiency and usability.",
+ paper = "Mour16.pdf"
+}
+
+\end{chunk}
+
+\index{Coquand, Thierry}
+\index{Huet, G\'erard}
+\index{Paulin, Christine}
+\begin{chunk}{axiom.bib}
+@misc{COQR16,
+ author = {Coquand, Thierry and Huet, G\'erard and Paulin, Christine},
+ title = "The COQ Proof Assistant Reference Manual",
+ year = "2016",
+ link="\url{https://coq.inria.fr/distrib/current/files/Reference-Manual.pdf}",
+ paper = "COQR16.pdf"
+}
+
+\end{chunk}
+
+\index{Chlipala, Adam}
+\index{Braibant, Thomas}
+\index{Cuellar, Santiago}
+\index{Delaware, Benjamin}
+\index{Gross, Jason}
+\index{Malecha, Gregory}
+\index{Pit Clement,-Claudel}
+\index{Wang, Peng}
+\begin{chunk}{axiom.bib}
+@misc{Chli14,
+ author = "Chlipala, Adam and Braibant, Thomas and Cuellar, Santiago and
+ Delaware, Benjamin and Gross, Jason and Malecha, Gregory, and
+ Clement,-Claudel, Pit and Wang, Peng",
+ title = "Bedrock: A Software Development Ecosystem Inside a Proof Assistant",
+ year = "2014",
+ link = "\url{https://www.youtube.com/watch?v=BSyrp-iYBMo}",
+ abstract =
+ "The benefits of formal correctness proofs for software are clear
+ intuitively, but the high human costs of proof construction have
+ generally been viewed as prohibitive. To support that integration, we
+ need to rethink the familiar programming toolchains. The new world
+ needn't be all about doing prodigious extra work to achieve the virtue
+ of correct programs; formal methods also suggest new programming
+ approaches that better support abstraction and modularity than do
+ coarser-grained specification styles like normal static types. This
+ talk overviews Bedrock, a framework for certified programming inside
+ of the Coq proof assistant. Bedrock programs are implemented,
+ specified, verified, and compiled inside of Coq. A single program may
+ be divided into modules with formal interfaces, written in different
+ programming languages and verified with different proof styles. The
+ common foundation is an assembly language with an operational
+ semantics (serving as the trusted code base) and a semantic module
+ system (orchestrating linking of code and proofs across source
+ languages). A few different programming styles have been connects to
+ the shared foundation, including a C-like language with an ``array of
+ bytes'' memory model, higher-level more C++-like languages with ``array
+ of abstract data types'' memory models, a domain-specific language for
+ XML processing, standard Coq functional programs, and even declarative
+ specifications that are refined automatically into assembly code with
+ correctness proofs. The talk will present Bedrock's shared foundation
+ and sketch the pieces that go into refining declarative specifications
+ into closed assembly programs, covering joint work with Thomas
+ Braibant, Santiago Cuellar, Benjamin Delaware, Jason Gross, Gregory
+ Malecha, Clement Pit-Claudel, and Peng Wang."
+
+}
+
+\end{chunk}
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index be1446d..f1e9e07 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5626,6 +5626,8 @@ books/bookvol13 books/bookvol13 COQ details

books/axiom.bst add link, isbn to biblio entries

20170109.01.tpd.patch
readme add Wolfgang Brehm to credit list

+20170112.01.tpd.patch
+books/bookvolbib References on Program Proofs

--
1.7.5.4