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