From d5b8ed2cd29277e1de4ed2f4f038e1347a7d795c Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Thu, 12 Jan 2017 18:14:16 0500
Subject: [PATCH] books/bookvolbib Formal verification of numerical analysis
programs
Goal: Proving Axiom Correct
\index{Boldo, Sylvie}
\begin{chunk}{axiom.bib}
@misc{Bold16,
author = "Boldo, Sylvie",
title = "Formal verification of numerical analysis programs",
year = "2016",
link = "\url{https://www.youtube.com/watch?v=7MDwpwD6Ts4}"
}
\end{chunk}

books/bookvolbib.pamphlet  11 ++++++++++
changelog  2 +
patch  43 ++++++++
src/axiomwebsite/patches.html  2 +
4 files changed, 24 insertions(+), 34 deletions()
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index d201931..44c992e 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 5586,6 +5586,17 @@ Martin, U.
\end{chunk}
+\index{Boldo, Sylvie}
+\begin{chunk}{axiom.bib}
+@misc{Bold16,
+ author = "Boldo, Sylvie",
+ title = "Formal verification of numerical analysis programs",
+ year = "2016",
+ link = "\url{https://www.youtube.com/watch?v=7MDwpwD6Ts4}"
+}
+
+\end{chunk}
+
\index{Boulm\'e, S.}
\index{Hardin, T.}
\index{Rioboo, Renaud}
diff git a/changelog b/changelog
index 8f02e6d..49b0883 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20170112 tpd src/axiomwebsite/patches.html 20170112.03.tpd.patch
+20170112 tpd books/bookvolbib Formal verif. of numerical analysis programs
20170112 tpd src/axiomwebsite/patches.html 20170112.02.tpd.patch
20170112 tpd books/bookvolbib Using Latex as a Semantic Markup Format
20170112 tpd src/axiomwebsite/patches.html 20170112.01.tpd.patch
diff git a/patch b/patch
index d368c32..4e8efba 100644
 a/patch
+++ b/patch
@@ 1,41 +1,16 @@
books/bookvolbib Using Latex as a Semantic Markup Format
+books/bookvolbib Formal verification of numerical analysis programs
Goal: Literate software
+Goal: Proving Axiom Correct
\index{Kohlhase, Michael}
+\index{Boldo, Sylvie}
\begin{chunk}{axiom.bib}
@misc{Kohl08,
 author = "Kohlhase, Michael",
 title = "Using Latex as a Semantic Markup Format",
 year = "2008",
 link = "\url{https://kwarc.info/kohlhase/papers/mcs08stex.pdf}",
 abstract =
 "One of the great problems of Mathematical Knowledge Management (MKM)
 systems is to obtain access to a sufficiently large corpus of
 mathematical knowledge to allow the management / search / naviation
 techniques developed by the community to display their strength. Such
 systems usually expect the mathematical knowledge they operate on in
 the form of semantically enhanced documents, but mathematicians and
 publishers in Mathematics have heavily invested into the Tex/Latex
 format and workflow.

 We analyze the current practice of semisemantic markup in Latex
 documents and extend it by a markup infrastructure that allows to
 embed semantic annotations into latex documents without changing their
 visual appearance. This collection of tex macro packages is called
 stex (semantic tex) as it allows to markup latex documents
 semantically without leaving the timetried tex/latex workflow,
 essentially turning latex into an MKM format. At the heart of stex is
 a definition mechanism for semantic macros for mathematical objects
 and a nonstandard scoping construct for them, which is oriented at
 the semantic dependency relation rather than the document structure.

 We evaulate the stex macro collection on a large case study: the
 course materials of a twosemester course in Computer Science was
 annotated semantically and coverted to the OMDOC MKM format by Bruce
 Miller's LatexML system.",
 paper = "Kohl08.pdf"
+@misc{Bold16,
+ author = "Boldo, Sylvie",
+ title = "Formal verification of numerical analysis programs",
+ year = "2016",
+ link = "\url{https://www.youtube.com/watch?v=7MDwpwD6Ts4}"
}
\end{chunk}
+
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 0cdf525..30aad89 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5630,6 +5630,8 @@ readme add Wolfgang Brehm to credit list
books/bookvolbib References on Program Proofs
20170112.02.tpd.patch
books/bookvolbib Using Latex as a Semantic Markup Format
+20170112.03.tpd.patch
+Formal verification of numerical analysis programs

1.7.5.4