From d5f8cbf0e249e2f8ec17628df7b2847d76d896dc Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Wed, 5 Apr 2017 22:08:19 0400
Subject: [PATCH] books/bookvolbib add proof references
Goal: Proving Axiom Correct
\index{Coquand, Thierry}
\index{Dybjer, Peter}
\begin{chunk}{axiom.bib}
@article{Coqu96,
author = "Coquand, Thierry and Dybjer, Peter",
title = "Intuitionistic Model Constructions and Normalization Proofs",
journal = "Mathematical Structures in Computer Science",
volume = "7",
pages = "7594",
year = "1996",
link = "\url{http://www.cse.chalmers.se/~peterd/papers/Glueing.ps}",
abstract =
"The traditional notions of {\sl strong} and {\sl weak normalization}
refer to properties of a binary {\sl reduction relation}. In this
paper we explore an alternative approach to normalization, where we
bypass the reduction relation and instead focus on the {
{\sl normalization function}, that is, the function which maps a term into
its normal form.
Such a normalization function can be constructed by building an
appropriate model and a function ``quote'' which inverts the
interpretation function. The normalization function is then obtained
by composing the quote function with the interpretation function. We
also discuss how to gt a simple proof of the property that
constructors are onetoone, which usually is obtained as a corollary
of ChurchRosser and normalization in the traditional sense.
We illustrate this approach by showing how a glueing model (closely
related to the glueing construction used in category theory) gives
rise to a normalization algorithm for a combinatory formlation of
Godel System T. We then show how the method extends in a
straightforward way when we add cartesian products and disjoint unions
(full intuitionistic propositional logic under a CurryHoward
interpretation) and transfinite inductive types such as the Brouwer
ordinals.",
paper = "Coqu96.pdf"
}
\end{chunk}
\index{Pelayo, Alvaro}
\index{Warren, Michael A.}
\begin{chunk}{axiom.bib}
@article{Pela14,
author = "Pelayo, Alvaro and Warren, Michael A.",
title = "Homotopy Type Theory and Voevodsky's Univalent Foundations",
journal = "Bulletin of the American Mathematical Society",
volume = "51",
number = "4",
year = "2014",
pages = "597648",
link = "\url{https://arxiv.org/pdf/1210.5658.pdf}",
abstract =
"Recent discoveries have been made connecting abstract homotopy
theory and the field of type theory from logic and theoretical computer
science. This has given rise to a new field, which has been christened
{\sl homotopy type theory}. In this direction, Vladimir Voevodsky
observed that it is possible to model type theory using simpical sets
and that this model satisfies an additional property, called the
{\sl Univalence Axiom}, which has a number of striking consequences.
He has subsequently advocated a program, which he calls {\sl univalent
foundations}, of developing mathematics in the setting of type theory
with the Univalence Axiom and possibly other additional axioms motivated
by the simplical set model. Because type theory posses good computational
properties, this program can be carried out in a computer proof assistant.
In this paper we give an introduction to homotopy type theory in
Voevodsky's setting, paying attention to both theoretical and practical
issues. In particular, the paper serves as an introduction to both the
general ideas of homotopy type theory as well as to some of the concrete
details of Voevodsky's work using the wellknown proof assistant Coq.
The paper is written for a general audience of mathematicians with basic
knowledge of algebraic topology; the paper does not assume any
preliminary knowledge of type theory, logic, or computer science. Because
a defining characteristic of Voevodsky's program is that the Coq code has
fundamental mathematical content, and many of the mathematical concepts
which are efficiently captured in the code cannot be explained in
standard mathematical English without a length detour through type theory,
the later sections of this paper (beginning with Section 3) make use of
code; however, all notions are introduced from the beginning and in a
selfcontained fashion.",
paper = "Pela14.pdf"
}
\end{chunk}

books/bookvolbib.pamphlet  108 ++++++++++++++++++++++++++++++++++++
changelog  2 +
patch  90 ++++++++++++++++++++++++++++++++
src/axiomwebsite/patches.html  2 +
4 files changed, 190 insertions(+), 12 deletions()
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 6e7b027..3d3c827 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 558,7 +558,8 @@ paragraph for those unfamiliar with the terms.
\begin{chunk}{axiom.bib}
@misc{Fija17,
author = "Fijalkow, Nathanael",
 title = "Computing using the generators of a group: the SchreierSims' algorithm",
+ 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/}"
}
@@ 1566,7 +1567,8 @@ when shown in factored form.
\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.",
+ 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",
@@ 1759,11 +1761,12 @@ when shown in factored form.
\end{chunk}
\begin{chunk}{axiom.bib}
\cite{Schr17,
+@misc{Schr17,
author = "Wikipedia",
title = "SchreierSims algorithm",
year = "2017",
 link = "\url{https://en.wikipedia.org/wiki/Schreier%E2%80%93Sims_algorithm}",
+ link =
+ "\url{https://en.wikipedia.org/wiki/Schreier\%E2%80%93Sims\_algorithm}",
abstract =
"The SchreierSims algorithm is an algorithm in computational group
theory named after mathematicians Otto Schreier and Charles Sims. Once
@@ 6288,6 +6291,46 @@ Martin, U.
\end{chunk}
\index{Coquand, Thierry}
+\index{Dybjer, Peter}
+\begin{chunk}{axiom.bib}
+@article{Coqu96,
+ author = "Coquand, Thierry and Dybjer, Peter",
+ title = "Intuitionistic Model Constructions and Normalization Proofs",
+ journal = "Mathematical Structures in Computer Science",
+ volume = "7",
+ pages = "7594",
+ year = "1996",
+ link = "\url{http://www.cse.chalmers.se/~peterd/papers/Glueing.ps}",
+ abstract =
+ "The traditional notions of {\sl strong} and {\sl weak normalization}
+ refer to properties of a binary {\sl reduction relation}. In this
+ paper we explore an alternative approach to normalization, where we
+ bypass the reduction relation and instead focus on the
+ {\sl normalization function}, that is, the function which maps a term into
+ its normal form.
+
+ Such a normalization function can be constructed by building an
+ appropriate model and a function ``quote'' which inverts the
+ interpretation function. The normalization function is then obtained
+ by composing the quote function with the interpretation function. We
+ also discuss how to gt a simple proof of the property that
+ constructors are onetoone, which usually is obtained as a corollary
+ of ChurchRosser and normalization in the traditional sense.
+
+ We illustrate this approach by showing how a glueing model (closely
+ related to the glueing construction used in category theory) gives
+ rise to a normalization algorithm for a combinatory formlation of
+ Godel System T. We then show how the method extends in a
+ straightforward way when we add cartesian products and disjoint unions
+ (full intuitionistic propositional logic under a CurryHoward
+ interpretation) and transfinite inductive types such as the Brouwer
+ ordinals.",
+ paper = "Coqu96.pdf"
+}
+
+\end{chunk}
+
+\index{Coquand, Thierry}
\index{Huet, G\'erard}
\index{Paulin, Christine}
\begin{chunk}{axiom.bib}
@@ 6898,7 +6941,8 @@ Calculemus (2011) Springer
number = "5",
pages = "539567",
year = "2005",
 link = "\url{http://www.sciencedirect.com/science/article/pii/S0747717105000295}",
+ link =
+ "\url{http://www.sciencedirect.com/science/article/pii/S0747717105000295}",
abstract =
"We present hidden verification as a means to make the power of
computational logic available to users of computer algebra systems
@@ 6952,10 +6996,11 @@ Calculemus (2011) Springer
\begin{chunk}{axiom.bib}
@misc{Hard13,
author = "Hardin, David S. and McClurg, Jedidiah R. and Davis, Jennifer A.",
 title = "Creating Formally Verified Components for Layered Assurance with an LLVM to ACL2 Translator",
 link = "\url{http://www.jrmcclurg.com/papers/law_2013_paper.pdf}",
 abstract = "
 This paper describes an effort to create a library of formally
+ title = "Creating Formally Verified Components for Layered Assurance
+ with an LLVM to ACL2 Translator",
+ link = "\url{http://www.jrmcclurg.com/papers/law\_2013\_paper.pdf}",
+ abstract =
+ "This paper describes an effort to create a library of formally
verified software component models from code that have been compiled
using the LowLevel Virtual Machine (LLVM) intermediate form. The idea
is to build a translator from LLVM to the applicative subset of Common
@@ 7986,6 +8031,51 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
\end{chunk}
+\index{Pelayo, Alvaro}
+\index{Warren, Michael A.}
+\begin{chunk}{axiom.bib}
+@article{Pela14,
+ author = "Pelayo, Alvaro and Warren, Michael A.",
+ title = "Homotopy Type Theory and Voevodsky's Univalent Foundations",
+ journal = "Bulletin of the American Mathematical Society",
+ volume = "51",
+ number = "4",
+ year = "2014",
+ pages = "597648",
+ link = "\url{https://arxiv.org/pdf/1210.5658.pdf}",
+ abstract =
+ "Recent discoveries have been made connecting abstract homotopy
+ theory and the field of type theory from logic and theoretical computer
+ science. This has given rise to a new field, which has been christened
+ {\sl homotopy type theory}. In this direction, Vladimir Voevodsky
+ observed that it is possible to model type theory using simpical sets
+ and that this model satisfies an additional property, called the
+ {\sl Univalence Axiom}, which has a number of striking consequences.
+ He has subsequently advocated a program, which he calls {\sl univalent
+ foundations}, of developing mathematics in the setting of type theory
+ with the Univalence Axiom and possibly other additional axioms motivated
+ by the simplical set model. Because type theory posses good computational
+ properties, this program can be carried out in a computer proof assistant.
+ In this paper we give an introduction to homotopy type theory in
+ Voevodsky's setting, paying attention to both theoretical and practical
+ issues. In particular, the paper serves as an introduction to both the
+ general ideas of homotopy type theory as well as to some of the concrete
+ details of Voevodsky's work using the wellknown proof assistant Coq.
+ The paper is written for a general audience of mathematicians with basic
+ knowledge of algebraic topology; the paper does not assume any
+ preliminary knowledge of type theory, logic, or computer science. Because
+ a defining characteristic of Voevodsky's program is that the Coq code has
+ fundamental mathematical content, and many of the mathematical concepts
+ which are efficiently captured in the code cannot be explained in
+ standard mathematical English without a length detour through type theory,
+ the later sections of this paper (beginning with Section 3) make use of
+ code; however, all notions are introduced from the beginning and in a
+ selfcontained fashion.",
+ paper = "Pela14.pdf"
+}
+
+\end{chunk}
+
\index{Pfenning, Frank}
\index{PaulinMohring, Christine}
\begin{chunk}{axiom.bib}
diff git a/changelog b/changelog
index 53f3d00..8ef61b5 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20170405 tpd src/axiomwebsite/patches.html 20170405.01.tpd.patch
+20170405 tpd books/bookvolbib add proof references
20170404 tpd src/axiomwebsite/patches.html 20170404.01.tpd.patch
20170404 tpd books/bookvol10.3 Add unittest and help for PrimeField
20170403 tpd src/axiomwebsite/patches.html 20170403.01.tpd.patch
diff git a/patch b/patch
index bf6202a..6582ce6 100644
 a/patch
+++ b/patch
@@ 1,4 +1,88 @@
books/bookvol10.3 Add unittest and help for PrimeField
+books/bookvolbib add proof references
Goal: Axiom Literate Programming

+Goal: Proving Axiom Correct
+
+\index{Coquand, Thierry}
+\index{Dybjer, Peter}
+\begin{chunk}{axiom.bib}
+@article{Coqu96,
+ author = "Coquand, Thierry and Dybjer, Peter",
+ title = "Intuitionistic Model Constructions and Normalization Proofs",
+ journal = "Mathematical Structures in Computer Science",
+ volume = "7",
+ pages = "7594",
+ year = "1996",
+ link = "\url{http://www.cse.chalmers.se/~peterd/papers/Glueing.ps}",
+ abstract =
+ "The traditional notions of {\sl strong} and {\sl weak normalization}
+ refer to properties of a binary {\sl reduction relation}. In this
+ paper we explore an alternative approach to normalization, where we
+ bypass the reduction relation and instead focus on the {
+ {\sl normalization function}, that is, the function which maps a term into
+ its normal form.
+
+ Such a normalization function can be constructed by building an
+ appropriate model and a function ``quote'' which inverts the
+ interpretation function. The normalization function is then obtained
+ by composing the quote function with the interpretation function. We
+ also discuss how to gt a simple proof of the property that
+ constructors are onetoone, which usually is obtained as a corollary
+ of ChurchRosser and normalization in the traditional sense.
+
+ We illustrate this approach by showing how a glueing model (closely
+ related to the glueing construction used in category theory) gives
+ rise to a normalization algorithm for a combinatory formlation of
+ Godel System T. We then show how the method extends in a
+ straightforward way when we add cartesian products and disjoint unions
+ (full intuitionistic propositional logic under a CurryHoward
+ interpretation) and transfinite inductive types such as the Brouwer
+ ordinals.",
+ paper = "Coqu96.pdf"
+}
+
+\end{chunk}
+
+\index{Pelayo, Alvaro}
+\index{Warren, Michael A.}
+\begin{chunk}{axiom.bib}
+@article{Pela14,
+ author = "Pelayo, Alvaro and Warren, Michael A.",
+ title = "Homotopy Type Theory and Voevodsky's Univalent Foundations",
+ journal = "Bulletin of the American Mathematical Society",
+ volume = "51",
+ number = "4",
+ year = "2014",
+ pages = "597648",
+ link = "\url{https://arxiv.org/pdf/1210.5658.pdf}",
+ abstract =
+ "Recent discoveries have been made connecting abstract homotopy
+ theory and the field of type theory from logic and theoretical computer
+ science. This has given rise to a new field, which has been christened
+ {\sl homotopy type theory}. In this direction, Vladimir Voevodsky
+ observed that it is possible to model type theory using simpical sets
+ and that this model satisfies an additional property, called the
+ {\sl Univalence Axiom}, which has a number of striking consequences.
+ He has subsequently advocated a program, which he calls {\sl univalent
+ foundations}, of developing mathematics in the setting of type theory
+ with the Univalence Axiom and possibly other additional axioms motivated
+ by the simplical set model. Because type theory posses good computational
+ properties, this program can be carried out in a computer proof assistant.
+ In this paper we give an introduction to homotopy type theory in
+ Voevodsky's setting, paying attention to both theoretical and practical
+ issues. In particular, the paper serves as an introduction to both the
+ general ideas of homotopy type theory as well as to some of the concrete
+ details of Voevodsky's work using the wellknown proof assistant Coq.
+ The paper is written for a general audience of mathematicians with basic
+ knowledge of algebraic topology; the paper does not assume any
+ preliminary knowledge of type theory, logic, or computer science. Because
+ a defining characteristic of Voevodsky's program is that the Coq code has
+ fundamental mathematical content, and many of the mathematical concepts
+ which are efficiently captured in the code cannot be explained in
+ standard mathematical English without a length detour through type theory,
+ the later sections of this paper (beginning with Section 3) make use of
+ code; however, all notions are introduced from the beginning and in a
+ selfcontained fashion.",
+ paper = "Pela14.pdf"
+}
+
+\end{chunk}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 9035c78..5722179 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5682,6 +5682,8 @@ books/bookvolbib Martin Baker's PERMGRP documentation
books/bookvolbib add proof references
20170404.01.tpd.patch
books/bookvol10.3 Add unittest and help for PrimeField
+20170405.01.tpd.patch
+books/bookvolbib add proof references

1.7.5.4