From 9ec132779ea63b62a2bbc15900b08a5711c5f05d Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Thu, 12 Jan 2017 16:07:18 0500
Subject: [PATCH] books/bookvolbib Using Latex as a Semantic Markup Format
Goal: Literate software
\index{Kohlhase, Michael}
\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"
}
\end{chunk}

books/bookvolbib.pamphlet  37 ++++++++
changelog  2 +
patch  201 +++++++
src/axiomwebsite/patches.html  2 +
4 files changed, 74 insertions(+), 168 deletions()
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 324de65..d201931 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 14314,6 +14314,43 @@ J. Symbolic Computation 5, 237259 (1988)
\end{chunk}
+\index{Kohlhase, Michael}
+\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"
+}
+
+\end{chunk}
+
\index{Vakil, Ravi}
\begin{chunk}{axiom.bib}
@misc{Vaki98,
diff git a/changelog b/changelog
index d753837..8f02e6d 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+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
20170112 tpd books/bookvolbib References on Program Proofs
20170109 tpd src/axiomwebsite/patches.html 20170109.01.tpd.patch
diff git a/patch b/patch
index 0e1d038..d368c32 100644
 a/patch
+++ b/patch
@@ 1,176 +1,41 @@
books/bookvolbib References on Program Proofs
+books/bookvolbib Using Latex as a Semantic Markup Format
Goal: Proving Axiom Correct
+Goal: Literate software
\index{Bauer, Andrej}
+\index{Kohlhase, Michael}
\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}",
+@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 =
 "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"
+ "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"
}
\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 = "3540208542",
 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 zerofault software."
}

\end{chunk}

\index{Huet, G\'erard}
\index{Kahn, Gilles}
\index{PaulinMohring, Christine}
\begin{chunk}{axiom.bib}
@misc{Heut16,
 author = {Huet, G\'erard and Kahn, Gilles and PaulinMohring, 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 coinductive 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, coinduction, etc.) Each technique is illustrated
 through an executable and selfcontained {\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 higherorder unification, adhoc 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/ReferenceManual.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=BSyrpiYBMo}",
 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
 coarsergrained 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 Clike language with an ``array of
 bytes'' memory model, higherlevel more C++like languages with ``array
 of abstract data types'' memory models, a domainspecific 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 PitClaudel, and Peng Wang."

}

\end{chunk}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index f1e9e07..0cdf525 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5628,6 +5628,8 @@ books/axiom.bst add link, isbn to biblio entries
readme add Wolfgang Brehm to credit list
20170112.01.tpd.patch
books/bookvolbib References on Program Proofs
+20170112.02.tpd.patch
+books/bookvolbib Using Latex as a Semantic Markup Format

1.7.5.4