From f871dffc48c86caf763b442edd73a0aa9db2f4c6 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Tue, 9 Jan 2018 00:31:04 0500
Subject: [PATCH] books/bookvolbib add references
Goal: Proving Axiom Correct
\index{Scott, Dana}
\begin{chunk}{axiom.bib}
@article{Scot76,
author = "Scott, Dana",
title = {{Data Types as Lattices}},
journal = "SIAM J. Comput.",
volume = "5",
year = "1976",
pages = "522587",
abstract =
"The meaning of many kinds of expressions in programming languages can
be taken as elements of certain spaces of 'partial' objects. In this
report these spaces are modeled in one univeral domain $P_\omega$, the
set of all subsets of the integers. This domain renders the connection
of this semantic theory with the ordinary theor of number theoretic
(especailly general recursive) functions clear and straightforward.",
paper = "Scot76.pdf"
}
\end{chunk}
\index{Bishop, Errett}
\begin{chunk}{axiom.bib}
@book{Bish12,
author = "Bishop, Errett",
title = {{Foundations of Constructive Analysis}},
publisher = "ISHI Press",
year = "2012",
isbn = "9784871877145"
}
\end{chunk}
\index{Asperti, Andrea}
\index{Ricciotti, Wilmer}
\index{Coer, Claudio Sacerdoti}
\index{Tassi, Enrico}
\begin{chunk}{axiom.bib}
@article{Aspe09,
author = "Asperti, Andrea and Ricciotti, Wilmer and Coer, Claudio
Sacerdoti and Tassi, Enrico",
title = {{A Compact Kernel for the Calculus of Inductive Constructions}},
journal = "Sadhana",
volume = "34",
number = "1",
year = "2009",
pages = "71104",
abstract =
"The paper describes the new kernel for the Calculus of Inductive
Constructions (CIC) implemented inside the Matita Interactive
Theorem Prover. The design of the new kernel has been completely
revisited since the first release, resulting in a remarkably compact
implementation of about 2300 lines of OCaml code. The work is meant
for people interested in implementation aspects of Interactive
Provers, and is not self contained . In particular, it requires good
acquaintance with Type Theory and functional programming
languages.",
paper = "Aspe09.pdf"
}
\end{chunk}
\index{Asperti, Andrea}
\index{Ricciotti, Wilmer}
\index{Coer, Claudio Sacerdoti}
\index{Tassi, Enrico}
\begin{chunk}{axiom.bib}
@inproceedings{Aspe11,
author = "Asperti, Andrea and Ricciotti, Wilmer and Coer, Claudio
Sacerdoti and Tassi, Enrico",
title = {{The Matita Interactive Theorem Prover}},
booktitle = "CADE23 Automated Deduction",
year = "2011",
pages = "6469",
abstract =
"Matita is an interactive theorem prover being developed by the Helm
team at the University of Bologna. Its stable version 0.5.x may be
downloaded at http://matita.cs.unibo.it . The tool originated in the
European project MoWGLI as a set of XMLbased tools aimed to provide a
mathematicianfriendly webinterface to repositories of formal
mathematical knoweldge, supporting advanced contentbased
functionalities for querying, searching and browsing the library. It
has since then evolved into a fully fledged ITP, specifically designed
as a lightweight, but competitive system, particularly suited for the
assessment of innovative ideas, both at foundational and logical
level. In this paper, we give an account of the whole system, its
peculiarities and its main applications.",
paper = "Aspe11.pdf",
}
\end{chunk}
\index{Spitters, Bas}
\index{van der Weegen, Eelis}
\begin{chunk}{axiom.bib}
@article{Spit11,
author = "Spitters, Bas and van der Weegen, Eelis",
title = {{Type Classes for Mathematics in Type Theory}},
journal = "Math. Struct. Comput. Sci.",
volume = "21",
number = "4",
pages = "795825",
year = "2011",
abstract =
"The introduction of firstclass type classes in the Coq system calls
for reexamination of the basic interfaces used for mathematical
formalization in type theory. We present a new set of type classes for
mathematics and take full advantage of their unique features to make
practical a particularly flexible approach formerly thought
infeasible. Thus, we address both traditional proof engineering
challenges as well as new ones resulting from our ambition to build
upon this development a library of constructive analysis in which
abstraction penalties inhibiting efficient computation are reduced to
a minimum.
The base of our development consists of type classes representing a
standard algebraic hierarchy, as well as portions of category theory
and universal algebra. On this foundation we build a set of
mathematically sound abstract interfaces for different kinds of
numbers, succinctly expressed using categorical language and universal
algebra constructions. Strategic use of type classes lets us support
these highlevel theoryfriendly definitions while still enabling
efficient implementations unhindered by gratuitous indirection,
conversion or projection.
Algebra thrives on the interplay between syntax and semantics. The
Prologlike abilities of type class instance resolution allow us to
conveniently define a quote function, thus facilitating the use of
reflective techniques.",
paper = "Spit11.pdf"
}
\end{chunk}
\index{Coen, Claudio Sacerdoti}
\begin{chunk}{axiom.bib}
@article{Coen10,
author = "Coen, Claudio Sacerdoti",
title = {{Declarative Representation of Proof Terms}},
journal = "J. Automated Reasoning",
volume = "44",
number = "12",
pages = "2552",
year = "2010",
abstract =
"We present a declarative language inspired by the pseudonatural
language previously used in Matita for the explanation of proof
terms. We show how to compile the language to proof terms and how to
automatically generate declarative scripts from proof terms. Then we
investigate the relationship between the two translations, identifying
the amount of proof structure preserved by compilation and
regeneration of declarative scripts.",
paper = "Coen10.pdf"
}
\end{chunk}
\index{Luo, Zhaohui}
\begin{chunk}{axiom.bib}
@inproceedings{Luox96,
author = "Luo, Zhaohui",
title = {{Coercive Subtyping in Type Theory}},
booktitle = "CSL'96 Euro. Ass. for Comput. Sci. Logic",
year = "1996",
abstract =
"We propose and study coercive subtyping, a formal extension with
subtyping of dependent type theories such as MartinLof's type theory
[NPS90] and the type theory UTT [Luo94]. In this approach, subtyping
with specied implicit coercions is treated as a feature at the level
of the logical framework; in particular, subsumption and coercion are
combined in such a way that the meaning of an object being in a
supertype is given by coercive definition rules for the definitional
equality. It is shown that this provides a conceptually simple and
uniform framework to understand subtyping and coercion relations in
type theories with sophisticated type structures such as inductive
types and universes. The use of coercive subtyping in formal
development and in reasoning about subsets of objects is discussed in
the context of computerassisted formal reasoning.",
paper = "Luox96.pdf"
}
\end{chunk}
\index{Luo, Zhaohui}
\begin{chunk}{axiom.bib}
@misc{Luox11,
author = "Luo, Zhaohui",
title = {{TypeTheoretical Semantics with Coercive Subtyping}},
year = "2011",
comment = "Lecture Notes 2011 ESSLLI Summer School, Ljubljana,
Slovenia",
paper = "Luox11.pdf"
}
\end{chunk}
\index{Bailey, Anthony}
\begin{chunk}{axiom.bib}
@phdthesis{Bail98,
author = "Bailey, Anthony",
title = {{The MachineChecked Literate Formalisation of Algebra
in Type Theory}},
school = "University of Manchester",
year = "1998",
link =
"\url{http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.464.1249&rep=rep1&type=pdf}",
abstract =
"I present a largescale formalisation within a type theory of a
proof of a result from abstract algebra. The formalisation body
consists of files that are machinechecked to ensure their
correctness, and also processed to produce a report on the proof that
is humanreadable. The resulting presentation is intended to approach
being a standard informal account of some mathematics. In addition
to presenting this proof, the thesis also identifies and examines
problems in reconciling the formal nature of the development with the
wish for it to be easy to read. It presents some tools and methodologies
for solving these problems, and discusses the advantages and
disadvantages of these solutions. In particular, it addresses the
implementation and use of implicit coercions within the type theory,
the styles of proof that can be used, and the borrowing of concepts
from the literate programming paradigm. To be more specific, the
algebra in question is a constructive version of the fundamental
theorem of Galois Theory. The formalisation is developed within a
variant of the Unified Theory of Types that is implemented by a
modified version of the LEGO proofchecker.",
paper = "Bail98.pdf",
keywords = "axiomref"
}
\end{chunk}
\index{Mulligan, Dominic P.}
\begin{chunk}{axiom.bib}
@misc{Mull13,
author = "Mulligan, Dominic P.",
title = {{Mosquito: An Aimplementation for HigherOrder Logic}},
school = "University of Cambridge",
year = "2013",
abstract =
"We present Mosquito: an experimental stateless, pure, largely total
LCFstyle implementation of higherorder logic using Haskell as a
metalanguage. We discuss details of the logic implemented, kernel
design, and novel proof state and tactic representations.",
paper = "Mull13.pdf"
}
\end{chunk}

books/axiom.bib  195 ++++++++++++++++++++++++
books/bookvolbib.pamphlet  243 ++++++++++++++++++++++++++++++
changelog  2 +
patch  315 +++++++++++++++++++++++++++++
src/axiomwebsite/patches.html  2 +
5 files changed, 666 insertions(+), 91 deletions()
diff git a/books/axiom.bib b/books/axiom.bib
index 3e85ba6..76b00af 100644
 a/books/axiom.bib
+++ b/books/axiom.bib
@@ 6947,6 +6947,51 @@ paper = "Brea89.pdf"
paper = "Yous04.pdf"
}
+@article{Aspe09,
+ author = "Asperti, Andrea and Ricciotti, Wilmer and Coer, Claudio
+ Sacerdoti and Tassi, Enrico",
+ title = {{A Compact Kernel for the Calculus of Inductive Constructions}},
+ journal = "Sadhana",
+ volume = "34",
+ number = "1",
+ year = "2009",
+ pages = "71104",
+ abstract =
+ "The paper describes the new kernel for the Calculus of Inductive
+ Constructions (CIC) implemented inside the Matita Interactive
+ Theorem Prover. The design of the new kernel has been completely
+ revisited since the first release, resulting in a remarkably compact
+ implementation of about 2300 lines of OCaml code. The work is meant
+ for people interested in implementation aspects of Interactive
+ Provers, and is not self contained . In particular, it requires good
+ acquaintance with Type Theory and functional programming
+ languages.",
+ paper = "Aspe09.pdf"
+}
+
+@inproceedings{Aspe11,
+ author = "Asperti, Andrea and Ricciotti, Wilmer and Coer, Claudio
+ Sacerdoti and Tassi, Enrico",
+ title = {{The Matita Interactive Theorem Prover}},
+ booktitle = "CADE23 Automated Deduction",
+ year = "2011",
+ pages = "6469",
+ abstract =
+ "Matita is an interactive theorem prover being developed by the Helm
+ team at the University of Bologna. Its stable version 0.5.x may be
+ downloaded at http://matita.cs.unibo.it . The tool originated in the
+ European project MoWGLI as a set of XMLbased tools aimed to provide a
+ mathematicianfriendly webinterface to repositories of formal
+ mathematical knoweldge, supporting advanced contentbased
+ functionalities for querying, searching and browsing the library. It
+ has since then evolved into a fully fledged ITP, specifically designed
+ as a lightweight, but competitive system, particularly suited for the
+ assessment of innovative ideas, both at foundational and logical
+ level. In this paper, we give an account of the whole system, its
+ peculiarities and its main applications.",
+ paper = "Aspe11.pdf",
+}
+
@book{Appe17,
author = "Appel, Andrew W.",
title = {{Verified Functional Algorithms}},
@@ 7000,6 +7045,14 @@ paper = "Brea89.pdf"
paper = "Bate85.pdf"
}
+@book{Bish12,
+ author = "Bishop, Errett",
+ title = {{Foundations of Constructive Analysis}},
+ publisher = "ISHI Press",
+ year = "2012",
+ isbn = "9784871877145"
+}
+
@inproceedings{Blak96,
author = "Blakley, Bob",
title = {{The Emperor's Old Armor}},
@@ 7185,6 +7238,25 @@ paper = "Brea89.pdf"
paper = "Chli17.pdf"
}
+@article{Coen10,
+ author = "Coen, Claudio Sacerdoti",
+ title = {{Declarative Representation of Proof Terms}},
+ journal = "J. Automated Reasoning",
+ volume = "44",
+ number = "12",
+ pages = "2552",
+ year = "2010",
+ abstract =
+ "We present a declarative language inspired by the pseudonatural
+ language previously used in Matita for the explanation of proof
+ terms. We show how to compile the language to proof terms and how to
+ automatically generate declarative scripts from proof terms. Then we
+ investigate the relationship between the two translations, identifying
+ the amount of proof structure preserved by compilation and
+ regeneration of declarative scripts.",
+ paper = "Coen10.pdf"
+}
+
@article{Cons85a,
author = "Constable, R.L. and Knoblock, T.B. and Gates, J.L.",
title = {{Writing Programs that Construct Proofs}},
@@ 7404,6 +7476,66 @@ paper = "Brea89.pdf"
paper = "Lind88.pdf"
}
+@inproceedings{Luox96,
+ author = "Luo, Zhaohui",
+ title = {{Coercive Subtyping in Type Theory}},
+ booktitle = "CSL'96 Euro. Ass. for Comput. Sci. Logic",
+ year = "1996",
+ abstract =
+ "We propose and study coercive subtyping, a formal extension with
+ subtyping of dependent type theories such as MartinLof's type theory
+ [NPS90] and the type theory UTT [Luo94]. In this approach, subtyping
+ with specied implicit coercions is treated as a feature at the level
+ of the logical framework; in particular, subsumption and coercion are
+ combined in such a way that the meaning of an object being in a
+ supertype is given by coercive definition rules for the definitional
+ equality. It is shown that this provides a conceptually simple and
+ uniform framework to understand subtyping and coercion relations in
+ type theories with sophisticated type structures such as inductive
+ types and universes. The use of coercive subtyping in formal
+ development and in reasoning about subsets of objects is discussed in
+ the context of computerassisted formal reasoning.",
+ paper = "Luox96.pdf"
+}
+
+@misc{Luox11,
+ author = "Luo, Zhaohui",
+ title = {{TypeTheoretical Semantics with Coercive Subtyping}},
+ year = "2011",
+ comment = "Lecture Notes 2011 ESSLLI Summer School, Ljubljana,
+ Slovenia",
+ paper = "Luox11.pdf"
+}
+
+@article{Luox13,
+ author = "Luo, Zhaohui and Soloviev, Sergei and Xue, Tao",
+ title = {{Coercive Subtyping: Theory and Implementation}},
+ volume = "223",
+ pages = "1842",
+ link =
+ "\url{https://halunivtlse3.archivesouvertes.fr/hal01130574/document}",
+ abstract =
+ "Coercive subtyping is a useful and powerful framework of subtyping
+ for type theories. The key idea of coercive subtyping is subtyping
+ as abbreviation. In this paper, we give a new and adequate formulation
+ of T[C] , the system that extends a type theory T with coercive
+ subtyping based on a set C of basic subtyping judgements, and show
+ that coercive subtyping is a conservative extension and, in a more
+ general sense, a definitional extension. We introduce an intermediate
+ system, the starcalculus T[C]∗ , in which the positions that
+ require coercion insertions are marked, and show that T[C]∗ is a
+ conservative extension of T and that T[C]∗ is equivalent to T[C].
+ This makes clear what we mean by coercive subtyping being a
+ conservative extension, on the one hand, and amends a technical
+ problem that has led to a gap in the earlier conservativity proof, on
+ the other. We also compare coercive subtyping with the ‘ordinary’
+ notion of subtyping – subsumptive subtyping, and show that the former
+ is adequate for type theories with canonical objects while the latter
+ is not. An improved implementation of coercive subtyping is done in
+ the proof assistant Plastic.",
+ paper = "Luox13.pdf"
+}
+
@article{Mann78,
author = "Manna, Zohar and Waldinger, Richard",
title = {{The Logic of Computer Programming}},
@@ 7501,6 +7633,19 @@ paper = "Brea89.pdf"
paper = "Mart79.pdf"
}
+@misc{Mull13,
+ author = "Mulligan, Dominic P.",
+ title = {{Mosquito: An Aimplementation for HigherOrder Logic}},
+ school = "University of Cambridge",
+ year = "2013",
+ abstract =
+ "We present Mosquito: an experimental stateless, pure, largely total
+ LCFstyle implementation of higherorder logic using Haskell as a
+ metalanguage. We discuss details of the logic implemented, kernel
+ design, and novel proof state and tactic representations.",
+ paper = "Mull13.pdf"
+}
+
@techreport{Pier97,
author = "Pierce, Benjamin C. and Turner, David N.",
title = {{Local Type Inference}},
@@ 7607,6 +7752,23 @@ paper = "Brea89.pdf"
paper = "Ruzi89.pdf"
}
+@article{Scot76,
+ author = "Scott, Dana",
+ title = {{Data Types as Lattices}},
+ journal = "SIAM J. Comput.",
+ volume = "5",
+ year = "1976",
+ pages = "522587",
+ abstract =
+ "The meaning of many kinds of expressions in programming languages can
+ be taken as elements of certain spaces of 'partial' objects. In this
+ report these spaces are modeled in one univeral domain $P_\omega$, the
+ set of all subsets of the integers. This domain renders the connection
+ of this semantic theory with the ordinary theor of number theoretic
+ (especailly general recursive) functions clear and straightforward.",
+ paper = "Scot76.pdf"
+}
+
@article{Tryb92,
author = "Trybulec, Zinaida and Swieczkowska, Halina",
title = {{Some Remarks on The Language of Mathematical Texts}},
@@ 32948,6 +33110,37 @@ paper = "Brea89.pdf"
paper = "Bail96.pdf"
}
+@phdthesis{Bail98,
+ author = "Bailey, Anthony",
+ title = {{The MachineChecked Literate Formalisation of Algebra
+ in Type Theory}},
+ school = "University of Manchester",
+ year = "1998",
+ link =
+ "\url{http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.464.1249&rep=rep1&type=pdf}",
+ abstract =
+ "I present a largescale formalisation within a type theory of a
+ proof of a result from abstract algebra. The formalisation body
+ consists of files that are machinechecked to ensure their
+ correctness, and also processed to produce a report on the proof that
+ is humanreadable. The resulting presentation is intended to approach
+ being a standard informal account of some mathematics. In addition
+ to presenting this proof, the thesis also identifies and examines
+ problems in reconciling the formal nature of the development with the
+ wish for it to be easy to read. It presents some tools and methodologies
+ for solving these problems, and discusses the advantages and
+ disadvantages of these solutions. In particular, it addresses the
+ implementation and use of implicit coercions within the type theory,
+ the styles of proof that can be used, and the borrowing of concepts
+ from the literate programming paradigm. To be more specific, the
+ algebra in question is a constructive version of the fundamental
+ theorem of Galois Theory. The formalisation is developed within a
+ variant of the Unified Theory of Types that is implemented by a
+ modified version of the LEGO proofchecker.",
+ paper = "Bail98.pdf",
+ keywords = "axiomref"
+}
+
@misc{Bake14,
author = "Baker, Martin",
title = {{Axiom Architecture}},
@@ 36048,7 +36241,7 @@ paper = "Brea89.pdf"
abstract =
"The constructive approach to mathematics has enjoyed a renaissance,
caused in large part by the appearance of Errett Bishop's book
 Foundations of constructiue analysis in 1967, and by the subtle
+ Foundations of constructive analysis in 1967, and by the subtle
influences of the proliferation of powerful computers. Bishop
demonstrated that pure mathematics can be developed from a
constructive point of view while maintaining a continuity with
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 5391370..a03fab5 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 9448,6 +9448,65 @@ when shown in factored form.
\section{Proving Axiom Correct  The Project} %%%%%%%%%%%%%%%%%%%%
+\index{Asperti, Andrea}
+\index{Ricciotti, Wilmer}
+\index{Coer, Claudio Sacerdoti}
+\index{Tassi, Enrico}
+\begin{chunk}{axiom.bib}
+@article{Aspe09,
+ author = "Asperti, Andrea and Ricciotti, Wilmer and Coer, Claudio
+ Sacerdoti and Tassi, Enrico",
+ title = {{A Compact Kernel for the Calculus of Inductive Constructions}},
+ journal = "Sadhana",
+ volume = "34",
+ number = "1",
+ year = "2009",
+ pages = "71104",
+ abstract =
+ "The paper describes the new kernel for the Calculus of Inductive
+ Constructions (CIC) implemented inside the Matita Interactive
+ Theorem Prover. The design of the new kernel has been completely
+ revisited since the first release, resulting in a remarkably compact
+ implementation of about 2300 lines of OCaml code. The work is meant
+ for people interested in implementation aspects of Interactive
+ Provers, and is not self contained . In particular, it requires good
+ acquaintance with Type Theory and functional programming
+ languages.",
+ paper = "Aspe09.pdf"
+}
+
+\end{chunk}
+
+\index{Asperti, Andrea}
+\index{Ricciotti, Wilmer}
+\index{Coer, Claudio Sacerdoti}
+\index{Tassi, Enrico}
+\begin{chunk}{axiom.bib}
+@inproceedings{Aspe11,
+ author = "Asperti, Andrea and Ricciotti, Wilmer and Coer, Claudio
+ Sacerdoti and Tassi, Enrico",
+ title = {{The Matita Interactive Theorem Prover}},
+ booktitle = "CADE23 Automated Deduction",
+ year = "2011",
+ pages = "6469",
+ abstract =
+ "Matita is an interactive theorem prover being developed by the Helm
+ team at the University of Bologna. Its stable version 0.5.x may be
+ downloaded at http://matita.cs.unibo.it . The tool originated in the
+ European project MoWGLI as a set of XMLbased tools aimed to provide a
+ mathematicianfriendly webinterface to repositories of formal
+ mathematical knoweldge, supporting advanced contentbased
+ functionalities for querying, searching and browsing the library. It
+ has since then evolved into a fully fledged ITP, specifically designed
+ as a lightweight, but competitive system, particularly suited for the
+ assessment of innovative ideas, both at foundational and logical
+ level. In this paper, we give an account of the whole system, its
+ peculiarities and its main applications.",
+ paper = "Aspe11.pdf",
+}
+
+\end{chunk}
+
\index{Appel, Andrew W.}
\begin{chunk}{axiom.bib}
@book{Appe17,
@@ 9515,6 +9574,18 @@ when shown in factored form.
\end{chunk}
+\index{Bishop, Errett}
+\begin{chunk}{axiom.bib}
+@book{Bish12,
+ author = "Bishop, Errett",
+ title = {{Foundations of Constructive Analysis}},
+ publisher = "ISHI Press",
+ year = "2012",
+ isbn = "9784871877145"
+}
+
+\end{chunk}
+
\index{Blakley, Bob}
\begin{chunk}{axiom.bib}
@inproceedings{Blak96,
@@ 9722,6 +9793,29 @@ when shown in factored form.
\end{chunk}
+\index{Coen, Claudio Sacerdoti}
+\begin{chunk}{axiom.bib}
+@article{Coen10,
+ author = "Coen, Claudio Sacerdoti",
+ title = {{Declarative Representation of Proof Terms}},
+ journal = "J. Automated Reasoning",
+ volume = "44",
+ number = "12",
+ pages = "2552",
+ year = "2010",
+ abstract =
+ "We present a declarative language inspired by the pseudonatural
+ language previously used in Matita for the explanation of proof
+ terms. We show how to compile the language to proof terms and how to
+ automatically generate declarative scripts from proof terms. Then we
+ investigate the relationship between the two translations, identifying
+ the amount of proof structure preserved by compilation and
+ regeneration of declarative scripts.",
+ paper = "Coen10.pdf"
+}
+
+\end{chunk}
+
\index{Constable, R.L.}
\index{Knoblock, T.B.}
\index{Gates, J.L.}
@@ 9995,6 +10089,80 @@ when shown in factored form.
\end{chunk}
+\index{Luo, Zhaohui}
+\begin{chunk}{axiom.bib}
+@inproceedings{Luox96,
+ author = "Luo, Zhaohui",
+ title = {{Coercive Subtyping in Type Theory}},
+ booktitle = "CSL'96 Euro. Ass. for Comput. Sci. Logic",
+ year = "1996",
+ abstract =
+ "We propose and study coercive subtyping, a formal extension with
+ subtyping of dependent type theories such as MartinLof's type theory
+ [NPS90] and the type theory UTT [Luo94]. In this approach, subtyping
+ with specied implicit coercions is treated as a feature at the level
+ of the logical framework; in particular, subsumption and coercion are
+ combined in such a way that the meaning of an object being in a
+ supertype is given by coercive definition rules for the definitional
+ equality. It is shown that this provides a conceptually simple and
+ uniform framework to understand subtyping and coercion relations in
+ type theories with sophisticated type structures such as inductive
+ types and universes. The use of coercive subtyping in formal
+ development and in reasoning about subsets of objects is discussed in
+ the context of computerassisted formal reasoning.",
+ paper = "Luox96.pdf"
+}
+
+\end{chunk}
+
+\index{Luo, Zhaohui}
+\begin{chunk}{axiom.bib}
+@misc{Luox11,
+ author = "Luo, Zhaohui",
+ title = {{TypeTheoretical Semantics with Coercive Subtyping}},
+ year = "2011",
+ comment = "Lecture Notes 2011 ESSLLI Summer School, Ljubljana,
+ Slovenia",
+ paper = "Luox11.pdf"
+}
+
+\end{chunk}
+
+\index{Luo, Zhaohui}
+\index{Soloviev, Sergei}
+\index{Xue, Tao}
+\begin{chunk}{axiom.bib}
+@article{Luox13,
+ author = "Luo, Zhaohui and Soloviev, Sergei and Xue, Tao",
+ title = {{Coercive Subtyping: Theory and Implementation}},
+ volume = "223",
+ pages = "1842",
+ link =
+ "\url{https://halunivtlse3.archivesouvertes.fr/hal01130574/document}",
+ abstract =
+ "Coercive subtyping is a useful and powerful framework of subtyping
+ for type theories. The key idea of coercive subtyping is subtyping
+ as abbreviation. In this paper, we give a new and adequate formulation
+ of T[C] , the system that extends a type theory T with coercive
+ subtyping based on a set C of basic subtyping judgements, and show
+ that coercive subtyping is a conservative extension and, in a more
+ general sense, a definitional extension. We introduce an intermediate
+ system, the starcalculus T[C]∗ , in which the positions that
+ require coercion insertions are marked, and show that T[C]∗ is a
+ conservative extension of T and that T[C]∗ is equivalent to T[C].
+ This makes clear what we mean by coercive subtyping being a
+ conservative extension, on the one hand, and amends a technical
+ problem that has led to a gap in the earlier conservativity proof, on
+ the other. We also compare coercive subtyping with the ‘ordinary’
+ notion of subtyping – subsumptive subtyping, and show that the former
+ is adequate for type theories with canonical objects while the latter
+ is not. An improved implementation of coercive subtyping is done in
+ the proof assistant Plastic.",
+ paper = "Luox13.pdf"
+}
+
+\end{chunk}
+
\index{Manna, Zohar}
\index{Waldinger, Richard}
\begin{chunk}{axiom.bib}
@@ 10109,6 +10277,23 @@ when shown in factored form.
\end{chunk}
+\index{Mulligan, Dominic P.}
+\begin{chunk}{axiom.bib}
+@misc{Mull13,
+ author = "Mulligan, Dominic P.",
+ title = {{Mosquito: An Aimplementation for HigherOrder Logic}},
+ school = "University of Cambridge",
+ year = "2013",
+ abstract =
+ "We present Mosquito: an experimental stateless, pure, largely total
+ LCFstyle implementation of higherorder logic using Haskell as a
+ metalanguage. We discuss details of the logic implemented, kernel
+ design, and novel proof state and tactic representations.",
+ paper = "Mull13.pdf"
+}
+
+\end{chunk}
+
\index{Pierce, Benjamin C.}
\index{Turner, David N.}
\begin{chunk}{axiom.bib}
@@ 10237,6 +10422,27 @@ when shown in factored form.
\end{chunk}
+\index{Scott, Dana}
+\begin{chunk}{axiom.bib}
+@article{Scot76,
+ author = "Scott, Dana",
+ title = {{Data Types as Lattices}},
+ journal = "SIAM J. Comput.",
+ volume = "5",
+ year = "1976",
+ pages = "522587",
+ abstract =
+ "The meaning of many kinds of expressions in programming languages can
+ be taken as elements of certain spaces of 'partial' objects. In this
+ report these spaces are modeled in one univeral domain $P_\omega$, the
+ set of all subsets of the integers. This domain renders the connection
+ of this semantic theory with the ordinary theor of number theoretic
+ (especailly general recursive) functions clear and straightforward.",
+ paper = "Scot76.pdf"
+}
+
+\end{chunk}
+
\index{Trybulec, Zinaida}
\index{Swieczkowska, Halina}
\begin{chunk}{axiom.bib}
@@ 48136,6 +48342,41 @@ SIAM J. Appl. Math . 14 242249. (1966)
\end{chunk}
+\index{Bailey, Anthony}
+\begin{chunk}{axiom.bib}
+@phdthesis{Bail98,
+ author = "Bailey, Anthony",
+ title = {{The MachineChecked Literate Formalisation of Algebra
+ in Type Theory}},
+ school = "University of Manchester",
+ year = "1998",
+ link =
+ "\url{http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.464.1249&rep=rep1&type=pdf}",
+ abstract =
+ "I present a largescale formalisation within a type theory of a
+ proof of a result from abstract algebra. The formalisation body
+ consists of files that are machinechecked to ensure their
+ correctness, and also processed to produce a report on the proof that
+ is humanreadable. The resulting presentation is intended to approach
+ being a standard informal account of some mathematics. In addition
+ to presenting this proof, the thesis also identifies and examines
+ problems in reconciling the formal nature of the development with the
+ wish for it to be easy to read. It presents some tools and methodologies
+ for solving these problems, and discusses the advantages and
+ disadvantages of these solutions. In particular, it addresses the
+ implementation and use of implicit coercions within the type theory,
+ the styles of proof that can be used, and the borrowing of concepts
+ from the literate programming paradigm. To be more specific, the
+ algebra in question is a constructive version of the fundamental
+ theorem of Galois Theory. The formalisation is developed within a
+ variant of the Unified Theory of Types that is implemented by a
+ modified version of the LEGO proofchecker.",
+ paper = "Bail98.pdf",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
\index{Baker, George A.}
\index{GravesMorris, Peter}
\begin{chunk}{ignore}
@@ 53683,7 +53924,7 @@ Elsevier. (1967)
abstract =
"The constructive approach to mathematics has enjoyed a renaissance,
caused in large part by the appearance of Errett Bishop's book
 Foundations of constructiue analysis in 1967, and by the subtle
+ Foundations of constructive analysis in 1967, and by the subtle
influences of the proliferation of powerful computers. Bishop
demonstrated that pure mathematics can be developed from a
constructive point of view while maintaining a continuity with
diff git a/changelog b/changelog
index 4bbbedc..63bee41 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20180109 tpd src/axiomwebsite/patches.html 20180109.01.tpd.patch
+20180109 tpd books/bookvolbib add references
20180106 tpd src/axiomwebsite/patches.html 20180106.01.tpd.patch
20180106 tpd books/bookvolbib add references
20180101 tpd src/axiomwebsite/patches.html 20180101.02.tpd.patch
diff git a/patch b/patch
index 88fc941..da2642a 100644
 a/patch
+++ b/patch
@@ 2,115 +2,252 @@ books/bookvolbib add references
Goal: Proving Axiom Correct
\index{Pierce, Benjamin C.}
\index{Turner, David N.}
+\index{Scott, Dana}
\begin{chunk}{axiom.bib}
@techreport{Pier97,
 author = "Pierce, Benjamin C. and Turner, David N.",
 title = {{Local Type Inference}},
 institution = "Indiana University",
 year = "1997",
 type = "CSCI Technical Report",
 number = "493",
+@article{Scot76,
+ author = "Scott, Dana",
+ title = {{Data Types as Lattices}},
+ journal = "SIAM J. Comput.",
+ volume = "5",
+ year = "1976",
+ pages = "522587",
abstract =
 "We study two partial type inference methods for a language combining
 subtyping and impredicative polymorphism. Both methods are {\sl local}
 in the sense that missing annotations are recovered using only
 information from adjacent nodes in the syntax tree, without long
 distance constraints such as unification variables. One method infers
 type arguments in polymorphic applications using a local constraint
 solver. The other infers annotations on bound variables in function
 abstractions by propagating type constraints downward from enclosing
 application nodes. We motivate our design choices by a statistical
 analysis of the uses of type inference in a sizable body of existing
 ML code.",
 paper = "Pier97.pdf"
+ "The meaning of many kinds of expressions in programming languages can
+ be taken as elements of certain spaces of 'partial' objects. In this
+ report these spaces are modeled in one univeral domain $P_\omega$, the
+ set of all subsets of the integers. This domain renders the connection
+ of this semantic theory with the ordinary theor of number theoretic
+ (especailly general recursive) functions clear and straightforward.",
+ paper = "Scot76.pdf"
}
\end{chunk}
\index{Ruzicka, Peter}
\index{Privara, Igor}
+\index{Bishop, Errett}
\begin{chunk}{axiom.bib}
@article{Ruzi89,
 author = "Ruzicka, Peter and Privara, Igor",
 title = {{An Almost Linear Robinson Unification Algorithm}},
 journal = "Acta Informatica",
 volume = "27",
 pages = "6171",
 year = "1989",
+@book{Bish12,
+ author = "Bishop, Errett",
+ title = {{Foundations of Constructive Analysis}},
+ publisher = "ISHI Press",
+ year = "2012",
+ isbn = "9784871877145"
+}
+
+\end{chunk}
+
+\index{Asperti, Andrea}
+\index{Ricciotti, Wilmer}
+\index{Coer, Claudio Sacerdoti}
+\index{Tassi, Enrico}
+\begin{chunk}{axiom.bib}
+@article{Aspe09,
+ author = "Asperti, Andrea and Ricciotti, Wilmer and Coer, Claudio
+ Sacerdoti and Tassi, Enrico",
+ title = {{A Compact Kernel for the Calculus of Inductive Constructions}},
+ journal = "Sadhana",
+ volume = "34",
+ number = "1",
+ year = "2009",
+ pages = "71104",
+ abstract =
+ "The paper describes the new kernel for the Calculus of Inductive
+ Constructions (CIC) implemented inside the Matita Interactive
+ Theorem Prover. The design of the new kernel has been completely
+ revisited since the first release, resulting in a remarkably compact
+ implementation of about 2300 lines of OCaml code. The work is meant
+ for people interested in implementation aspects of Interactive
+ Provers, and is not self contained . In particular, it requires good
+ acquaintance with Type Theory and functional programming
+ languages.",
+ paper = "Aspe09.pdf"
+}
+
+\end{chunk}
+
+\index{Asperti, Andrea}
+\index{Ricciotti, Wilmer}
+\index{Coer, Claudio Sacerdoti}
+\index{Tassi, Enrico}
+\begin{chunk}{axiom.bib}
+@inproceedings{Aspe11,
+ author = "Asperti, Andrea and Ricciotti, Wilmer and Coer, Claudio
+ Sacerdoti and Tassi, Enrico",
+ title = {{The Matita Interactive Theorem Prover}},
+ booktitle = "CADE23 Automated Deduction",
+ year = "2011",
+ pages = "6469",
+ abstract =
+ "Matita is an interactive theorem prover being developed by the Helm
+ team at the University of Bologna. Its stable version 0.5.x may be
+ downloaded at http://matita.cs.unibo.it . The tool originated in the
+ European project MoWGLI as a set of XMLbased tools aimed to provide a
+ mathematicianfriendly webinterface to repositories of formal
+ mathematical knoweldge, supporting advanced contentbased
+ functionalities for querying, searching and browsing the library. It
+ has since then evolved into a fully fledged ITP, specifically designed
+ as a lightweight, but competitive system, particularly suited for the
+ assessment of innovative ideas, both at foundational and logical
+ level. In this paper, we give an account of the whole system, its
+ peculiarities and its main applications.",
+ paper = "Aspe11.pdf",
+}
+
+\end{chunk}
+
+\index{Spitters, Bas}
+\index{van der Weegen, Eelis}
+\begin{chunk}{axiom.bib}
+@article{Spit11,
+ author = "Spitters, Bas and van der Weegen, Eelis",
+ title = {{Type Classes for Mathematics in Type Theory}},
+ journal = "Math. Struct. Comput. Sci.",
+ volume = "21",
+ number = "4",
+ pages = "795825",
+ year = "2011",
+ abstract =
+ "The introduction of firstclass type classes in the Coq system calls
+ for reexamination of the basic interfaces used for mathematical
+ formalization in type theory. We present a new set of type classes for
+ mathematics and take full advantage of their unique features to make
+ practical a particularly flexible approach formerly thought
+ infeasible. Thus, we address both traditional proof engineering
+ challenges as well as new ones resulting from our ambition to build
+ upon this development a library of constructive analysis in which
+ abstraction penalties inhibiting efficient computation are reduced to
+ a minimum.
+
+ The base of our development consists of type classes representing a
+ standard algebraic hierarchy, as well as portions of category theory
+ and universal algebra. On this foundation we build a set of
+ mathematically sound abstract interfaces for different kinds of
+ numbers, succinctly expressed using categorical language and universal
+ algebra constructions. Strategic use of type classes lets us support
+ these highlevel theoryfriendly definitions while still enabling
+ efficient implementations unhindered by gratuitous indirection,
+ conversion or projection.
+
+ Algebra thrives on the interplay between syntax and semantics. The
+ Prologlike abilities of type class instance resolution allow us to
+ conveniently define a quote function, thus facilitating the use of
+ reflective techniques.",
+ paper = "Spit11.pdf"
+}
+
+\end{chunk}
+
+\index{Coen, Claudio Sacerdoti}
+\begin{chunk}{axiom.bib}
+@article{Coen10,
+ author = "Coen, Claudio Sacerdoti",
+ title = {{Declarative Representation of Proof Terms}},
+ journal = "J. Automated Reasoning",
+ volume = "44",
+ number = "12",
+ pages = "2552",
+ year = "2010",
abstract =
 "Further asymptotical improvement of original Robinson's unification
 idea is presented. By postponing the socalled occurcheck in Corbin
 and Bidoit's quadratic rehabilitation of the Robinson algorithm at the
 end of unification an almost linear unification algorithm is obtained.
 In the worst case, the resulting algorithm has the time complexity
 O(p.A(p)), where p is the size of input terms and A is the inverse to
 the Ackermann function. Moreover, the practical experiments are
 summarized comparing Corbin and Bidoit's quadratic algorithm with the
 resulting almost linear unification algorithm based on Robinson's
 principle. ",
 paper = "Ruzi89.pdf"
+ "We present a declarative language inspired by the pseudonatural
+ language previously used in Matita for the explanation of proof
+ terms. We show how to compile the language to proof terms and how to
+ automatically generate declarative scripts from proof terms. Then we
+ investigate the relationship between the two translations, identifying
+ the amount of proof structure preserved by compilation and
+ regeneration of declarative scripts.",
+ paper = "Coen10.pdf"
}
\end{chunk}
\index{Robinson, J.A.}
+\index{Luo, Zhaohui}
\begin{chunk}{axiom.bib}
@article{Robi65,
 author = "Robinson, J.A.",
 title = {{A MachineOriented Logic Based on the Resolution Principle}},
 journal = "ACM",
 volume = "12",
 pages = "2341",
 year = "1965",
+@inproceedings{Luox96,
+ author = "Luo, Zhaohui",
+ title = {{Coercive Subtyping in Type Theory}},
+ booktitle = "CSL'96 Euro. Ass. for Comput. Sci. Logic",
+ year = "1996",
abstract =
 "Theoremproving on the computer, using procedures based on the
 fundamental theorem of Herbrand concerning the firstorder predicate
 calculus, is examined with a view towards improving the efficiency and
 widening the range of practical applicability of these procedures. A
 elose analysis of the process of substitution (of terms for
 variables), and the process of truthfunctional analysis of the
 results of such substitutions, reveals that both processes can be
 combined into a single new process (called resolution), iterating
 which is vastty more effieient than the older cyclic procedures
 consisting of substitution stages alternating with truthfunctional
 analysis stages.

 The theory of the resolution process is presented in the form of a
 system of firstorder logic with .just one inference principle (the
 resolution principle). The completeness of the system is proved; the
 simplest proofprocedure based on the system is then the direct
 implementation of the proof of completeness. Howewer, this procedure is
 quite inefficient, and the paper concludes with a discussion of
 several principles (called search principles) which are applicable to
 the design of efficient proofprocedures employing resolution as the
 basic logical process.",
 paper = "Robi65.pdf"
+ "We propose and study coercive subtyping, a formal extension with
+ subtyping of dependent type theories such as MartinLof's type theory
+ [NPS90] and the type theory UTT [Luo94]. In this approach, subtyping
+ with specied implicit coercions is treated as a feature at the level
+ of the logical framework; in particular, subsumption and coercion are
+ combined in such a way that the meaning of an object being in a
+ supertype is given by coercive definition rules for the definitional
+ equality. It is shown that this provides a conceptually simple and
+ uniform framework to understand subtyping and coercion relations in
+ type theories with sophisticated type structures such as inductive
+ types and universes. The use of coercive subtyping in formal
+ development and in reasoning about subsets of objects is discussed in
+ the context of computerassisted formal reasoning.",
+ paper = "Luox96.pdf"
+}
+
+\end{chunk}
+
+\index{Luo, Zhaohui}
+\begin{chunk}{axiom.bib}
+@misc{Luox11,
+ author = "Luo, Zhaohui",
+ title = {{TypeTheoretical Semantics with Coercive Subtyping}},
+ year = "2011",
+ comment = "Lecture Notes 2011 ESSLLI Summer School, Ljubljana,
+ Slovenia",
+ paper = "Luox11.pdf"
}
\end{chunk}
\index{van Lamsweerde, Axel}
+\index{Bailey, Anthony}
\begin{chunk}{axiom.bib}
@incollection{Lams00,
 author = "van Lamsweerde, Axel",
 title = {{Formal Specification: A Roadmap}},
 booktitle = "The Future of Software Engineering",
 publisher = "ACM Press",
 year = "2000",
+@phdthesis{Bail98,
+ author = "Bailey, Anthony",
+ title = {{The MachineChecked Literate Formalisation of Algebra
+ in Type Theory}},
+ school = "University of Manchester",
+ year = "1998",
+ link =
+ "\url{http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.464.1249&rep=rep1&type=pdf}",
abstract =
 "Formal specifications have been a focus of software engineering
 research for many years and have been applied in a wide variety of
 settings. Their industrial use is still limited but has been steadily
 growing. After recalling the essence, role, usage, and pitfalls of
 formal specification, the paper reviews the main specification
 paradigms to date and discuss their evaluation criteria. It then
 provides a brief assessment of the current strengths and weaknesses of
 today's formal specification technology. This provides a basis for
 formulating a number of requirements for formal specification to
 become a core software engineering activity in the future.",
 paper = "Lams00.pdf"
+ "I present a largescale formalisation within a type theory of a
+ proof of a result from abstract algebra. The formalisation body
+ consists of files that are machinechecked to ensure their
+ correctness, and also processed to produce a report on the proof that
+ is humanreadable. The resulting presentation is intended to approach
+ being a standard informal account of some mathematics. In addition
+ to presenting this proof, the thesis also identifies and examines
+ problems in reconciling the formal nature of the development with the
+ wish for it to be easy to read. It presents some tools and methodologies
+ for solving these problems, and discusses the advantages and
+ disadvantages of these solutions. In particular, it addresses the
+ implementation and use of implicit coercions within the type theory,
+ the styles of proof that can be used, and the borrowing of concepts
+ from the literate programming paradigm. To be more specific, the
+ algebra in question is a constructive version of the fundamental
+ theorem of Galois Theory. The formalisation is developed within a
+ variant of the Unified Theory of Types that is implemented by a
+ modified version of the LEGO proofchecker.",
+ paper = "Bail98.pdf",
+ keywords = "axiomref"
}
\end{chunk}
+
+\index{Mulligan, Dominic P.}
+\begin{chunk}{axiom.bib}
+@misc{Mull13,
+ author = "Mulligan, Dominic P.",
+ title = {{Mosquito: An Aimplementation for HigherOrder Logic}},
+ school = "University of Cambridge",
+ year = "2013",
+ abstract =
+ "We present Mosquito: an experimental stateless, pure, largely total
+ LCFstyle implementation of higherorder logic using Haskell as a
+ metalanguage. We discuss details of the logic implemented, kernel
+ design, and novel proof state and tactic representations.",
+ paper = "Mull13.pdf"
+}
+
+\end{chunk}
+
+
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 2eb0f34..81a0747 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5888,6 +5888,8 @@ books/bookheader.tex add date and git master
src/axiomwebsite/documentation.html add Pierce quote about TeX
20180106.01.tpd.patch
books/bookvolbib add references
+20180109.01.tpd.patch
+books/bookvolbib add references

1.9.1