From 04f4ed6d8efe892ec2f7d4c8a395ce801e02bb27 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Mon, 3 Apr 2017 23:05:27 0400
Subject: [PATCH] books/bookvolbib add proof references
Goal: Proving Axiom Correct
\index{Platzer, Andre}
\index{Quesel, JanDavid}
\index{Rummer, Philipp}
\begin{chunk}{axiom.bib}
@article{Plat09,
author = "Platzer, Andre and Quesel, JanDavid and Rummer, Philipp",
title = "Real World Verification",
journal = "LNCS",
volume = "5663",
year = "2009",
pages = "495501",
link = "\url{http://www.cs.cmu.edu/~aplatzer/pub/rwv.pdf}",
abstract =
"Scalable handling of real arithmetic is a crucial part of the
verification of hybrid systems, mathematical algorithms, and mixed
analog/digital circuits. Despite substantial advances in verification
technology, complexity issues with classical decision procedures are
still a major obstacle for formal verification of realworld
applications, e.g., in automotive and avionic industries. To identify
strengths and weaknesses, we examine state of the art symbolic
techniques and implementations for the universal fragment of
realclosed fields: approaches based on quantifier elimination,
Groebner Bases, and semidefinite programming for the
Positivstellensatz. Within a uniform context of the verification tool
KeYmaera, we compare these approaches qualitatively and quantitatively
on verification benchmarks from hybrid systems, textbook algorithms,
and on geometric problems. Finally, we introduce a new decision
procedure combining Groebner Bases and semidefinite programming for
the real Nullstellensatz that outperforms the individual approaches on
an interesting set of problems.",
paper = "Plat09,pdf"
}
\end{chunk}
\index{Krebbers, Robbert Jan}
\index{Wiedijk, Freek}
\begin{chunk}{axiom.bib}
@misc{Kreb15a,
author = "Krebbers, Robbert and Wiedijk, Freek",
title = "A Typed C11 Semantics for Interactive Theorem Proving",
year = "2015",
link = "\url{http://robbertkrebbers.nl/research/articles/interpreter.pdf}",
abstract =
"We present a semantics of a significant fragment of the C programming
language as described by the C11 standard. It consists of a small step
semantics of a core language, which uses a structured memory model to
capture subtleties of C11, such as strictaliasing restrictions
related to unions, that have not yet been addressed by others. The
semantics of actual C programs is defined by translation into this
core language. We have an explicit type system for the core language,
and prove type preservation and progress, as well as type correctness
of the translation.
Due to unspecified order of evaluation, our operational semantics is
nondeterministic. To explore all defined and undefined behaviors, we
present an executable semantics that computes a stream of finite sets
of reachable states. It is proved sound and complete with respect to
the operational semantics.
Both the translation into the core language and the executable
semantics are defined as Coq programs. Extraction to OCaml is used to
obtain a C interpreter to run and test the semantics on actual C
programs. All proofs are fully formalized in Coq.",
paper = "Kreb15a.pdf"
}
\end{chunk}
\index{Krebbers, Robbert Jan}
\begin{chunk}{axiom.bib}
@misc{Kreb17,
author = "Krebbers, Robbert Jan",
title = {The CH$_2$O formalization of ISO C11},
year = "2017",
link = "\url{http://robbertkrebbers.nl/research/ch2o/}"
}
\end{chunk}
\index{Liskov, Barbara}
\index{Synder, Alan}
\index{Atkinson, Russell}
\index{Schaffert, Craig}
\begin{chunk}{axiom.bib}
@article{Lisk77,
author = "Liskov, Barbara and Synder, Alan and Atkinson, Russell and
Schaffert, Craig",
title = "Abstraction Mechanisms in CLU",
journal = "CACM",
volume = "20",
number = "8",
year = "1977",
link = "\url{https://www.cs.virginia.edu/~weimer/615/reading/liskovcluabstraction.pdf}",
abstract =
"CLU is a new programming language designed to support the use of
abstractions in program construction. Work in programming methodology
has led to the realization that three kinds of abstractions 
procedural, control, and especially data abstractions  are useful in
the programming process. Of these, only the procedural abstraction is
supported well by conventional languages, through the procedure or
subroutine. CLU provides, in addition to procedures, novel linguistic
mechanisms that support the use of data and control abstractions. This
paper provides an introduction to the abstraction mechanisms of
CLU. By means of programming examples, the utility of the three kinds
of abstractions in program construction is illustrated, and it is
shown how CLU programs may be written to use and implement
abstractions. The CLU library, which permits incremental program
development with complete type checking performed at compile time, is
also discussed.",
paper = "Lisk77.pdf"
}
\end{chunk}

books/bookvolbib.pamphlet  117 +++++++++++++++++++++++
changelog  2 +
patch  199 +++++++++++++
src/axiomwebsite/patches.html  2 +
4 files changed, 186 insertions(+), 134 deletions()
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 74a130a..6e7b027 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 1723,6 +1723,41 @@ when shown in factored form.
\end{chunk}
+\index{Platzer, Andre}
+\index{Quesel, JanDavid}
+\index{Rummer, Philipp}
+\begin{chunk}{axiom.bib}
+@article{Plat09,
+ author = "Platzer, Andre and Quesel, JanDavid and Rummer, Philipp",
+ title = "Real World Verification",
+ journal = "LNCS",
+ volume = "5663",
+ year = "2009",
+ pages = "495501",
+ link = "\url{http://www.cs.cmu.edu/~aplatzer/pub/rwv.pdf}",
+ abstract =
+ "Scalable handling of real arithmetic is a crucial part of the
+ verification of hybrid systems, mathematical algorithms, and mixed
+ analog/digital circuits. Despite substantial advances in verification
+ technology, complexity issues with classical decision procedures are
+ still a major obstacle for formal verification of realworld
+ applications, e.g., in automotive and avionic industries. To identify
+ strengths and weaknesses, we examine state of the art symbolic
+ techniques and implementations for the universal fragment of
+ realclosed fields: approaches based on quantifier elimination,
+ Groebner Bases, and semidefinite programming for the
+ Positivstellensatz. Within a uniform context of the verification tool
+ KeYmaera, we compare these approaches qualitatively and quantitatively
+ on verification benchmarks from hybrid systems, textbook algorithms,
+ and on geometric problems. Finally, we introduce a new decision
+ procedure combining Groebner Bases and semidefinite programming for
+ the real Nullstellensatz that outperforms the individual approaches on
+ an interesting set of problems.",
+ paper = "Plat09,pdf"
+}
+
+\end{chunk}
+
\begin{chunk}{axiom.bib}
\cite{Schr17,
author = "Wikipedia",
@@ 7215,6 +7250,51 @@ Calculemus (2011) Springer
\end{chunk}
+\index{Krebbers, Robbert Jan}
+\index{Wiedijk, Freek}
+\begin{chunk}{axiom.bib}
+@misc{Kreb15a,
+ author = "Krebbers, Robbert and Wiedijk, Freek",
+ title = "A Typed C11 Semantics for Interactive Theorem Proving",
+ year = "2015",
+ link = "\url{http://robbertkrebbers.nl/research/articles/interpreter.pdf}",
+ abstract =
+ "We present a semantics of a significant fragment of the C programming
+ language as described by the C11 standard. It consists of a small step
+ semantics of a core language, which uses a structured memory model to
+ capture subtleties of C11, such as strictaliasing restrictions
+ related to unions, that have not yet been addressed by others. The
+ semantics of actual C programs is defined by translation into this
+ core language. We have an explicit type system for the core language,
+ and prove type preservation and progress, as well as type correctness
+ of the translation.
+
+ Due to unspecified order of evaluation, our operational semantics is
+ nondeterministic. To explore all defined and undefined behaviors, we
+ present an executable semantics that computes a stream of finite sets
+ of reachable states. It is proved sound and complete with respect to
+ the operational semantics.
+
+ Both the translation into the core language and the executable
+ semantics are defined as Coq programs. Extraction to OCaml is used to
+ obtain a C interpreter to run and test the semantics on actual C
+ programs. All proofs are fully formalized in Coq.",
+ paper = "Kreb15a.pdf"
+}
+
+\end{chunk}
+
+\index{Krebbers, Robbert Jan}
+\begin{chunk}{axiom.bib}
+@misc{Kreb17,
+ author = "Krebbers, Robbert Jan",
+ title = {The CH$_2$O formalization of ISO C11},
+ year = "2017",
+ link = "\url{http://robbertkrebbers.nl/research/ch2o/}"
+}
+
+\end{chunk}
+
\index{Kuper, Jan}
\index{Wester, Rinse}
\begin{chunk}{axiom.bib}
@@ 8339,7 +8419,7 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\end{chunk}
\begin{chunk}{axiom.bib}
@misc{Stac17,
+@misc{Stac17a,
author = "cstheory.stackexchange.com",
title = "Why does Coq have Prop?",
link = "\url{http://cstheory.stackexchange.com/questions/21836/whydoescoqhaveprop/21878\#21878}",
@@ 37759,6 +37839,41 @@ AddisonWesley (March 1979) ISBN 0201144611
\end{chunk}
\index{Liskov, Barbara}
+\index{Synder, Alan}
+\index{Atkinson, Russell}
+\index{Schaffert, Craig}
+\begin{chunk}{axiom.bib}
+@article{Lisk77,
+ author = "Liskov, Barbara and Synder, Alan and Atkinson, Russell and
+ Schaffert, Craig",
+ title = "Abstraction Mechanisms in CLU",
+ journal = "CACM",
+ volume = "20",
+ number = "8",
+ year = "1977",
+ link = "\url{https://www.cs.virginia.edu/~weimer/615/reading/liskovcluabstraction.pdf}",
+ abstract =
+ "CLU is a new programming language designed to support the use of
+ abstractions in program construction. Work in programming methodology
+ has led to the realization that three kinds of abstractions 
+ procedural, control, and especially data abstractions  are useful in
+ the programming process. Of these, only the procedural abstraction is
+ supported well by conventional languages, through the procedure or
+ subroutine. CLU provides, in addition to procedures, novel linguistic
+ mechanisms that support the use of data and control abstractions. This
+ paper provides an introduction to the abstraction mechanisms of
+ CLU. By means of programming examples, the utility of the three kinds
+ of abstractions in program construction is illustrated, and it is
+ shown how CLU programs may be written to use and implement
+ abstractions. The CLU library, which permits incremental program
+ development with complete type checking performed at compile time, is
+ also discussed.",
+ paper = "Lisk77.pdf"
+}
+
+\end{chunk}
+
+\index{Liskov, Barbara}
\index{Atkinson, Russ}
\index{Bloom, Toby}
\index{Moss, Eliot}
diff git a/changelog b/changelog
index a7eedc8..e88c863 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20170403 tpd src/axiomwebsite/patches.html 20170403.01.tpd.patch
+20170403 tpd books/bookvolbib add proof references
20170325 myb src/axiomwebsite/patches.html 20170325.01.myb.patch
20170325 myb books/bookvol10.3 Martin Baker's PERMGRP documentation
20170325 myb books/bookvolbib Martin Baker's PERMGRP documentation
diff git a/patch b/patch
index 977fba0..da4f8a0 100644
 a/patch
+++ b/patch
@@ 1,154 +1,88 @@
books/bookvolbib Martin Baker's PERMGRP documentation
+books/bookvolbib add proof references
Goal: Literate Programming

\index{Baker, Martin}
\begin{chunk}{axiom.bib}
@misc{Bake17,
 author = "Baker, Martin",
 title = "Finite Group Implementation",
 link = "\url{http://www.euclideanspace.com/prog/scratchpad/mycode/discrete/finiteGroup/}",
 year = "2017"
}

\end{chunk}

\index{Baker, Martin}
+Goal: Proving Axiom Correct
+
+\index{Platzer, Andre}
+\index{Quesel, JanDavid}
+\index{Rummer, Philipp}
\begin{chunk}{axiom.bib}
@misc{Bake16b,
 author = "Baker, Martin",
 title = "add coerce from PermutationGroup to GroupPresentation",
 link = "\url{https://groups.google.com/forum/?hl=en\#!topic/fricasdevel/EtLwgd2dWNU}",
 year = "2016"
}

\end{chunk}

\index{Cannon, John J.}
\index{Dimino, Lucien A.}
\index{Havas, George}
\index{Watson, Jane M.}
\begin{chunk}{axiom.bib}
@article{Cann73,
 author = "Cannon, John J. and Dimino, Lucien A. and Havas, George and Watson, Jane M.",
 title = "Implementation and Analysis of the ToddCoxeter Algorithm",
 year = "1973",
 journal = "Mathematics of Computation",
 volume = "27",
 number = "123",
 pages = "463490",
+@article{Plat09,
+ author = "Platzer, Andre and Quesel, JanDavid and Rummer, Philipp",
+ title = "Real World Verification",
+ journal = "LNCS",
+ volume = "5663",
+ year = "2009",
+ pages = "495501",
+ link = "\url{http://www.cs.cmu.edu/~aplatzer/pub/rwv.pdf}",
abstract =
 "A recent form of the ToddCoxeter algorithm, known as the lookahead
 algorithm, is described. The time and space requirements for this
 algorithm are shown experimentally to be usually either equivalent or
 superior to the Felsch and HaselgroveLeechTrotter algorithms. Some
 finding from an experimental study of the behaviour of ToddCoxeter
 programs in a variety of situations is given.",
 paper = "Cann73.pdf"
}
+ "Scalable handling of real arithmetic is a crucial part of the
+ verification of hybrid systems, mathematical algorithms, and mixed
+ analog/digital circuits. Despite substantial advances in verification
+ technology, complexity issues with classical decision procedures are
+ still a major obstacle for formal verification of realworld
+ applications, e.g., in automotive and avionic industries. To identify
+ strengths and weaknesses, we examine state of the art symbolic
+ techniques and implementations for the universal fragment of
+ realclosed fields: approaches based on quantifier elimination,
+ Groebner Bases, and semidefinite programming for the
+ Positivstellensatz. Within a uniform context of the verification tool
+ KeYmaera, we compare these approaches qualitatively and quantitatively
+ on verification benchmarks from hybrid systems, textbook algorithms,
+ and on geometric problems. Finally, we introduce a new decision
+ procedure combining Groebner Bases and semidefinite programming for
+ the real Nullstellensatz that outperforms the individual approaches on
+ an interesting set of problems.",
+ paper = "Plat09,pdf"
+}
\end{chunk}
+\index{Krebbers, Robbert Jan}
+\index{Wiedijk, Freek}
\begin{chunk}{axiom.bib}
\cite{Schr17,
 author = "Wikipedia",
 title = "SchreierSims algorithm",
 year = "2017",
 link = "\url{https://en.wikipedia.org/wiki/Schreier%E2%80%93Sims_algorithm}",
+@misc{Kreb15a,
+ author = "Krebbers, Robbert and Wiedijk, Freek",
+ title = "A Typed C11 Semantics for Interactive Theorem Proving",
+ year = "2015",
+ link = "\url{http://robbertkrebbers.nl/research/articles/interpreter.pdf}",
abstract =
 "The SchreierSims algorithm is an algorithm in computational group
 theory named after mathematicians Otto Schreier and Charles Sims. Once
 performed, it allows a linear time computation of the order of a
 finite permuation group, group membership test (is a given permutation
 contained in a group?), and many other tasks. The algorith was
 introduced by Sims in 1970, based on Schreier's subgroup lemma. The
 timing was subsequently improved by Donald Knuth in 1991. Later, an
 even faster randomized version of the algorithm was developed.
+ "We present a semantics of a significant fragment of the C programming
+ language as described by the C11 standard. It consists of a small step
+ semantics of a core language, which uses a structured memory model to
+ capture subtleties of C11, such as strictaliasing restrictions
+ related to unions, that have not yet been addressed by others. The
+ semantics of actual C programs is defined by translation into this
+ core language. We have an explicit type system for the core language,
+ and prove type preservation and progress, as well as type correctness
+ of the translation.
 The algorithm is an efficient method of computing a base and strong
 generating set (BSGS) of a permutation group. In particular, an SGS
 determines the order of a group and makes it easy to test membership
 in the group. Since the SGS is critical for many algorithms in
 computational group theory, computer algebra systems typically rely on
 the SchreierSims algorithm for efficient calculations in groups"
}

\end{chunk}

\begin{chunk}{axiom.bib}
@misc{Wiki17a,
 author = "Wikipedia",
 title = "Group Action",
 year = "2017",
 link = "\url{https://en.wikipedia.org/wiki/Group\_action}",
 abstract =
 "In mathematics, an action of a group is a way of interpreting the
 elements of the group as ``acting'' on some space in a way that
 preserves the structure of that space. Common examples of spaces that
 groups act on are sets, vector spaces, and topological spaces. Actions
 of groups on vector stacces are called representations of the group."
}

\end{chunk}

\begin{chunk}{axiom.bib}
@misc{Wiki17b,
 author = "Wikipedia",
 title = "Strong generating set",
 year = "2017",
 link = "\url{http://en.wikipedia.org/wiki/Strong\_generating\_set}",
 abstract =
 "In abstract algebra, especially in the area of group theory, a strong
 generating set of a permutation group is a generating set that clearly
 exhibits the permutation structure as described by a stabilizer
 chain. A stabilizer chain is a sequence of subgroups, each containing
 the next and each stabilizing one more point."
}

\end{chunk}

\index{Fijalkow, Nathanael}
\begin{chunk}{axiom.bib}
@misc{Fija17,
 author = "Fijalkow, Nathanael",
 title = "Computing using the generators of a group: the SchreierSims' algorithm",
 year = "2017",
 link = "\url{https://www.cs.ox.ac.uk/blogs/nathanaelfijalkow/2016/01/27/computingusingthegeneratorsofagroup/}"
}

\end{chunk}

\index{Gowers, Timothy}
\begin{chunk}{axiom.bib}
@misc{Gowe17,
 author = "Gowers, Timothy",
 title = "Group actions II: the orbitstabilizer theorem",
 year = "2017",
 link = "\url{https://gowers.wordpress.com/2011/11/09/groupactionsiitheorbitstabilizertheorem/}"
+ Due to unspecified order of evaluation, our operational semantics is
+ nondeterministic. To explore all defined and undefined behaviors, we
+ present an executable semantics that computes a stream of finite sets
+ of reachable states. It is proved sound and complete with respect to
+ the operational semantics.
+
+ Both the translation into the core language and the executable
+ semantics are defined as Coq programs. Extraction to OCaml is used to
+ obtain a C interpreter to run and test the semantics on actual C
+ programs. All proofs are fully formalized in Coq.",
+ paper = "Kreb15a.pdf"
}
\end{chunk}
+\index{Krebbers, Robbert Jan}
\begin{chunk}{axiom.bib}
@misc{Stac17,
 author = "StackExchange",
 title = "How do Gap generate the elements in permutation groups",
+@misc{Kreb17,
+ author = "Krebbers, Robbert Jan",
+ title = {The CH$_2$O formalization of ISO C11},
year = "2017",
 link = "\url{http://math.stackexchange.com/questions/1705277/howdogapgeneratetheelementsinpermutationgroups}"
}

\end{chunk}
\index{Judson, Thomas W.}
\begin{chunk}{axiom.bib}
@misc{Juds16,
 author = "Judson, Thomas W.",
 title = "Abstract Algebra: Theory and Applications",
 link = "\url{http://abstract.ups.edu/download/aata20160809sage7.3.pdf}",
 year = "2016"
+ link = "\url{http://robbertkrebbers.nl/research/ch2o/}"
}
\end{chunk}
+
\index{Liskov, Barbara}
\index{Synder, Alan}
\index{Atkinson, Russell}
@@ 183,4 +117,3 @@ Goal: Literate Programming
}
\end{chunk}

diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index d48897f..1399d4c 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5678,6 +5678,8 @@ books/Makefile add tanglec to $AXIOM/bin
books/bookvolbib Homotopy Type Theory reference
20170325.01.myb.patch
books/bookvolbib Martin Baker's PERMGRP documentation
+20170403.01.tpd.patch
+books/bookvolbib add proof references

1.7.5.4