From bbd9b94fb5ad7c6f63acb55b57fc4ee6e761d8e0 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Wed, 18 Jan 2017 14:44:52 -0500
Subject: [PATCH] books/bookvol13 pre/post conditions and Coq nat vs Axiom NNI
Goal: Proving Axiom Correct
\index{Chlipala, Adam}
\begin{chunk}{axiom.bib}
@article{Chli10,
author = "Chlipala, Adam",
title = "An Introduction to Programming and Proving with Dependent Types
in Coq",
journal = "Journal of Formalized Reasoning",
volume = "3",
number = "2",
pages = "1-93",
year = "2010",
paper = "Chli10.pdf"
}
\end{chunk}
\index{Boldo, Sylvie}
\index{March\'e, Claude}
\begin{chunk}{axiom.bib}
@article{Bold11,
author = "Boldo, Sylvie and Marche, Claude",
title = "Formal verification of numerical programs: from C annotated
programs to mechanical proofs",
year = "2011",
publisher = "Springer",
journal = "Mathematics in Computer Science",
volume = "5",
pages = "377-393",
link = "\url{https://hal.archives-ouvertes.fr/hal-00777605/document}",
abstract =
"Numerical programs may require a high level of guarantee. This can be
achieved by applying formal methods, such as machine-checked proofs.
But these tools handle mathematical theorems while we are interested
in C code, in which numerical computations are performed using
floating-point arithmetic, whereas proof tools typically handle exact
real arithmetic. To achieve this high level of confidence on C programs,
we use a chain of tools: Frama-C, its Jessie plugin, Why and provers
among Coq, Gappa, Alt-Ergo, CVC3 and Z3. This approach requires the C
program to be annotated; each function must be precisely specified, and
we prove the correctness of the program by proving both that it meets its
specifications and that no runtime error may occur. The purpose of this
paper is to illustrate, on various examples, the features of this
approach.",
paper = "Bold11.pdf"
}
\end{chunk}
\index{Boldo, Sylvie}
\index{Filliatre, Jean-Christophe}
\begin{chunk}{axiom.bib}
@misc{Bold07,
author = "Boldo, Sylvie and Filliatre, Jean-Christophe}",
title = "Formal Verification of Floating-Point programs",
link = "\url{http://www-lipn.univ-paris13.fr/CerPAN/files/ARITH.pdf}",
paper = "Bold07.pdf"
}
\end{chunk}
\index{Boldo, Sylvie}
\index{Filliatre, Jean-Christophe}
\begin{chunk}{axiom.bib}
@misc{Bold07a,
author = "Boldo, Sylvie and Filliatre, Jean-Christophe",
title = "Formal Verification of Floating-Point programs",
link = "\url{http://www.lri.fr/~filliatr/ftp/publis/caduceus-floats.pdf}",
abstract =
"This paper introduces a methodology to perform formal verification of
floating-point C programs. It extends an existing tool for
verification of C programs, Caduceus, with new annotations for
specific floating-point arithmetic. The Caduceus first-order logic
model for C programs is extended accordingly. Then verification
conditions are obtained in the usual way and can be discharged
interactively with the Coqa proof assistant, using an existing Coq
formalization of floating-point arithmetic. This methodology is
already implemented and has been successfully applied to several short
floating-point programs, which are presented in this paper.",
paper = "Bold07a.pdf"
}
\end{chunk}
\index{Wadler, Philip}
\begin{chunk}{axiom.bib}
@misc{Wadl14,
author = "Wadler, Philip",
title = "Propositions as Types",
year = "2014",
link = "\url{http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf}",
paper = "Wadl14.pdf"
}
\end{chunk}
\begin{chunk}{axiom.bib}
@misc{COQnat,
author = "COQ Proof Assistant",
title = "{Library} {Coq}.{Init}.{Nat}",
link = "\url{https://coq.inria.fr/library/Coq.Init.Nat.html}",
abstract = "Peano natural numbers, defintions of operations",
year = "2017"
}
\end{chunk}
\index{Pierce, Benjamin C.}
\begin{chunk}{axiom.bib}
@book{Pier00,
author = "Pierce, Benjamin C.",
title = "Type Systems for Programming Languages",
year = "2000",
publisher = "MIT Press",
link = "\url{http://ropas.snu.ac.kr/~kwang/S20/pierce\_book.pdf}",
paper = "Pier00.pdf"
}
\end{chunk}
---
books/bookvolbib.pamphlet | 29 +++++++++++++++++++++++++++++
changelog | 2 ++
patch | 29 +++++++++++++++++++++++++++++
src/axiom-website/patches.html | 2 ++
4 files changed, 62 insertions(+), 0 deletions(-)
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index b692b79..5f55bda 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -5822,6 +5822,22 @@ Martin, U.
\end{chunk}
\index{Chlipala, Adam}
+\begin{chunk}{axiom.bib}
+@article{Chli10,
+ author = "Chlipala, Adam",
+ title = "An Introduction to Programming and Proving with Dependent Types
+ in Coq",
+ journal = "Journal of Formalized Reasoning",
+ volume = "3",
+ number = "2",
+ pages = "1-93",
+ year = "2010",
+ paper = "Chli10.pdf"
+}
+
+\end{chunk}
+
+\index{Chlipala, Adam}
\index{Braibant, Thomas}
\index{Cuellar, Santiago}
\index{Delaware, Benjamin}
@@ -7090,6 +7106,19 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\end{chunk}
+\index{Pierce, Benjamin C.}
+\begin{chunk}{axiom.bib}
+@book{Pier00,
+ author = "Pierce, Benjamin C.",
+ title = "Type Systems for Programming Languages",
+ year = "2000",
+ publisher = "MIT Press",
+ link = "\url{http://ropas.snu.ac.kr/~kwang/S20/pierce\_book.pdf}",
+ paper = "Pier00.pdf"
+}
+
+\end{chunk}
+
\index{Poll, Erik}
\index{Thompson, Simon}
\begin{chunk}{axiom.bib}
diff --git a/changelog b/changelog
index 7a27853..1251cb8 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20170118 tpd src/axiom-website/patches.html 20170118.01.tpd.patch
+20170118 tpd books/bookvolbib References on Program Proofs
20170113 tpd src/axiom-website/patches.html 20170113.01.tpd.patch
20170113 tpd books/bookvol13 pre/post conditions and Coq nat vs Axiom NNI
20170113 tpd books/bookvolbib pre/post conditions and Coq nat vs Axiom NNI
diff --git a/patch b/patch
index 693790e..c79e8d3 100644
--- a/patch
+++ b/patch
@@ -2,6 +2,22 @@ books/bookvol13 pre/post conditions and Coq nat vs Axiom NNI
Goal: Proving Axiom Correct
+\index{Chlipala, Adam}
+\begin{chunk}{axiom.bib}
+@article{Chli10,
+ author = "Chlipala, Adam",
+ title = "An Introduction to Programming and Proving with Dependent Types
+ in Coq",
+ journal = "Journal of Formalized Reasoning",
+ volume = "3",
+ number = "2",
+ pages = "1-93",
+ year = "2010",
+ paper = "Chli10.pdf"
+}
+
+\end{chunk}
+
\index{Boldo, Sylvie}
\index{March\'e, Claude}
\begin{chunk}{axiom.bib}
@@ -92,3 +108,16 @@ Goal: Proving Axiom Correct
\end{chunk}
+\index{Pierce, Benjamin C.}
+\begin{chunk}{axiom.bib}
+@book{Pier00,
+ author = "Pierce, Benjamin C.",
+ title = "Type Systems for Programming Languages",
+ year = "2000",
+ publisher = "MIT Press",
+ link = "\url{http://ropas.snu.ac.kr/~kwang/S20/pierce\_book.pdf}",
+ paper = "Pier00.pdf"
+}
+
+\end{chunk}
+
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index e94fe55..d479907 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5634,6 +5634,8 @@ books/bookvolbib Using Latex as a Semantic Markup Format

books/bookvolbib Formal verification of numerical analysis programs

20170113.01.tpd.patch
books/bookvol13 pre/post conditions and Coq nat vs Axiom NNI

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

--
1.7.5.4