From f133abe7b643ceba50bb0d96e612953edeefbd5f Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Wed, 6 Dec 2017 20:46:57 0500
Subject: [PATCH] books/bookvolbib add references
MIMEVersion: 1.0
ContentType: text/plain; charset=UTF8
ContentTransferEncoding: 8bit
Goal: Proving Axiom Correct  Coercion in CASProof Systesms
\index{Sozeau, Matthieu}
\begin{chunk}{axiom.bib}
\incollection{Soze06,
author = "Sozeau, Matthieu",
title = {{Subset Coercions in Coq}},
booktitle = "TYPES: Int. Workshop on Types for Proofs and Programs",
journal = "LNCS",
volume = "4502",
pages = "237252",
year = "2006",
abstract =
"We propose a new language for writing programs with dependent types
on top of the Coq proof assistant. This language permits to establish
a phase distinction between writing and proving algorithms in the Coq
environment. Concretely, this means allowing to write algorithms as
easily as in a practical functional programming language whilst giving
them as rich a specification as desired and proving that the code
meets the specification using the whole Coq proof apparatus. This is
achieved by extending conversion to an equivalence which relates
types and subsets based on them, a technique originating from the
``Predicate subtyping'' featureof PVS and following mathematical
convention. The typing judgements can be translated to the Calculus of
(Co)Inductive Constructions (Cic) by means of an interpretation
which inserts coercions at the appropriate places.These coercions
can contain existential variables representing the propositional
parts of the final term, corresponding to proof obligations (or
PVS typechecking conditions). A prototype implementation of this
process is integrated with the Coq environment.",
paper = "Soze06.pdf"
}
\end{chunk}
\index{Pierce, Benjamin}
\begin{chunk}{axiom.bib}
@misc{Pier17,
author = "Pierce, Benjamin",
title = "DeepSpec Summer School, Coq Intensive, Part 1 (July 13,2017)",
year = "2017",
link = "\url{https://www.youtube.com/watch?v=jG61w5pOc2A}"
}
\end{chunk}
\index{Haftmann, Florian}
\index{Wenzel, Makarius}
\begin{chunk}{axiom.bib}
@article{Haft06,
author = "Haftmann, Florian and Wenzel, Makarius",
title = {{Constructive Type Classes in Isabelle}},
journal = "LNCS",
volume = "4502",
year = "2006",
abstract =
"We reconsider the wellknown concept of Haskellstyle type classes
within the logical framework of Isabelle. So far, axiomatic type
classes in Isabelle merely account for the logical aspect as
predicates over types, while the opera tional part is only a
convention based on raw overloading. Our more elaborate approach to
constructive type classes provides a seamless integration with
Isabelle locales, which are able to manage both operations and logical
properties uniformly. Thus we combine the convenience of type
classes and the flexibility of locales. Furthermore, we construct
dictionary terms derived from notions of the type system. This
additional internal structure provides satisfactory foundations of
type classes, and supports further applications, such as code
generation and export of theories and theorems to environments without
type classes.",
paper = "Haft06.pdf"
}
\end{chunk}
\index{Kiessling, Robert}
\index{Luo, Zhaohui}
\begin{chunk}{axiom.bib}
@article{Kies03,
author = "Kiessling, Robert and Luo, Zhaohui",
title = {{Coercions in HindleyMilner Systems}},
journal = "LNCS",
volume = "3085",
year = "2003",
abstract =
"Coercive subtyping is a theory of abbreviation for dependent type
theories. In this paper, we incorporate the idea of coercive subtyping
into the traditional HindleyMilner type systems in functional
programming languages. This results in a typing system with coercions,
an extension of the HindleyMilner type system. A type inference
algorithm is developed and shown to be sound and complete with respect
to the typing system. A notion of derivational coherence is developed
to deal with the problem of ambiguity and the corresponding type
inference algorithm is shown to be sound and complete.",
paper = "Kies03.pdf"
}
\end{chunk}
\index{Wiedijk, Freek}
\begin{chunk}{axiom.bib}
@article{Wied03,
author = "Wiedijk, Freek",
title = {{Formal Proof Sketches}},
journal = "LNCS",
volume = "3085",
year = "2003",
pages = "378393",
abstract =
"Formalized mathematics currently does not look much like informal
mathematics. Also, formalizing mathematics currently seems far too
much work to be worth the time of the working mathematician. To
address both of these problems we introduce the notion of a formal
proof sketch . This is a proof representation that is in between a
fully checkable formal proof and a statement without any proof at
all. Although a formal proof sketch is too high level to be checkable
by computer, it has a precise notion of correctness (hence the
adjective formal ). We will show through examples that formal proof
sketches can closely mimic already existing mathematical
proofs. Therefore, although a formal proof sketch contains gaps in
the reasoning from a formal point of view (which is why we call it a
sketch ), a mathematician probably would call such a text just a
‘proof’.",
paper = "Wied03.pdf"
}
\end{chunk}
\index{Coquand, Thierry}
\index{Persson, Henrik}
\begin{chunk}{axiom.bib}
@article{Coqu98,
author = "Coquand, Thierry and Persson, Henrik",
title = {{Groebner Bases in Type Theory}},
journal = "LNCS",
volume = "1657",
year = "1998",
pages = "3346",
abstract =
"We describe how the theory of Groebner bases, an important part
of computational algebra, can be developed within Martin Lof’s
type theory. In particular, we aim for an integrated development
of the algorithms for computing Groebner bases: we want to prove,
constructively in type theory, the existence of Groebner bases and
from such proofs extract the algorithms. Our main contribution is
a reformulation of the standard theory of Groebner bases which
uses generalised inductive definitions. We isolate the main
non–constructive part, a minimal bad sequence argument, and use
the open induction principle [Rao88,Coq92] to interpret it by
induction. This leads to short constructive proofs of Dickson’s
lemma and Hilbert’s basis theorem, which are used to give an
integrated development of Buchberger’s algorithm. An important
point of this work is that the elegance and brevity of the
original proofs are maintained while the new proofs also have a
direct constructive content. In the appendix we present a
computer formalisation of Dickson’s lemma and an abstract
existence proof of Groebner bases.",
paper = "Coqu98.pdf"
}
\end{chunk}
\index{Filliatre, JeanChristophe}
\begin{chunk}{axiom.bib}
@article{Fill98,
author = "Filliatre, JeanChristophe",
title = {{Proof of Imperative Programs in Type Theory}},
journal = "LNCS",
volume = "1657",
year = "1998",
pages = "7892",
abstract =
"We present a new approach to certifying functional programs with
imperative aspects, in the context of Type Theory. The key is a
functional translation of imperative programs, based on a combination
of the type and effect discipline and monads. Then an incomplete proof
of the specification is built in the Type Theory, whose gaps would
corre spond to proof obligations. On sequential imperative programs,
we get the same proof obligations as those given by FloydHoare
logic. Compared to the latter, our approach also includes functional
constructions in a straightforward way. This work has been
implemented in the Coq Proof Assistant and applied on nontrivial
examples.",
paper = "Fill98.pdf"
}
\end{chunk}
\index{Nipkow, Tobias}
\begin{chunk}{axiom.bib}
@article{Nipk02,
author = "Nipkow, Tobias",
title = {{Structured Proofs in Isar/HOL}},
journal = "LNCS",
volume = "2646",
year = "2002",
pages = "259278",
abstract =
"Isar is an extension of the theorem prover Isabelle with a language
for writing humanreadable structured proofs. This paper is an
introduction to the basic constructs of this language.",
paper = "Nipk02.pdf"
}
\end{chunk}
\index{Carlstrom, Jesper}
\begin{chunk}{axiom.bib}
@article{Carl02,
author = "Carlstrom, Jesper",
title = {{Subsets, Quotients, and Partial Functions in MartinL\"of's
Type Theory}},
journal = "LNCS",
volume = "2646",
year = "2002",
pages = "7894",
abstract =
"We treat subsets, equivalence relations, and partial functions,
with subsets as propositional functions .In order for these three
notions to work well together, we propose some changes to the theory
of subsets as propositional functions .The method used is not to make
any changes to the type theory itself, but to view the new concepts as
defined ones.",
paper = "Carl02.pdf"
}
\end{chunk}
\index{Bove, Ana}
\begin{chunk}{axiom.bib}
@article{Bove02,
author = "Bove, Ana",
title = {{General Recursion in Type Theory}},
journal = "LNCS",
volume = "2646",
pages = "3958",
abstract =
"In this work, a method to formalise general recursive algorithms in
constructive type theory is presented throughout examples. The method
separates the computational and logical parts of the definitions. As
a consequence, the resulting typetheoretic algorithms are clear,
compact and easy to understand. They are as simple as their
equivalents in a functional programming language, where there is no
restriction on recursive calls. Given a general recursive algorithm,
the method consists in defining an inductive specialpurpose
accessibility predicate that characterises the inputs on which the
algorithm terminates. The typetheoretic version of the algorithm can
then be defined by structural recursion on the proof that the input
values satisfy this predicate. When formalising nested algorithms, the
specialpurpose accessibility predicate and the typetheoretic version
of the algorithm must be defined simultaneously because they depend on
each other. Since the method separates the computational part from
the logical part of a definition, formalising partial functions
becomes also possible.",
paper = "Bove02.pdf"
}
\end{chunk}
\index{Coen, Claudio Sacerdoti}
\index{Tassi, Enrico}
\begin{chunk}{axiom.bib}
@article{Coen07,
author = "Coen, Claudio Sacerdoti and Tassi, Enrico",
title = {{Working with Mathematical Structures in Type Theory}},
journal = "LNCS",
volume = "4941",
year = "2007",
pages = "157172",
abstract =
"We address the problem of representing mathematical structures in a
proof assistant which: 1) is based on a type theory with depen dent
types, telescopes and a computational version of Leibniz equality; 2)
implements coercive subtyping, accepting multiple coherent paths
between type families; 3) implements a restricted form of higher order
unification and type reconstruction. We show how to exploit the
previous quite common features to reduce the ``syntactic'' gap between
pen and paper and formalised algebra. However, to reach our goal we need
to propose unification and type reconstruction heuristics that are
slightly different from the ones usually implemented. We have
implemented them in Matita.",
paper = "Coen07.pdf"
}
\end{chunk}
\index{Coquand, Thierry}
\begin{chunk}{axiom.bib}
@article{Coqu93,
author = "Coquand, Thierry",
title = {{Infinite Objects in Type Theory}},
journal = "LNCS",
volume = "806",
year = "1993",
pages = "6278",
abstract =
"We show that infinite objects can be constructively understood
without the consideration of partial elements, or greatest fixed
points, through the explicit consideration of proof objects. We
present then a proof system based on these explanations. According to
this analysis, the proof expressions should have the same structure
as the program expressions of a pure functional lazy language:
variable, constructor, application, abstraction, case expressions,
and local let expressions.",
paper = "Coqu93.pdf"
}
\end{chunk}
\index{Barthe, Gilles}
\begin{chunk}{axiom.bib}
@article{Bart95,
author = "Barthe, Gilles",
title = {{Implicit Coercions in Type Systems}},
journal = "LNCS",
volume = "1158",
year = "1995",
pages = "115",
abstract =
"We propose a notion of pure type system with implicit coercions. In
our framework, judgements are extended with a context of coercions Δ
and the application rule is modified so as to allow coercions to be
left implicit. The setting supports multiple inheritance and can be
applied to all type theories with $\Pi$types. One originality of our work
is to propose a computational interpretation for implicit
coercions. In this paper, we demonstrate how this interpretation
allows a strict control on the logical properties of pure type systems
with implicit coecions.",
paper = "Bart95.pdf"
}
\end{chunk}
\index{Berger, U.}
\index{Schwichtenberg, H.}
\begin{chunk}{axiom.bib}
@article{Berg95,
author = "Berger, U. and Schwichtenberg, H.",
title = {{The Greatest Common Divisor: A Case Study for Program
Extraction from Classical Proofs}},
journal = "LNCS",
volume = "1158",
year = "1995",
pages = "3646",
paper = "Berg95.pdf"
}
\end{chunk}
\index{Magaud, Nicolas}
\index{Bertot, Yves}
\begin{chunk}{axiom.bib}
@article{Maga00,
author = "Magaud, Nicolas and Bertot, Yves",
title = {{Changing Data Structures in Type Theory: A Study of
Natural Numbers}},
journal = "LNCS",
volume = "2277",
pages = "181196",
year = "2000",
abstract =
"In typetheory based proof systems that provide inductive
structures, computation tools are automatically associated to
inductive definitions. Choosing a particular representation for a
given concept has a strong influence on proof structure. We
propose a method to make the change from one representation to
another easier, by systematically translating proofs from one
context to another. We show how this method works by using it on
natural numbers, for which a unary representation (based on Peano
axioms) and abinary representation are available. This method
leads to an automatic translation tool that we have implemented in
Coq and successfully applied to several arithmetical theorems.",
paper = "Maga00.pdf"
}
\end{chunk}
\index{Bailey, Anthony}
\begin{chunk}{axiom.bib}
@article{Bail96,
author = "Bailey, Anthony",
title = {{Coercion Synthesis in Computer Implementations of
TypeTheoretic Frameworks}},
journal = "LNCS",
year = "1996",
pages = "927",
abstract =
"A coercion is a function that acts on a representation of some object
in order to alter its type. The idea is that although applying a
coercion to an object changes its type, the result still represents
the ``same'' abject in some sense; perhaps it is some essential
underlying part of the original object, or a different representation
of that object. This paper examines some of the issues involved in
the computer implementation of systems that allow a user to define
coercions that may then be left implicit in the syntax of expressions
and synthesised automatically. From a typetheoretic perspective,
coercions are often left implicit in mathematical texts, so they can
be used to improve the readability of a formalisation, and to
implement other tricks of syntax if so desired.",
paper = "Bail96.pdf"
}
\end{chunk}
\index{Barras, Bruno}
\begin{chunk}{axiom.bib}
@article{Barr96,
author = "Barras, Bruno",
title = {{Verification of the Interface of a Small Proof System in Coq}},
journal = "LNCS",
volume = "1512",
pages = "2845",
year = "1996",
abstract =
"This article describes the formalization of the interface of a
proofchecker. The latter is based on a kernel consisting of
typechecking functions for the Calculus of Constructions, but it
seems the ideas can generalize to other type systems, as fax as they
axe based on the proofs asterms principle. We suppose that the
metatheory of the corresponding type system is proved (up to type
decidability). We specify and certify the toplevel loop, the system
invariant, and the error messages.",
paper = "Barr96.pdf"
}
\end{chunk}
\index{Dowek, Gilles}
\begin{chunk}{axiom.bib}
@article{Dowe96,
author = "Dowek, Gilles",
title = {{A TypeFree Formalization of Mathematics Where Proofs are
Objects}},
journal = "LNCS",
volume = "1512",
year = "1996",
pages = "88111",
abstract =
"We present a firstorder typefree axiomatization of mathematics
where proofs are objects in the sense of HeytingKolmogorov functional
interpretation. The consistency of this theory is open.",
paper = "Dowe96.pdf"
}
\end{chunk}
\index{Harrison, John}
\begin{chunk}{axiom.bib}
@article{Harr06,
author = "Harrison, John",
title = {{Proof Style}},
journal = "LNCS",
volume = "1512",
year = "2006",
pages = "154172",
abstract =
"We are concerned with how computer theorem provers should expect
users to communicate proofs to them. There are many stylistic choices
that still allow the machine to generate a completely formal proof
object. The most obvious choice is the amount of guidance required
from the user, or from the machine perspective, the degree of
automation provided. But another important consideration, which we
consider particularly significant, is the bias towards a
'procedural' or 'declarative' proof style. We will explore this
choice in depth, and discuss the strengths and weaknesses of
declarative and procedural styles for proofs in pure mathematics and
for verification applications. We conclude with a brief summary of
our own experiments in trying to combine both approaches.",
paper = "Harr06.pdf"
}
\end{chunk}
\index{Jones, Alex}
\index{Luo, Zhaohui}
\index{Soloviev, Sergei}
\begin{chunk}{axiom.bib}
@article{Jone96,
author = "Jones, Alex and Luo, Zhaohui and Soloviev, Sergei",
title = {{Some Algorithmic and ProofTheoretical Aspects of
Coercive Subtyping}},
journal = "LNCS",
volume = "1512",
year = "1996",
pages = "173195",
abstract =
"Coercive subtyping offers a conceptually simple but powerful
framework to understand subtyping and subset relationships in type
theory. In this paper we study some of its prooftheoretic and
computational properties.",
paper = "Jone96.pdf"
}
\end{chunk}
\index{Naraschewski, Wolfgang}
\index{Nipkow, Tobias}
\begin{chunk}{axiom.bib}
@article{Nara99,
author = "Naraschewski, Wolfgang and Nipkow, Tobias",
title = {{Type Inference Verified: Algorithm W in Isabelle/HOL}},
journal = "LNCS",
volume = "1512",
year = "1999",
pages = "317332",
paper = "Nara99.pdf"
}
\end{chunk}
\index{Constable, R.L.}
\index{Knoblock, T.B.}
\index{Gates, J.L.}
\begin{chunk}{axiom.bib}
@article{Cons85a,
author = "Constable, R.L. and Knoblock, T.B. and Gates, J.L.",
title = {{Writing Programs that Construct Proofs}},
journal = "J. of Automated Reasoning",
volume = "1",
number = "3",
pages = "285326",
year = "1985",
abstract =
"When we learn mathematics, we learn more than definitions and
theorems. We learn techniques of proof. In this paper, we describe
a particular way to express these techniques and incorporate them
into formal theories and into computer systems used to build such
theories. We illustrate the methods as they were applied in the
$\lambda$PRL system, essentially using the ML programming
language from Edinburgh LCF [23] as the formalised
metalanguage. We report our experience with such an approach
emphasizing the ideas that go beyond the LCF work, such as
transformation tactics and special purpose reasoners. We also show
how the validity of tactics can be guaranteed. The introduction
places the work in historical context and the conclusion briefly
describes plans to carry the methods further. The majority of the
paper presents the $\lambda$PRL approach in detail.",
paper = "Cons85a.pdf"
}
\end{chunk}
\index{Trybulec, Zinaida}
\index{Swieczkowska, Halina}
\begin{chunk}{axiom.bib}
@article{Tryb92,
author = "Trybulec, Zinaida and Swieczkowska, Halina",
title = {{Some Remarks on The Language of Mathematical Texts}},
journal = "Studies in Logic, Grammar and Rhetoric",
volume = "10/11",
pages = "103124",
year = "1992",
paper = "Tryb92.pdf"
}
\end{chunk}
\index{Traytel, Bmytro}
\begin{chunk}{axiom.bib}
@misc{Tray10,
author = "Traytel, Bmytro",
title = {{Extensions of a Type Inference Algorithm with Coerce Subtyping}},
school = "Der Technischen Universitat Munchen",
year = "2010",
abstract =
"Subtyping with coercion semantics allows a type inference system to
correct some illtyped programs by the automatic insertion of
implicit type conversions at runtime. This simplifies programmer’s
life but has its price: the general typability problem for given base
type subtype dependencies is NPcomplete. Nevertheless, if the given
coercions define an order on types with certain properties, the
problem behaves in a sane way in terms of complexity. This thesis
presents an algorithm that can be used to extend HindleyMilner type
inference with coercive subtyping assuming a given partial order on
base types. Especially, we discuss restrictions on the subtype
dependencies that are necessary to achieve an efficient
implementation. Examples of problems that occur if these restrictions
are not met are given. The result of these considerations is that the
algorithm is complete if the given base type poset is a disjoint union
of lattices. Furthermore, the interaction of subtyping with type
classes is addressed. The algorithm that is extended to deal with
type classes requires even a stronger restriction to assure
completeness. An MLimplementation of the presented algorithm is used
in the generic proof assistant Isabelle.",
paper = "Tray10.pdf"
}
\end{chunk}
\index{Luo, Zhaohui}
\index{Soloviev, Sergei}
\begin{chunk}{axiom.bib}
@article{Luox99,
author = "Luo, Zhaohui and Soloviev, Sergei",
title = {{Dependent Coercions}},
journal = "Electr. Notes Theor. Comput. Sci.",
volume = "29",
year = "1999",
pages = "152168",
abstract =
"A notion of dependent coercion is introduced and studied in the
context of depen dent type theories. It extends our earlier work on
coercive subtyping into a uniform framework which increases the
expressive power with new applications. A dependent coercion
introduces a subtyping relation between a type and a family of types
in that an object of the type is mapped into one of the types in the
family. We present the formal framework, discuss its metatheory, and
consider applications such as its use in functional programming with
dependent types.",
paper = "Luox99.pdf"
}
\end{chunk}

books/axiom.bib  515 +++++++++++++++++++++++
books/bookvolbib.pamphlet  635 ++++++++++++++++++++++++++++
changelog  2 +
patch  894 +++++++++++++++++++++++
src/axiomwebsite/patches.html  2 +
5 files changed, 1652 insertions(+), 396 deletions()
diff git a/books/axiom.bib b/books/axiom.bib
index 7c9c749..2404f2b 100644
 a/books/axiom.bib
+++ b/books/axiom.bib
@@ 6917,6 +6917,72 @@ paper = "Brea89.pdf"
paper = "Yous04.pdf"
}
+@article{Cons85a,
+ author = "Constable, R.L. and Knoblock, T.B. and Gates, J.L.",
+ title = {{Writing Programs that Construct Proofs}},
+ journal = "J. of Automated Reasoning",
+ volume = "1",
+ number = "3",
+ pages = "285326",
+ year = "1985",
+ abstract =
+ "When we learn mathematics, we learn more than definitions and
+ theorems. We learn techniques of proof. In this paper, we describe
+ a particular way to express these techniques and incorporate them
+ into formal theories and into computer systems used to build such
+ theories. We illustrate the methods as they were applied in the
+ $\lambda$PRL system, essentially using the ML programming
+ language from Edinburgh LCF [23] as the formalised
+ metalanguage. We report our experience with such an approach
+ emphasizing the ideas that go beyond the LCF work, such as
+ transformation tactics and special purpose reasoners. We also show
+ how the validity of tactics can be guaranteed. The introduction
+ places the work in historical context and the conclusion briefly
+ describes plans to carry the methods further. The majority of the
+ paper presents the $\lambda$PRL approach in detail.",
+ paper = "Cons85a.pdf"
+}
+
+@article{Tryb92,
+ author = "Trybulec, Zinaida and Swieczkowska, Halina",
+ title = {{Some Remarks on The Language of Mathematical Texts}},
+ journal = "Studies in Logic, Grammar and Rhetoric",
+ volume = "10/11",
+ pages = "103124",
+ year = "1992",
+ link = "\url{http://mizar.org/trybulec65/5.pdf}",
+ paper = "Tryb92.pdf"
+}
+
+@incollection{Soze06,
+ author = "Sozeau, Matthieu",
+ title = {{Subset Coercions in Coq}},
+ booktitle = "TYPES: Int. Workshop on Types for Proofs and Programs",
+ journal = "LNCS",
+ volume = "4502",
+ pages = "237252",
+ year = "2006",
+ abstract =
+ "We propose a new language for writing programs with dependent types
+ on top of the Coq proof assistant. This language permits to establish
+ a phase distinction between writing and proving algorithms in the Coq
+ environment. Concretely, this means allowing to write algorithms as
+ easily as in a practical functional programming language whilst giving
+ them as rich a specification as desired and proving that the code
+ meets the specification using the whole Coq proof apparatus. This is
+ achieved by extending conversion to an equivalence which relates
+ types and subsets based on them, a technique originating from the
+ ``Predicate subtyping'' featureof PVS and following mathematical
+ convention. The typing judgements can be translated to the Calculus of
+ (Co)Inductive Constructions (Cic) by means of an interpretation
+ which inserts coercions at the appropriate places.These coercions
+ can contain existential variables representing the propositional
+ parts of the final term, corresponding to proof obligations (or
+ PVS typechecking conditions). A prototype implementation of this
+ process is integrated with the Coq environment.",
+ paper = "Soze06.pdf"
+}
+
@article{Aban16,
author = "Abanades, M. and Botana, F. and Kovacs, Z. and Recio, T. and
SolyomGecse, C.",
@@ 8621,6 +8687,25 @@ paper = "Brea89.pdf"
paper = "Coqu86.pdf"
}
+@article{Coqu93,
+ author = "Coquand, Thierry",
+ title = {{Infinite Objects in Type Theory}},
+ journal = "LNCS",
+ volume = "806",
+ year = "1993",
+ pages = "6278",
+ abstract =
+ "We show that infinite objects can be constructively understood
+ without the consideration of partial elements, or greatest fixed
+ points, through the explicit consideration of proof objects. We
+ present then a proof system based on these explanations. According to
+ this analysis, the proof expressions should have the same structure
+ as the program expressions of a pure functional lazy language:
+ variable, constructor, application, abstraction, case expressions,
+ and local let expressions.",
+ paper = "Coqu93.pdf"
+}
+
@article{Coqu96,
author = "Coquand, Thierry and Dybjer, Peter",
title = {{Intuitionistic Model Constructions and Normalization Proofs}},
@@ 10232,7 +10317,7 @@ paper = "Brea89.pdf"
@inproceedings{Koun90,
author = "Kounalis, Emmanuel and Rusinowitch, Michael",
 titlexo = {{A Proof System for Conditional Algebraic Specifications}},
+ title = {{A Proof System for Conditional Algebraic Specifications}},
booktitle = "Conference Conditional and Typed Rewriting Systems",
year = "1990",
abstract =
@@ 11365,7 +11450,7 @@ paper = "Brea89.pdf"
program can be extracted. Since some information cannot automatically
be inferred, we show how to annotate the program by specifying some of
its parts in order to guide the search for the proof.",
 paper = "Pare93.ps"
+ paper = "Pare93.pdf"
}
@techreport{Pare94,
@@ 12773,6 +12858,7 @@ paper = "Brea89.pdf"
journal = "LNCS",
volume = "958",
pages = "209223",
+ year = "1994",
abstract =
"We present extended term rewriting systems as a means to describe a
simplification relation for an equational specification with a
@@ 19199,6 +19285,7 @@ paper = "Brea89.pdf"
journal = "LNCS",
volume = "535",
pages = "243255",
+ year = "1991",
abstract =
"The paper presents an overview of the research achievements on issues
of common interest for Symbolic Computation and Artificial
@@ 26166,7 +26253,7 @@ paper = "Brea89.pdf"
@article{Igar75,
author = "Igarashi, Shigeru and London, Ralph L. and Luckham, David C.",
 titile = {{Automatic Program Verification I: A Logical Basis and Its
+ title = {{Automatic Program Verification I: A Logical Basis and Its
Implementation}},
journal = "Acta Informatica",
volume = "4",
@@ 32066,6 +32153,29 @@ paper = "Brea89.pdf"
paper = "Avig17a.pdf"
}
+@article{Bail96,
+ author = "Bailey, Anthony",
+ title = {{Coercion Synthesis in Computer Implementations of
+ TypeTheoretic Frameworks}},
+ journal = "LNCS",
+ year = "1996",
+ pages = "927",
+ abstract =
+ "A coercion is a function that acts on a representation of some object
+ in order to alter its type. The idea is that although applying a
+ coercion to an object changes its type, the result still represents
+ the ``same'' abject in some sense; perhaps it is some essential
+ underlying part of the original object, or a different representation
+ of that object. This paper examines some of the issues involved in
+ the computer implementation of systems that allow a user to define
+ coercions that may then be left implicit in the syntax of expressions
+ and synthesised automatically. From a typetheoretic perspective,
+ coercions are often left implicit in mathematical texts, so they can
+ be used to improve the readability of a formalisation, and to
+ implement other tricks of syntax if so desired.",
+ paper = "Bail96.pdf"
+}
+
@misc{Bake14,
author = "Baker, Martin",
title = {{Axiom Architecture}},
@@ 32074,6 +32184,45 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@article{Barr96,
+ author = "Barras, Bruno",
+ title = {{Verification of the Interface of a Small Proof System in Coq}},
+ journal = "LNCS",
+ volume = "1512",
+ pages = "2845",
+ year = "1996",
+ abstract =
+ "This article describes the formalization of the interface of a
+ proofchecker. The latter is based on a kernel consisting of
+ typechecking functions for the Calculus of Constructions, but it
+ seems the ideas can generalize to other type systems, as fax as they
+ axe based on the proofs asterms principle. We suppose that the
+ metatheory of the corresponding type system is proved (up to type
+ decidability). We specify and certify the toplevel loop, the system
+ invariant, and the error messages.",
+ paper = "Barr96.pdf"
+}
+
+@article{Bart95,
+ author = "Barthe, Gilles",
+ title = {{Implicit Coercions in Type Systems}},
+ journal = "LNCS",
+ volume = "1158",
+ year = "1995",
+ pages = "115",
+ abstract =
+ "We propose a notion of pure type system with implicit coercions. In
+ our framework, judgements are extended with a context of coercions Δ
+ and the application rule is modified so as to allow coercions to be
+ left implicit. The setting supports multiple inheritance and can be
+ applied to all type theories with $\Pi$types. One originality of our
+ work is to propose a computational interpretation for implicit
+ coercions. In this paper, we demonstrate how this interpretation
+ allows a strict control on the logical properties of pure type systems
+ with implicit coecions.",
+ paper = "Bart95.pdf"
+}
+
@article{Bart72,
author = "Barton, D.R. and Fitch, John P.",
title = {{A Review of Algebraic Manipulative Programs and their
@@ 32142,6 +32291,17 @@ paper = "Brea89.pdf"
paper = "Beez15.pdf"
}
+@article{Berg95,
+ author = "Berger, U. and Schwichtenberg, H.",
+ title = {{The Greatest Common Divisor: A Case Study for Program
+ Extraction from Classical Proofs}},
+ journal = "LNCS",
+ volume = "1158",
+ year = "1995",
+ pages = "3646",
+ paper = "Berg95.pdf"
+}
+
@misc{Bern85,
author = "Berndt, B.C.",
title = {{Ramanujan's Notebooks, Part I}},
@@ 32247,6 +32407,34 @@ paper = "Brea89.pdf"
paper = "Boge77.pdf"
}
+@article{Bove02,
+ author = "Bove, Ana",
+ title = {{General Recursion in Type Theory}},
+ journal = "LNCS",
+ volume = "2646",
+ pages = "3958",
+ year = "2002",
+ abstract =
+ "In this work, a method to formalise general recursive algorithms in
+ constructive type theory is presented throughout examples. The method
+ separates the computational and logical parts of the definitions. As
+ a consequence, the resulting typetheoretic algorithms are clear,
+ compact and easy to understand. They are as simple as their
+ equivalents in a functional programming language, where there is no
+ restriction on recursive calls. Given a general recursive algorithm,
+ the method consists in defining an inductive specialpurpose
+ accessibility predicate that characterises the inputs on which the
+ algorithm terminates. The typetheoretic version of the algorithm can
+ then be defined by structural recursion on the proof that the input
+ values satisfy this predicate. When formalising nested algorithms, the
+ specialpurpose accessibility predicate and the typetheoretic version
+ of the algorithm must be defined simultaneously because they depend on
+ each other. Since the method separates the computational part from
+ the logical part of a definition, formalising partial functions
+ becomes also possible.",
+ paper = "Bove02.pdf"
+}
+
@inproceedings{Brad86,
author = "Bradford, Russell J. and Hearn, Anthony C. and Padget, Julian and
Schrufer, Eberhard",
@@ 32665,6 +32853,24 @@ paper = "Brea89.pdf"
link = "\url{https://www.w3.org/TR/MathML3/}"
}
+@article{Carl02,
+ author = "Carlstrom, Jesper",
+ title = {{Subsets, Quotients, and Partial Functions in MartinL\"of's
+ Type Theory}},
+ journal = "LNCS",
+ volume = "2646",
+ year = "2002",
+ pages = "7894",
+ abstract =
+ "We treat subsets, equivalence relations, and partial functions,
+ with subsets as propositional functions .In order for these three
+ notions to work well together, we propose some changes to the theory
+ of subsets as propositional functions .The method used is not to make
+ any changes to the type theory itself, but to view the new concepts as
+ defined ones.",
+ paper = "Carl02.pdf"
+}
+
@book{Char92,
author = "Char, B.W. and Geddes, K.O. and Gonnet, G.H. and Leong, B.L.
and Monagan, M.B. and Watt, S.M.",
@@ 32763,6 +32969,28 @@ paper = "Brea89.pdf"
keywords = "CASProof"
}
+@article{Coen07,
+ author = "Coen, Claudio Sacerdoti and Tassi, Enrico",
+ title = {{Working with Mathematical Structures in Type Theory}},
+ journal = "LNCS",
+ volume = "4941",
+ year = "2007",
+ pages = "157172",
+ abstract =
+ "We address the problem of representing mathematical structures in a
+ proof assistant which: 1) is based on a type theory with depen dent
+ types, telescopes and a computational version of Leibniz equality; 2)
+ implements coercive subtyping, accepting multiple coherent paths
+ between type families; 3) implements a restricted form of higher order
+ unification and type reconstruction. We show how to exploit the
+ previous quite common features to reduce the ``syntactic'' gap between
+ pen and paper and formalised algebra. However, to reach our goal we need
+ to propose unification and type reconstruction heuristics that are
+ slightly different from the ones usually implemented. We have
+ implemented them in Matita.",
+ paper = "Coen07.pdf"
+}
+
@book{Cohn65,
author = "Cohn, Paul Moritz",
title = {{Universal Algebra}},
@@ 32803,6 +33031,35 @@ paper = "Brea89.pdf"
paper = "Colm90.pdf"
}
+@article{Coqu98,
+ author = "Coquand, Thierry and Persson, Henrik",
+ title = {{Groebner Bases in Type Theory}},
+ journal = "LNCS",
+ volume = "1657",
+ year = "1998",
+ pages = "3346",
+ abstract =
+ "We describe how the theory of Groebner bases, an important part
+ of computational algebra, can be developed within Martin Lof’s
+ type theory. In particular, we aim for an integrated development
+ of the algorithms for computing Groebner bases: we want to prove,
+ constructively in type theory, the existence of Groebner bases and
+ from such proofs extract the algorithms. Our main contribution is
+ a reformulation of the standard theory of Groebner bases which
+ uses generalised inductive definitions. We isolate the main
+ non–constructive part, a minimal bad sequence argument, and use
+ the open induction principle [Rao88,Coq92] to interpret it by
+ induction. This leads to short constructive proofs of Dickson’s
+ lemma and Hilbert’s basis theorem, which are used to give an
+ integrated development of Buchberger’s algorithm. An important
+ point of this work is that the elegance and brevity of the
+ original proofs are maintained while the new proofs also have a
+ direct constructive content. In the appendix we present a
+ computer formalisation of Dickson’s lemma and an abstract
+ existence proof of Groebner bases.",
+ paper = "Coqu98.pdf"
+}
+
@article{Corl92,
author = "Corless, Robert M. and Jeffrey, David J.",
title = {{Well, it isn't quite that simple}},
@@ 32987,6 +33244,21 @@ paper = "Brea89.pdf"
paper = "Dowe00.pdf"
}
+@article{Dowe96,
+ author = "Dowek, Gilles",
+ title = {{A TypeFree Formalization of Mathematics Where Proofs are
+ Objects}},
+ journal = "LNCS",
+ volume = "1512",
+ year = "1996",
+ pages = "88111",
+ abstract =
+ "We present a firstorder typefree axiomatization of mathematics
+ where proofs are objects in the sense of HeytingKolmogorov functional
+ interpretation. The consistency of this theory is open.",
+ paper = "Dowe96.pdf"
+}
+
@misc{Duns01,
author = "Dunstan, M.N. and Gottliebsen, H. and Kelsey, T.W. and
Martin, U.",
@@ 33259,6 +33531,28 @@ paper = "Brea89.pdf"
paper = "Fevr98.pdf"
}
+@article{Fill98,
+ author = "Filliatre, JeanChristophe",
+ title = {{Proof of Imperative Programs in Type Theory}},
+ journal = "LNCS",
+ volume = "1657",
+ year = "1998",
+ pages = "7892",
+ abstract =
+ "We present a new approach to certifying functional programs with
+ imperative aspects, in the context of Type Theory. The key is a
+ functional translation of imperative programs, based on a combination
+ of the type and effect discipline and monads. Then an incomplete proof
+ of the specification is built in the Type Theory, whose gaps would
+ corre spond to proof obligations. On sequential imperative programs,
+ we get the same proof obligations as those given by FloydHoare
+ logic. Compared to the latter, our approach also includes functional
+ constructions in a straightforward way. This work has been
+ implemented in the Coq Proof Assistant and applied on nontrivial
+ examples.",
+ paper = "Fill98.pdf"
+}
+
@misc{Fitc74,
author = "Fitch, J.P.",
title = {{CAMAL Users Manual}},
@@ 33351,6 +33645,7 @@ paper = "Brea89.pdf"
volume = "3702",
pages = "123137",
isbn = "3540289313",
+ year = "1985",
abstract =
"We extend classical firstorder logic with subtyping by type
predicates and type coercion. Type predicates assert that the value of
@@ 33539,6 +33834,30 @@ paper = "Brea89.pdf"
month = "Septembre"
}
+@article{Haft06,
+ author = "Haftmann, Florian and Wenzel, Makarius",
+ title = {{Constructive Type Classes in Isabelle}},
+ journal = "LNCS",
+ volume = "4502",
+ year = "2006",
+ abstract =
+ "We reconsider the wellknown concept of Haskellstyle type classes
+ within the logical framework of Isabelle. So far, axiomatic type
+ classes in Isabelle merely account for the logical aspect as
+ predicates over types, while the opera tional part is only a
+ convention based on raw overloading. Our more elaborate approach to
+ constructive type classes provides a seamless integration with
+ Isabelle locales, which are able to manage both operations and logical
+ properties uniformly. Thus we combine the convenience of type
+ classes and the flexibility of locales. Furthermore, we construct
+ dictionary terms derived from notions of the type system. This
+ additional internal structure provides satisfactory foundations of
+ type classes, and supports further applications, such as code
+ generation and export of theories and theorems to environments without
+ type classes.",
+ paper = "Haft06.pdf"
+}
+
@inproceedings{Haml02,
author = "Hamlet, Dick",
title = {{Continuity in Software Systems}},
@@ 33547,6 +33866,29 @@ paper = "Brea89.pdf"
year = "2002",
}
+@article{Harr06,
+ author = "Harrison, John",
+ title = {{Proof Style}},
+ journal = "LNCS",
+ volume = "1512",
+ year = "2006",
+ pages = "154172",
+ abstract =
+ "We are concerned with how computer theorem provers should expect
+ users to communicate proofs to them. There are many stylistic choices
+ that still allow the machine to generate a completely formal proof
+ object. The most obvious choice is the amount of guidance required
+ from the user, or from the machine perspective, the degree of
+ automation provided. But another important consideration, which we
+ consider particularly significant, is the bias towards a
+ 'procedural' or 'declarative' proof style. We will explore this
+ choice in depth, and discuss the strengths and weaknesses of
+ declarative and procedural styles for proofs in pure mathematics and
+ for verification applications. We conclude with a brief summary of
+ our own experiments in trying to combine both approaches.",
+ paper = "Harr06.pdf"
+}
+
@inproceedings{Harr07,
author = "Harrison, John",
title = {{A Short Survey of Automated Reasoning}},
@@ 33835,6 +34177,22 @@ paper = "Brea89.pdf"
number = "3",
}
+@article{Jone96,
+ author = "Jones, Alex and Luo, Zhaohui and Soloviev, Sergei",
+ title = {{Some Algorithmic and ProofTheoretical Aspects of
+ Coercive Subtyping}},
+ journal = "LNCS",
+ volume = "1512",
+ year = "1996",
+ pages = "173195",
+ abstract =
+ "Coercive subtyping offers a conceptually simple but powerful
+ framework to understand subtyping and subset relationships in type
+ theory. In this paper we study some of its prooftheoretic and
+ computational properties.",
+ paper = "Jone96.pdf"
+}
+
@phdthesis{Kalk91,
author = "Kalkbrener, M.",
title = {{Three contributions to elimination theory}},
@@ 34091,6 +34449,25 @@ paper = "Brea89.pdf"
keywords = "axiomref"
}
+@article{Kies03,
+ author = "Kiessling, Robert and Luo, Zhaohui",
+ title = {{Coercions in HindleyMilner Systems}},
+ journal = "LNCS",
+ volume = "3085",
+ year = "2003",
+ abstract =
+ "Coercive subtyping is a theory of abbreviation for dependent type
+ theories. In this paper, we incorporate the idea of coercive subtyping
+ into the traditional HindleyMilner type systems in functional
+ programming languages. This results in a typing system with coercions,
+ an extension of the HindleyMilner type system. A type inference
+ algorithm is developed and shown to be sound and complete with respect
+ to the typing system. A notion of derivational coherence is developed
+ to deal with the problem of ambiguity and the corresponding type
+ inference algorithm is shown to be sound and complete.",
+ paper = "Kies03.pdf"
+}
+
@book{Knut92,
author = "Knuth, Donald E.",
title = {{Literate Programming}},
@@ 34505,6 +34882,26 @@ paper = "Brea89.pdf"
isbn = "9780124599406"
}
+@article{Luox99,
+ author = "Luo, Zhaohui and Soloviev, Sergei",
+ title = {{Dependent Coercions}},
+ journal = "Electr. Notes Theor. Comput. Sci.",
+ volume = "29",
+ year = "1999",
+ pages = "152168",
+ abstract =
+ "A notion of dependent coercion is introduced and studied in the
+ context of depen dent type theories. It extends our earlier work on
+ coercive subtyping into a uniform framework which increases the
+ expressive power with new applications. A dependent coercion
+ introduces a subtyping relation between a type and a family of types
+ in that an object of the type is mapped into one of the types in the
+ family. We present the formal framework, discuss its metatheory, and
+ consider applications such as its use in functional programming with
+ dependent types.",
+ paper = "Luox99.pdf"
+}
+
@book{Lutz90,
author = "Lutzen, Jesper",
title = {{Joseph Liouville. 18091882: Master of Pure and Applied
@@ 34524,6 +34921,29 @@ paper = "Brea89.pdf"
paper = "Lutz90a.pdf"
}
+@article{Maga00,
+ author = "Magaud, Nicolas and Bertot, Yves",
+ title = {{Changing Data Structures in Type Theory: A Study of
+ Natural Numbers}},
+ journal = "LNCS",
+ volume = "2277",
+ pages = "181196",
+ year = "2000",
+ abstract =
+ "In typetheory based proof systems that provide inductive
+ structures, computation tools are automatically associated to
+ inductive definitions. Choosing a particular representation for a
+ given concept has a strong influence on proof structure. We
+ propose a method to make the change from one representation to
+ another easier, by systematically translating proofs from one
+ context to another. We show how this method works by using it on
+ natural numbers, for which a unary representation (based on Peano
+ axioms) and abinary representation are available. This method
+ leads to an automatic translation tool that we have implemented in
+ Coq and successfully applied to several arithmetical theorems.",
+ paper = "Maga00.pdf"
+}
+
@article{Maga08,
author = "Magaud, Nicolas and Narboux, Julien and Schreck, Pascal",
title = {{Formalizing Projective Plane Geometry in Coq}},
@@ 34856,6 +35276,16 @@ paper = "Brea89.pdf"
paper = "Muld97.pdf"
}
+@article{Nara99,
+ author = "Naraschewski, Wolfgang and Nipkow, Tobias",
+ title = {{Type Inference Verified: Algorithm W in Isabelle/HOL}},
+ journal = "LNCS",
+ volume = "1512",
+ year = "1999",
+ pages = "317332",
+ paper = "Nara99.pdf"
+}
+
@article{Naud98,
author = "Naudin, Patrice and Quitte, Claude",
title = {{Univariate polynomial factorization over finite fields}},
@@ 34914,7 +35344,7 @@ paper = "Brea89.pdf"
paper = "Neup12.pdf"
}
@article{Meup13a,
+@article{Neup13a,
author = "Neuper, Walther",
title = {{On the Emergence of TPbased Educational Math
Assistants}},
@@ 34968,6 +35398,20 @@ paper = "Brea89.pdf"
a senior or graduate AI course, or for individual study."
}
+@article{Nipk02,
+ author = "Nipkow, Tobias",
+ title = {{Structured Proofs in Isar/HOL}},
+ journal = "LNCS",
+ volume = "2646",
+ year = "2002",
+ pages = "259278",
+ abstract =
+ "Isar is an extension of the theorem prover Isabelle with a language
+ for writing humanreadable structured proofs. This paper is an
+ introduction to the basic constructs of this language.",
+ paper = "Nipk02.pdf"
+}
+
@misc{OCAM14,
author = "unknown",
title = {{The OCAML website}},
@@ 35002,7 +35446,7 @@ paper = "Brea89.pdf"
@article{Paul90,
author = "Paulson, Lawrence C.",
title = {{A Formulation of the Simple Theory of Types (for
 Isabelle}}},
+ Isabelle)}},
journal = "LNCS",
volume = "417",
pages = "246274",
@@ 35126,6 +35570,13 @@ paper = "Brea89.pdf"
paper = "Phil02.pdf"
}
+@misc{Pier17,
+ author = "Pierce, Benjamin",
+ title = "DeepSpec Summer School, Coq Intensive, Part 1 (July 13,2017)",
+ year = "2017",
+ link = "\url{https://www.youtube.com/watch?v=jG61w5pOc2A}"
+}
+
@inproceedings{Popo09,
author = "Popov, Nikolaj and Jebelean, Tudor",
title = {{Functional Program Verification in Theorema Soundness and
@@ 35677,6 +36128,35 @@ paper = "Brea89.pdf"
paper = "Thur94.pdf"
}
+@misc{Tray10,
+ author = "Traytel, Bmytro",
+ title = {{Extensions of a Type Inference Algorithm with Coerce Subtyping}},
+ school = "Der Technischen Universitat Munchen",
+ link = "\url{https://www21.in.tum.de/~traytel/bscthesis.pdf}",
+ year = "2010",
+ abstract =
+ "Subtyping with coercion semantics allows a type inference system to
+ correct some illtyped programs by the automatic insertion of
+ implicit type conversions at runtime. This simplifies programmer’s
+ life but has its price: the general typability problem for given base
+ type subtype dependencies is NPcomplete. Nevertheless, if the given
+ coercions define an order on types with certain properties, the
+ problem behaves in a sane way in terms of complexity. This thesis
+ presents an algorithm that can be used to extend HindleyMilner type
+ inference with coercive subtyping assuming a given partial order on
+ base types. Especially, we discuss restrictions on the subtype
+ dependencies that are necessary to achieve an efficient
+ implementation. Examples of problems that occur if these restrictions
+ are not met are given. The result of these considerations is that the
+ algorithm is complete if the given base type poset is a disjoint union
+ of lattices. Furthermore, the interaction of subtyping with type
+ classes is addressed. The algorithm that is extended to deal with
+ type classes requires even a stronger restriction to assure
+ completeness. An MLimplementation of the presented algorithm is used
+ in the generic proof assistant Isabelle.",
+ paper = "Tray10.pdf"
+}
+
@misc{Tryb02,
author = "Trybulec, Andrzej",
title = {{Towards Practical Formalizaiton of Mathematics}},
@@ 35847,6 +36327,31 @@ paper = "Brea89.pdf"
link = "\url{http://www.weitz.de/hunchentoot}"
}
+@article{Wied03,
+ author = "Wiedijk, Freek",
+ title = {{Formal Proof Sketches}},
+ journal = "LNCS",
+ volume = "3085",
+ year = "2003",
+ pages = "378393",
+ abstract =
+ "Formalized mathematics currently does not look much like informal
+ mathematics. Also, formalizing mathematics currently seems far too
+ much work to be worth the time of the working mathematician. To
+ address both of these problems we introduce the notion of a formal
+ proof sketch . This is a proof representation that is in between a
+ fully checkable formal proof and a statement without any proof at
+ all. Although a formal proof sketch is too high level to be checkable
+ by computer, it has a precise notion of correctness (hence the
+ adjective formal ). We will show through examples that formal proof
+ sketches can closely mimic already existing mathematical
+ proofs. Therefore, although a formal proof sketch contains gaps in
+ the reasoning from a formal point of view (which is why we call it a
+ sketch ), a mathematician probably would call such a text just a
+ ‘proof’.",
+ paper = "Wied03.pdf"
+}
+
@misc{Wiki14a,
author = "ProofWiki",
title = {{Euclidean Algorithm}},
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 987e071..d086a67 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 9444,7 +9444,93 @@ when shown in factored form.
\end{chunk}
\section{Proving SAxiom Correct} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\section{Proving Axiom Correct  The Project} %%%%%%%%%%%%%%%%%%%%
+
+\index{Constable, R.L.}
+\index{Knoblock, T.B.}
+\index{Gates, J.L.}
+\begin{chunk}{axiom.bib}
+@article{Cons85a,
+ author = "Constable, R.L. and Knoblock, T.B. and Gates, J.L.",
+ title = {{Writing Programs that Construct Proofs}},
+ journal = "J. of Automated Reasoning",
+ volume = "1",
+ number = "3",
+ pages = "285326",
+ year = "1985",
+ abstract =
+ "When we learn mathematics, we learn more than definitions and
+ theorems. We learn techniques of proof. In this paper, we describe
+ a particular way to express these techniques and incorporate them
+ into formal theories and into computer systems used to build such
+ theories. We illustrate the methods as they were applied in the
+ $\lambda$PRL system, essentially using the ML programming
+ language from Edinburgh LCF [23] as the formalised
+ metalanguage. We report our experience with such an approach
+ emphasizing the ideas that go beyond the LCF work, such as
+ transformation tactics and special purpose reasoners. We also show
+ how the validity of tactics can be guaranteed. The introduction
+ places the work in historical context and the conclusion briefly
+ describes plans to carry the methods further. The majority of the
+ paper presents the $\lambda$PRL approach in detail.",
+ paper = "Cons85a.pdf"
+}
+
+\end{chunk}
+
+\index{Trybulec, Zinaida}
+\index{Swieczkowska, Halina}
+\begin{chunk}{axiom.bib}
+@article{Tryb92,
+ author = "Trybulec, Zinaida and Swieczkowska, Halina",
+ title = {{Some Remarks on The Language of Mathematical Texts}},
+ journal = "Studies in Logic, Grammar and Rhetoric",
+ volume = "10/11",
+ pages = "103124",
+ year = "1992",
+ link = "\url{http://mizar.org/trybulec65/5.pdf}",
+ paper = "Tryb92.pdf"
+}
+
+\end{chunk}
+
+\section{Proving Axiom Correct  Coercion in CASProof Systesms} %
+
+\index{Sozeau, Matthieu}
+\begin{chunk}{axiom.bib}
+@incollection{Soze06,
+ author = "Sozeau, Matthieu",
+ title = {{Subset Coercions in Coq}},
+ booktitle = "TYPES: Int. Workshop on Types for Proofs and Programs",
+ journal = "LNCS",
+ volume = "4502",
+ pages = "237252",
+ year = "2006",
+ abstract =
+ "We propose a new language for writing programs with dependent types
+ on top of the Coq proof assistant. This language permits to establish
+ a phase distinction between writing and proving algorithms in the Coq
+ environment. Concretely, this means allowing to write algorithms as
+ easily as in a practical functional programming language whilst giving
+ them as rich a specification as desired and proving that the code
+ meets the specification using the whole Coq proof apparatus. This is
+ achieved by extending conversion to an equivalence which relates
+ types and subsets based on them, a technique originating from the
+ ``Predicate subtyping'' featureof PVS and following mathematical
+ convention. The typing judgements can be translated to the Calculus of
+ (Co)Inductive Constructions (Cic) by means of an interpretation
+ which inserts coercions at the appropriate places.These coercions
+ can contain existential variables representing the propositional
+ parts of the final term, corresponding to proof obligations (or
+ PVS typechecking conditions). A prototype implementation of this
+ process is integrated with the Coq environment.",
+ paper = "Soze06.pdf"
+}
+
+\end{chunk}
+
+
+\section{Proving SAxiom Correct  CASProof System Survey} %%%%%%%%
\subsection{A} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ 11671,6 +11757,29 @@ when shown in factored form.
\end{chunk}
\index{Coquand, Thierry}
+\begin{chunk}{axiom.bib}
+@article{Coqu93,
+ author = "Coquand, Thierry",
+ title = {{Infinite Objects in Type Theory}},
+ journal = "LNCS",
+ volume = "806",
+ year = "1993",
+ pages = "6278",
+ abstract =
+ "We show that infinite objects can be constructively understood
+ without the consideration of partial elements, or greatest fixed
+ points, through the explicit consideration of proof objects. We
+ present then a proof system based on these explanations. According to
+ this analysis, the proof expressions should have the same structure
+ as the program expressions of a pure functional lazy language:
+ variable, constructor, application, abstraction, case expressions,
+ and local let expressions.",
+ paper = "Coqu93.pdf"
+}
+
+\end{chunk}
+
+\index{Coquand, Thierry}
\index{Dybjer, Peter}
\begin{chunk}{axiom.bib}
@article{Coqu96,
@@ 13751,7 +13860,7 @@ when shown in factored form.
\begin{chunk}{axiom.bib}
@inproceedings{Koun90,
author = "Kounalis, Emmanuel and Rusinowitch, Michael",
 titlexo = {{A Proof System for Conditional Algebraic Specifications}},
+ title = {{A Proof System for Conditional Algebraic Specifications}},
booktitle = "Conference Conditional and Typed Rewriting Systems",
year = "1990",
abstract =
@@ 15168,7 +15277,7 @@ when shown in factored form.
program can be extracted. Since some information cannot automatically
be inferred, we show how to annotate the program by specifying some of
its parts in order to guide the search for the proof.",
 paper = "Pare93.ps"
+ paper = "Pare93.pdf"
}
\end{chunk}
@@ 17324,6 +17433,7 @@ J. Symbolic COmputations 36 pp 855889
journal = "LNCS",
volume = "958",
pages = "209223",
+ year = "1994",
abstract =
"We present extended term rewriting systems as a means to describe a
simplification relation for an equational specification with a
@@ 26408,6 +26518,7 @@ Proc ISSAC 97 pp172175 (1997)
journal = "LNCS",
volume = "535",
pages = "243255",
+ year = "1991",
abstract =
"The paper presents an overview of the research achievements on issues
of common interest for Symbolic Computation and Artificial
@@ 37226,7 +37337,7 @@ SpringerVerlag, Berlin, Germany / Heildelberg, Germany / London, UK / etc.,
\begin{chunk}{axiom.bib}
@article{Igar75,
author = "Igarashi, Shigeru and London, Ralph L. and Luckham, David C.",
 titile = {{Automatic Program Verification I: A Logical Basis and Its
+ title = {{Automatic Program Verification I: A Logical Basis and Its
Implementation}},
journal = "Acta Informatica",
volume = "4",
@@ 47094,6 +47205,33 @@ National Physical Laboratory. (1982)
\subsection{B} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Bailey, Anthony}
+\begin{chunk}{axiom.bib}
+@article{Bail96,
+ author = "Bailey, Anthony",
+ title = {{Coercion Synthesis in Computer Implementations of
+ TypeTheoretic Frameworks}},
+ journal = "LNCS",
+ year = "1996",
+ pages = "927",
+ abstract =
+ "A coercion is a function that acts on a representation of some object
+ in order to alter its type. The idea is that although applying a
+ coercion to an object changes its type, the result still represents
+ the ``same'' abject in some sense; perhaps it is some essential
+ underlying part of the original object, or a different representation
+ of that object. This paper examines some of the issues involved in
+ the computer implementation of systems that allow a user to define
+ coercions that may then be left implicit in the syntax of expressions
+ and synthesised automatically. From a typetheoretic perspective,
+ coercions are often left implicit in mathematical texts, so they can
+ be used to improve the readability of a formalisation, and to
+ implement other tricks of syntax if so desired.",
+ paper = "Bail96.pdf"
+}
+
+\end{chunk}
+
\index{Bailey P. B.}
\begin{chunk}{ignore}
\bibitem[Bailey 66]{Bai66} Bailey P B
@@ 47148,6 +47286,29 @@ Academic Press. 1974
\end{chunk}
+\index{Barras, Bruno}
+\begin{chunk}{axiom.bib}
+@article{Barr96,
+ author = "Barras, Bruno",
+ title = {{Verification of the Interface of a Small Proof System in Coq}},
+ journal = "LNCS",
+ volume = "1512",
+ pages = "2845",
+ year = "1996",
+ abstract =
+ "This article describes the formalization of the interface of a
+ proofchecker. The latter is based on a kernel consisting of
+ typechecking functions for the Calculus of Constructions, but it
+ seems the ideas can generalize to other type systems, as fax as they
+ axe based on the proofs asterms principle. We suppose that the
+ metatheory of the corresponding type system is proved (up to type
+ decidability). We specify and certify the toplevel loop, the system
+ invariant, and the error messages.",
+ paper = "Barr96.pdf"
+}
+
+\end{chunk}
+
\index{Barrodale I.}
\index{Roberts F. D. K.}
\begin{chunk}{ignore}
@@ 47167,6 +47328,30 @@ Comm. ACM. 17, 6 319320. (1974)
\end{chunk}
+\index{Barthe, Gilles}
+\begin{chunk}{axiom.bib}
+@article{Bart95,
+ author = "Barthe, Gilles",
+ title = {{Implicit Coercions in Type Systems}},
+ journal = "LNCS",
+ volume = "1158",
+ year = "1995",
+ pages = "115",
+ abstract =
+ "We propose a notion of pure type system with implicit coercions. In
+ our framework, judgements are extended with a context of coercions Δ
+ and the application rule is modified so as to allow coercions to be
+ left implicit. The setting supports multiple inheritance and can be
+ applied to all type theories with $\Pi$types. One originality of our
+ work is to propose a computational interpretation for implicit
+ coercions. In this paper, we demonstrate how this interpretation
+ allows a strict control on the logical properties of pure type systems
+ with implicit coecions.",
+ paper = "Bart95.pdf"
+}
+
+\end{chunk}
+
\index{Barton, D.R.}
\index{Fitch, John P.}
\begin{chunk}{axiom.bib}
@@ 47282,6 +47467,22 @@ J. Symbolic Computation (1993) 15, 393413
\end{chunk}
+\index{Berger, U.}
+\index{Schwichtenberg, H.}
+\begin{chunk}{axiom.bib}
+@article{Berg95,
+ author = "Berger, U. and Schwichtenberg, H.",
+ title = {{The Greatest Common Divisor: A Case Study for Program
+ Extraction from Classical Proofs}},
+ journal = "LNCS",
+ volume = "1158",
+ year = "1995",
+ pages = "3646",
+ paper = "Berg95.pdf"
+}
+
+\end{chunk}
+
\index{Berndt, B.C.}
\begin{chunk}{axiom.bib}
@misc{Bern85,
@@ 47445,6 +47646,38 @@ Ginn \& Co., Boston and New York. (1962)
\end{chunk}
+\index{Bove, Ana}
+\begin{chunk}{axiom.bib}
+@article{Bove02,
+ author = "Bove, Ana",
+ title = {{General Recursion in Type Theory}},
+ journal = "LNCS",
+ volume = "2646",
+ pages = "3958",
+ year = "2002",
+ abstract =
+ "In this work, a method to formalise general recursive algorithms in
+ constructive type theory is presented throughout examples. The method
+ separates the computational and logical parts of the definitions. As
+ a consequence, the resulting typetheoretic algorithms are clear,
+ compact and easy to understand. They are as simple as their
+ equivalents in a functional programming language, where there is no
+ restriction on recursive calls. Given a general recursive algorithm,
+ the method consists in defining an inductive specialpurpose
+ accessibility predicate that characterises the inputs on which the
+ algorithm terminates. The typetheoretic version of the algorithm can
+ then be defined by structural recursion on the proof that the input
+ values satisfy this predicate. When formalising nested algorithms, the
+ specialpurpose accessibility predicate and the typetheoretic version
+ of the algorithm must be defined simultaneously because they depend on
+ each other. Since the method separates the computational part from
+ the logical part of a definition, formalising partial functions
+ becomes also possible.",
+ paper = "Bove02.pdf"
+}
+
+\end{chunk}
+
\index{Boyd, David W.}
\begin{chunk}{ignore}
\bibitem[Boyd9 3a]{Boyd93a} Boyd, David W.
@@ 48105,6 +48338,28 @@ Math. Comput. 51 267280. (1988)
\end{chunk}
+\index{Carlstrom, Jesper}
+\begin{chunk}{axiom.bib}
+@article{Carl02,
+ author = "Carlstrom, Jesper",
+ title = {{Subsets, Quotients, and Partial Functions in MartinL\"of's
+ Type Theory}},
+ journal = "LNCS",
+ volume = "2646",
+ year = "2002",
+ pages = "7894",
+ abstract =
+ "We treat subsets, equivalence relations, and partial functions,
+ with subsets as propositional functions .In order for these three
+ notions to work well together, we propose some changes to the theory
+ of subsets as propositional functions .The method used is not to make
+ any changes to the type theory itself, but to view the new concepts as
+ defined ones.",
+ paper = "Carl02.pdf"
+}
+
+\end{chunk}
+
\index{Cauchy, AugustinLux}
\begin{chunk}{ignore}
\bibitem[Cauchy 1829]{Cau1829} AugustinLux Cauchy
@@ 48321,6 +48576,33 @@ Rocky Mountain J. Math. 14 119139. (1984)
\end{chunk}
+\index{Coen, Claudio Sacerdoti}
+\index{Tassi, Enrico}
+\begin{chunk}{axiom.bib}
+@article{Coen07,
+ author = "Coen, Claudio Sacerdoti and Tassi, Enrico",
+ title = {{Working with Mathematical Structures in Type Theory}},
+ journal = "LNCS",
+ volume = "4941",
+ year = "2007",
+ pages = "157172",
+ abstract =
+ "We address the problem of representing mathematical structures in a
+ proof assistant which: 1) is based on a type theory with depen dent
+ types, telescopes and a computational version of Leibniz equality; 2)
+ implements coercive subtyping, accepting multiple coherent paths
+ between type families; 3) implements a restricted form of higher order
+ unification and type reconstruction. We show how to exploit the
+ previous quite common features to reduce the ``syntactic'' gap between
+ pen and paper and formalised algebra. However, to reach our goal we need
+ to propose unification and type reconstruction heuristics that are
+ slightly different from the ones usually implemented. We have
+ implemented them in Matita.",
+ paper = "Coen07.pdf"
+}
+
+\end{chunk}
+
\index{Cohn, Paul Moritz}
\begin{chunk}{axiom.bib}
@book{Cohn65,
@@ 48399,6 +48681,40 @@ A.K Peters, Natick, MA. (2003) ISBN 1568811349
\end{chunk}
+\index{Coquand, Thierry}
+\index{Persson, Henrik}
+\begin{chunk}{axiom.bib}
+@article{Coqu98,
+ author = "Coquand, Thierry and Persson, Henrik",
+ title = {{Groebner Bases in Type Theory}},
+ journal = "LNCS",
+ volume = "1657",
+ year = "1998",
+ pages = "3346",
+ abstract =
+ "We describe how the theory of Groebner bases, an important part
+ of computational algebra, can be developed within Martin Lof’s
+ type theory. In particular, we aim for an integrated development
+ of the algorithms for computing Groebner bases: we want to prove,
+ constructively in type theory, the existence of Groebner bases and
+ from such proofs extract the algorithms. Our main contribution is
+ a reformulation of the standard theory of Groebner bases which
+ uses generalised inductive definitions. We isolate the main
+ non–constructive part, a minimal bad sequence argument, and use
+ the open induction principle [Rao88,Coq92] to interpret it by
+ induction. This leads to short constructive proofs of Dickson’s
+ lemma and Hilbert’s basis theorem, which are used to give an
+ integrated development of Buchberger’s algorithm. An important
+ point of this work is that the elegance and brevity of the
+ original proofs are maintained while the new proofs also have a
+ direct constructive content. In the appendix we present a
+ computer formalisation of Dickson’s lemma and an abstract
+ existence proof of Groebner bases.",
+ paper = "Coqu98.pdf"
+}
+
+\end{chunk}
+
\index{Corless, Robert M.}
\index{Jeffrey, David J.}
\begin{chunk}{axiom.bib}
@@ 48949,6 +49265,25 @@ pp 1828
\end{chunk}
+\index{Dowek, Gilles}
+\begin{chunk}{axiom.bib}
+@article{Dowe96,
+ author = "Dowek, Gilles",
+ title = {{A TypeFree Formalization of Mathematics Where Proofs are
+ Objects}},
+ journal = "LNCS",
+ volume = "1512",
+ year = "1996",
+ pages = "88111",
+ abstract =
+ "We present a firstorder typefree axiomatization of mathematics
+ where proofs are objects in the sense of HeytingKolmogorov functional
+ interpretation. The consistency of this theory is open.",
+ paper = "Dowe96.pdf"
+}
+
+\end{chunk}
+
\index{Ducos, Lionel}
\begin{chunk}{ignore}
\bibitem[Ducos 00]{Duc00} Ducos, Lionel
@@ 49317,6 +49652,32 @@ A.E.R.E. Report R.8730. HMSO. (1977)
\end{chunk}
+\index{Filliatre, JeanChristophe}
+\begin{chunk}{axiom.bib}
+@article{Fill98,
+ author = "Filliatre, JeanChristophe",
+ title = {{Proof of Imperative Programs in Type Theory}},
+ journal = "LNCS",
+ volume = "1657",
+ year = "1998",
+ pages = "7892",
+ abstract =
+ "We present a new approach to certifying functional programs with
+ imperative aspects, in the context of Type Theory. The key is a
+ functional translation of imperative programs, based on a combination
+ of the type and effect discipline and monads. Then an incomplete proof
+ of the specification is built in the Type Theory, whose gaps would
+ corre spond to proof obligations. On sequential imperative programs,
+ we get the same proof obligations as those given by FloydHoare
+ logic. Compared to the latter, our approach also includes functional
+ constructions in a straightforward way. This work has been
+ implemented in the Coq Proof Assistant and applied on nontrivial
+ examples.",
+ paper = "Fill98.pdf"
+}
+
+\end{chunk}
+
\index{Fitch, John P.}
\begin{chunk}{axiom.bib}
@misc{Fitc74,
@@ 49637,6 +49998,7 @@ J. Comput. Appl. Math. 6 295302. (1980)
volume = "3702",
pages = "123137",
isbn = "3540289313",
+ year = "1985",
abstract =
"We extend classical firstorder logic with subtyping by type
predicates and type coercion. Type predicates assert that the value of
@@ 50125,6 +50487,35 @@ Grove, IL, USA and Oxford, UK, 1992
\end{chunk}
+\index{Haftmann, Florian}
+\index{Wenzel, Makarius}
+\begin{chunk}{axiom.bib}
+@article{Haft06,
+ author = "Haftmann, Florian and Wenzel, Makarius",
+ title = {{Constructive Type Classes in Isabelle}},
+ journal = "LNCS",
+ volume = "4502",
+ year = "2006",
+ abstract =
+ "We reconsider the wellknown concept of Haskellstyle type classes
+ within the logical framework of Isabelle. So far, axiomatic type
+ classes in Isabelle merely account for the logical aspect as
+ predicates over types, while the opera tional part is only a
+ convention based on raw overloading. Our more elaborate approach to
+ constructive type classes provides a seamless integration with
+ Isabelle locales, which are able to manage both operations and logical
+ properties uniformly. Thus we combine the convenience of type
+ classes and the flexibility of locales. Furthermore, we construct
+ dictionary terms derived from notions of the type system. This
+ additional internal structure provides satisfactory foundations of
+ type classes, and supports further applications, such as code
+ generation and export of theories and theorems to environments without
+ type classes.",
+ paper = "Haft06.pdf"
+}
+
+\end{chunk}
+
\index{Hall, G.}
\index{Watt J M.}
\begin{chunk}{ignore}
@@ 50166,6 +50557,33 @@ Methuen. (1967)
\index{Harrison, John}
\begin{chunk}{axiom.bib}
+@article{Harr06,
+ author = "Harrison, John",
+ title = {{Proof Style}},
+ journal = "LNCS",
+ volume = "1512",
+ year = "2006",
+ pages = "154172",
+ abstract =
+ "We are concerned with how computer theorem provers should expect
+ users to communicate proofs to them. There are many stylistic choices
+ that still allow the machine to generate a completely formal proof
+ object. The most obvious choice is the amount of guidance required
+ from the user, or from the machine perspective, the degree of
+ automation provided. But another important consideration, which we
+ consider particularly significant, is the bias towards a
+ 'procedural' or 'declarative' proof style. We will explore this
+ choice in depth, and discuss the strengths and weaknesses of
+ declarative and procedural styles for proofs in pure mathematics and
+ for verification applications. We conclude with a brief summary of
+ our own experiments in trying to combine both approaches.",
+ paper = "Harr06.pdf"
+}
+
+\end{chunk}
+
+\index{Harrison, John}
+\begin{chunk}{axiom.bib}
@inproceedings{Harr07,
author = "Harrison, John",
title = {{A Short Survey of Automated Reasoning}},
@@ 50662,6 +51080,28 @@ Comput. J. 9 281285. (1966)
\end{chunk}
+\index{Jones, Alex}
+\index{Luo, Zhaohui}
+\index{Soloviev, Sergei}
+\begin{chunk}{axiom.bib}
+@article{Jone96,
+ author = "Jones, Alex and Luo, Zhaohui and Soloviev, Sergei",
+ title = {{Some Algorithmic and ProofTheoretical Aspects of
+ Coercive Subtyping}},
+ journal = "LNCS",
+ volume = "1512",
+ year = "1996",
+ pages = "173195",
+ abstract =
+ "Coercive subtyping offers a conceptually simple but powerful
+ framework to understand subtyping and subset relationships in type
+ theory. In this paper we study some of its prooftheoretic and
+ computational properties.",
+ paper = "Jone96.pdf"
+}
+
+\end{chunk}
+
\index{Joyner, W. D.}
@misc{Joyn08a,
author = "Joyner, W. D.",
@@ 51016,6 +51456,30 @@ Springer Verlag Heidelberg, 1989, ISBN 0387969802
\end{chunk}
+\index{Kiessling, Robert}
+\index{Luo, Zhaohui}
+\begin{chunk}{axiom.bib}
+@article{Kies03,
+ author = "Kiessling, Robert and Luo, Zhaohui",
+ title = {{Coercions in HindleyMilner Systems}},
+ journal = "LNCS",
+ volume = "3085",
+ year = "2003",
+ abstract =
+ "Coercive subtyping is a theory of abbreviation for dependent type
+ theories. In this paper, we incorporate the idea of coercive subtyping
+ into the traditional HindleyMilner type systems in functional
+ programming languages. This results in a typing system with coercions,
+ an extension of the HindleyMilner type system. A type inference
+ algorithm is developed and shown to be sound and complete with respect
+ to the typing system. A notion of derivational coherence is developed
+ to deal with the problem of ambiguity and the corresponding type
+ inference algorithm is shown to be sound and complete.",
+ paper = "Kies03.pdf"
+}
+
+\end{chunk}
+
\index{Knuth, Donald E.}
\begin{chunk}{ignore}
\bibitem[Knuth 71]{Knu71} Knuth, Donald
@@ 51709,6 +52173,31 @@ AddisonWesley (March 1979) ISBN 0201144611
\end{chunk}
+\index{Luo, Zhaohui}
+\index{Soloviev, Sergei}
+\begin{chunk}{axiom.bib}
+@article{Luox99,
+ author = "Luo, Zhaohui and Soloviev, Sergei",
+ title = {{Dependent Coercions}},
+ journal = "Electr. Notes Theor. Comput. Sci.",
+ volume = "29",
+ year = "1999",
+ pages = "152168",
+ abstract =
+ "A notion of dependent coercion is introduced and studied in the
+ context of depen dent type theories. It extends our earlier work on
+ coercive subtyping into a uniform framework which increases the
+ expressive power with new applications. A dependent coercion
+ introduces a subtyping relation between a type and a family of types
+ in that an object of the type is mapped into one of the types in the
+ family. We present the formal framework, discuss its metatheory, and
+ consider applications such as its use in functional programming with
+ dependent types.",
+ paper = "Luox99.pdf"
+}
+
+\end{chunk}
+
\index{Lutzen, Jesper}
\begin{chunk}{axiom.bib}
@book{Lutz90,
@@ 51756,6 +52245,34 @@ AMS Chelsea Publishing ISBN 0821816462
\end{chunk}
\index{Magaud, Nicolas}
+\index{Bertot, Yves}
+\begin{chunk}{axiom.bib}
+@article{Maga00,
+ author = "Magaud, Nicolas and Bertot, Yves",
+ title = {{Changing Data Structures in Type Theory: A Study of
+ Natural Numbers}},
+ journal = "LNCS",
+ volume = "2277",
+ pages = "181196",
+ year = "2000",
+ abstract =
+ "In typetheory based proof systems that provide inductive
+ structures, computation tools are automatically associated to
+ inductive definitions. Choosing a particular representation for a
+ given concept has a strong influence on proof structure. We
+ propose a method to make the change from one representation to
+ another easier, by systematically translating proofs from one
+ context to another. We show how this method works by using it on
+ natural numbers, for which a unary representation (based on Peano
+ axioms) and abinary representation are available. This method
+ leads to an automatic translation tool that we have implemented in
+ Coq and successfully applied to several arithmetical theorems.",
+ paper = "Maga00.pdf"
+}
+
+\end{chunk}
+
+\index{Magaud, Nicolas}
\index{Narboux, Julien}
\index{Schreck, Pascal}
\begin{chunk}{axiom.bib}
@@ 52312,6 +52829,21 @@ Journal of the ACM, Vol. 25, No. 2, April 1978, pp. 271282
\subsection{N} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Naraschewski, Wolfgang}
+\index{Nipkow, Tobias}
+\begin{chunk}{axiom.bib}
+@article{Nara99,
+ author = "Naraschewski, Wolfgang and Nipkow, Tobias",
+ title = {{Type Inference Verified: Algorithm W in Isabelle/HOL}},
+ journal = "LNCS",
+ volume = "1512",
+ year = "1999",
+ pages = "317332",
+ paper = "Nara99.pdf"
+}
+
+\end{chunk}
+
\index{Naudin, Patrice}
\index{Quitte, Claude}
\begin{chunk}{axiom.bib}
@@ 52381,7 +52913,7 @@ Journal of the ACM, Vol. 25, No. 2, April 1978, pp. 271282
\index{Neuper, Walther}
\begin{chunk}{axiom.bib}
@article{Meup13a,
+@article{Neup13a,
author = "Neuper, Walther",
title = {{On the Emergence of TPbased Educational Math
Assistants}},
@@ 52459,6 +52991,24 @@ ACM Trans. Math. Softw. 5 118125. (1979)
\end{chunk}
+\index{Nipkow, Tobias}
+\begin{chunk}{axiom.bib}
+@article{Nipk02,
+ author = "Nipkow, Tobias",
+ title = {{Structured Proofs in Isar/HOL}},
+ journal = "LNCS",
+ volume = "2646",
+ year = "2002",
+ pages = "259278",
+ abstract =
+ "Isar is an extension of the theorem prover Isabelle with a language
+ for writing humanreadable structured proofs. This paper is an
+ introduction to the basic constructs of this language.",
+ paper = "Nipk02.pdf"
+}
+
+\end{chunk}
+
\subsection{O} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{chunk}{axiom.bib}
@@ 52604,7 +53154,7 @@ Science of Computer Programming V25 No.1 Oct 1995 pp4161 Elesevier
@article{Paul90,
author = "Paulson, Lawrence C.",
title = {{A Formulation of the Simple Theory of Types (for
 Isabelle}}},
+ Isabelle)}},
journal = "LNCS",
volume = "417",
pages = "246274",
@@ 52812,6 +53362,17 @@ SpringerVerlag, Heidelberg, 1982, ISBN 0387906932
\end{chunk}
+\index{Pierce, Benjamin}
+\begin{chunk}{axiom.bib}
+@misc{Pier17,
+ author = "Pierce, Benjamin",
+ title = "DeepSpec Summer School, Coq Intensive, Part 1 (July 13,2017)",
+ year = "2017",
+ link = "\url{https://www.youtube.com/watch?v=jG61w5pOc2A}"
+}
+
+\end{chunk}
+
\index{Piessens, R.}
\begin{chunk}{ignore}
\bibitem[Piessens 73]{Pie73} Piessens R.
@@ 54031,6 +54592,39 @@ J. Comput. Phys. 52 340350. (1983)
\end{chunk}
+\index{Traytel, Bmytro}
+\begin{chunk}{axiom.bib}
+@misc{Tray10,
+ author = "Traytel, Bmytro",
+ title = {{Extensions of a Type Inference Algorithm with Coerce Subtyping}},
+ school = "Der Technischen Universitat Munchen",
+ link = "\url{https://www21.in.tum.de/~traytel/bscthesis.pdf}",
+ year = "2010",
+ abstract =
+ "Subtyping with coercion semantics allows a type inference system to
+ correct some illtyped programs by the automatic insertion of
+ implicit type conversions at runtime. This simplifies programmer’s
+ life but has its price: the general typability problem for given base
+ type subtype dependencies is NPcomplete. Nevertheless, if the given
+ coercions define an order on types with certain properties, the
+ problem behaves in a sane way in terms of complexity. This thesis
+ presents an algorithm that can be used to extend HindleyMilner type
+ inference with coercive subtyping assuming a given partial order on
+ base types. Especially, we discuss restrictions on the subtype
+ dependencies that are necessary to achieve an efficient
+ implementation. Examples of problems that occur if these restrictions
+ are not met are given. The result of these considerations is that the
+ algorithm is complete if the given base type poset is a disjoint union
+ of lattices. Furthermore, the interaction of subtyping with type
+ classes is addressed. The algorithm that is extended to deal with
+ type classes requires even a stronger restriction to assure
+ completeness. An MLimplementation of the presented algorithm is used
+ in the generic proof assistant Isabelle.",
+ paper = "Tray10.pdf"
+}
+
+\end{chunk}
+
\index{Trybulec, Andrzej}
\begin{chunk}{axiom.bib}
@misc{Tryb02,
@@ 54350,6 +54944,35 @@ SIAM J. Sci. Statist. Comput. 3 387407. (1982)
\end{chunk}
+\index{Wiedijk, Freek}
+\begin{chunk}{axiom.bib}
+@article{Wied03,
+ author = "Wiedijk, Freek",
+ title = {{Formal Proof Sketches}},
+ journal = "LNCS",
+ volume = "3085",
+ year = "2003",
+ pages = "378393",
+ abstract =
+ "Formalized mathematics currently does not look much like informal
+ mathematics. Also, formalizing mathematics currently seems far too
+ much work to be worth the time of the working mathematician. To
+ address both of these problems we introduce the notion of a formal
+ proof sketch . This is a proof representation that is in between a
+ fully checkable formal proof and a statement without any proof at
+ all. Although a formal proof sketch is too high level to be checkable
+ by computer, it has a precise notion of correctness (hence the
+ adjective formal ). We will show through examples that formal proof
+ sketches can closely mimic already existing mathematical
+ proofs. Therefore, although a formal proof sketch contains gaps in
+ the reasoning from a formal point of view (which is why we call it a
+ sketch ), a mathematician probably would call such a text just a
+ ‘proof’.",
+ paper = "Wied03.pdf"
+}
+
+\end{chunk}
+
\begin{chunk}{ignore}
\bibitem[Wiki 3]{Wiki3}.
title = {{Givens Rotations}},
diff git a/changelog b/changelog
index fbda247..95bee80 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20171206 tpd src/axiomwebsite/patches.html 20171206.01.tpd.patch
+20171206 tpd books/bookvolbib add references
20171202 tpd src/axiomwebsite/patches.html 20171202.01.tpd.patch
20171202 tpd books/bookvolbib add references
20171127 tpd src/axiomwebsite/patches.html 20171127.01.tpd.patch
diff git a/patch b/patch
index 2cd26dc..eaf8604 100644
 a/patch
+++ b/patch
@@ 1,491 +1,615 @@
books/bookvolbib add references
Goal: Proving Axiom Correct
+Goal: Proving Axiom Correct  Coercion in CASProof Systesms
\index{Maurer, D.}
+\index{Sozeau, Matthieu}
\begin{chunk}{axiom.bib}
@article{Maur73,
 author = "Maurer, D.",
 title = {{Applications of Symbolic Mathematical Manipulation to
 Algorithmic Verification (Abstract)},
 journal = "SIGSAM Bulletin",
 volume = "26",
 year = "1973",
 pages = "4"
+\incollection{Soze06,
+ author = "Sozeau, Matthieu",
+ title = {{Subset Coercions in Coq}},
+ booktitle = "TYPES: Int. Workshop on Types for Proofs and Programs",
+ journal = "LNCS",
+ volume = "4502",
+ pages = "237252",
+ year = "2006",
+ abstract =
+ "We propose a new language for writing programs with dependent types
+ on top of the Coq proof assistant. This language permits to establish
+ a phase distinction between writing and proving algorithms in the Coq
+ environment. Concretely, this means allowing to write algorithms as
+ easily as in a practical functional programming language whilst giving
+ them as rich a specification as desired and proving that the code
+ meets the specification using the whole Coq proof apparatus. This is
+ achieved by extending conversion to an equivalence which relates
+ types and subsets based on them, a technique originating from the
+ ``Predicate subtyping'' featureof PVS and following mathematical
+ convention. The typing judgements can be translated to the Calculus of
+ (Co)Inductive Constructions (Cic) by means of an interpretation
+ which inserts coercions at the appropriate places.These coercions
+ can contain existential variables representing the propositional
+ parts of the final term, corresponding to proof obligations (or
+ PVS typechecking conditions). A prototype implementation of this
+ process is integrated with the Coq environment.",
+ paper = "Soze06.pdf"
}
\end{chunk}
\index{Waldinger, R.J.}
\index{Levitt, K.N.}
+\index{Pierce, Benjamin}
\begin{chunk}{axiom.bib}
@article{Wald74,
 author = "Waldinger, R.J. and Levitt, K.N.",
 title = {{Reasoning about Programs}},
 journal = "Artificial Intelligence",
 volume = "5",
 number = "3",
 year = "1974",
 pages = "235316",
+@misc{Pier17,
+ author = "Pierce, Benjamin",
+ title = "DeepSpec Summer School, Coq Intensive, Part 1 (July 13,2017)",
+ year = "2017",
+ link = "\url{https://www.youtube.com/watch?v=jG61w5pOc2A}"
+}
+
+\end{chunk}
+
+\index{Haftmann, Florian}
+\index{Wenzel, Makarius}
+\begin{chunk}{axiom.bib}
+@article{Haft06,
+ author = "Haftmann, Florian and Wenzel, Makarius",
+ title = {{Constructive Type Classes in Isabelle}},
+ journal = "LNCS",
+ volume = "4502",
+ year = "2006",
abstract =
 "This paper describes a theorem prover that embodies knowledge about
 programming constructs, such as numbers, arrays, lists, and
 expressions. The program can reason about these concepts and is used
 as part of a program verification system that uses the FloydNaur
 explication of program semantics. It is implemented in the qa4
 language; the qa4 system allows many pieces of strategic knowledge,
 each expressed as a small program, to be coordinated so that a program
 stands forward when it is relevant to the problem at hand. The
 language allows clear, concise representation of this sort of
 knowledge. The qa4 system also has special facilities for dealing with
 commutative functions, ordering relations, and equivalence relations;
 these features are heavily used in this deductive system. The program
 interrogates the user and asks his advice in the course of a
 proof. Verifications have been found for Hoare's FIND program, a
 realnumber division algorithm, and some sort programs, as well as for
 many simpler algorithms. Additional theorems have been proved about a
 pattern matcher and a version of Robinson's unification algorithm. The
 appendix contains a complete, annotated listing of the deductive
 system and annotated traces of several of the deductions performed by
 the system.",
 paper = "Wald74.pdf"
+ "We reconsider the wellknown concept of Haskellstyle type classes
+ within the logical framework of Isabelle. So far, axiomatic type
+ classes in Isabelle merely account for the logical aspect as
+ predicates over types, while the opera tional part is only a
+ convention based on raw overloading. Our more elaborate approach to
+ constructive type classes provides a seamless integration with
+ Isabelle locales, which are able to manage both operations and logical
+ properties uniformly. Thus we combine the convenience of type
+ classes and the flexibility of locales. Furthermore, we construct
+ dictionary terms derived from notions of the type system. This
+ additional internal structure provides satisfactory foundations of
+ type classes, and supports further applications, such as code
+ generation and export of theories and theorems to environments without
+ type classes.",
+ paper = "Haft06.pdf"
}
\end{chunk}
\index{Floyd, W.}
+\index{Kiessling, Robert}
+\index{Luo, Zhaohui}
\begin{chunk}{axiom.bib}
@incollection{Floy86,
 author = "Floyd, W.",
 title = {{Toward Interactive Design of Correct Programs}},
 booktitle = "Reading in Artificial Intelligence and Software Engeering",
 pages = "331334",
 year = "1986",
 isbn = "0934613125"
+@article{Kies03,
+ author = "Kiessling, Robert and Luo, Zhaohui",
+ title = {{Coercions in HindleyMilner Systems}},
+ journal = "LNCS",
+ volume = "3085",
+ year = "2003",
+ abstract =
+ "Coercive subtyping is a theory of abbreviation for dependent type
+ theories. In this paper, we incorporate the idea of coercive subtyping
+ into the traditional HindleyMilner type systems in functional
+ programming languages. This results in a typing system with coercions,
+ an extension of the HindleyMilner type system. A type inference
+ algorithm is developed and shown to be sound and complete with respect
+ to the typing system. A notion of derivational coherence is developed
+ to deal with the problem of ambiguity and the corresponding type
+ inference algorithm is shown to be sound and complete.",
+ paper = "Kies03.pdf"
}
\end{chunk}
\index{Milner, R.}
+\index{Wiedijk, Freek}
\begin{chunk}{axiom.bib}
@article{Miln84,
 author = "Milner, R.",
 title = {{The Use of Machines to Assist in Rigorous Proof}},
 journal = "Philosophical Transactions of the Royal Society",
 volume = "312",
 pages = "411422",
 number = "1522",
 year = "1984",
+@article{Wied03,
+ author = "Wiedijk, Freek",
+ title = {{Formal Proof Sketches}},
+ journal = "LNCS",
+ volume = "3085",
+ year = "2003",
+ pages = "378393",
abstract =
 "A methodology for computer assisted proof is presented with an
 example. A central ingredient in the method is the presentation of
 tactics (or strategies) in an algorithmic metalanguage. Further, the
 same language is also used to express combinators, by which simple
 elementary tactics  which often correspond to the inference rules of
 the logic employed  are combined into more complex tactics, which may
 even be strategies complete for a class of problems. However, the
 emphasis is not upon completeness but upon providing a metalogical
 framework within which a user may express his insight into proof
 methods and may delegate routine (but errorprone) work to the
 computer. This method of tactic composition is presented at the start
 of the paper in the form of an elementary theory of goalseeking. A
 second ingredient of the methodology is the stratification of
 machineassisted proof by an ancestry graph of applied theories, and
 the example illustrates this stratification. In the final section,
 some recent developments and applications of the method are cited.",
 paper = "Miln84.pdf"
+ "Formalized mathematics currently does not look much like informal
+ mathematics. Also, formalizing mathematics currently seems far too
+ much work to be worth the time of the working mathematician. To
+ address both of these problems we introduce the notion of a formal
+ proof sketch . This is a proof representation that is in between a
+ fully checkable formal proof and a statement without any proof at
+ all. Although a formal proof sketch is too high level to be checkable
+ by computer, it has a precise notion of correctness (hence the
+ adjective formal ). We will show through examples that formal proof
+ sketches can closely mimic already existing mathematical
+ proofs. Therefore, although a formal proof sketch contains gaps in
+ the reasoning from a formal point of view (which is why we call it a
+ sketch ), a mathematician probably would call such a text just a
+ ‘proof’.",
+ paper = "Wied03.pdf"
}
\end{chunk}
\index{Giunchiglia, Fausto}
\index{Pecchiari, Paolo}
\index{Talcott, Carolyn}
+\index{Coquand, Thierry}
+\index{Persson, Henrik}
\begin{chunk}{axiom.bib}
@techreport{Giun94,
 author = "Giunchiglia, Fausto and Pecchiari, Paolo and Talcott, Carolyn",
 title = {{Reasoning Theories  Towards an Architecture for Open
 Mechanized Reasoning}},
 year = "1994",
 institution = "Stanford University",
+@article{Coqu98,
+ author = "Coquand, Thierry and Persson, Henrik",
+ title = {{Groebner Bases in Type Theory}},
+ journal = "LNCS",
+ volume = "1657",
+ year = "1998",
+ pages = "3346",
abstract =
 "Our ultimate goal is to provide a framework and a methodology which
 will allow users, and not only system developers, to construct complex
 reasoning systems by composing existing modules, or to add new modules
 to existing systems, in a "plug and play" manner. These modules and
 systems might be based on different logics; have different domain
 models; use different vocabularies and data structures; use different
 reasoning strategies; and have different interaction
 capabilities. This paper makes two main contributions towards our
 goal. First, it proposes a general architecture for a class of
 reasoning systems called Open Mechanized Reasoning Systems (OMRSs). An
 OMRS has three components: a reasoning theory component which is the
 counterpart of the logical notion of formal system, a control
 component which consists of a set of inference strategies, and an
 interaction component which provides an OMRS with the capability of
 interacting with other systems, including OMRSs and hum...",
 paper = "Giun94.pdf"
+ "We describe how the theory of Groebner bases, an important part
+ of computational algebra, can be developed within Martin Lof’s
+ type theory. In particular, we aim for an integrated development
+ of the algorithms for computing Groebner bases: we want to prove,
+ constructively in type theory, the existence of Groebner bases and
+ from such proofs extract the algorithms. Our main contribution is
+ a reformulation of the standard theory of Groebner bases which
+ uses generalised inductive definitions. We isolate the main
+ non–constructive part, a minimal bad sequence argument, and use
+ the open induction principle [Rao88,Coq92] to interpret it by
+ induction. This leads to short constructive proofs of Dickson’s
+ lemma and Hilbert’s basis theorem, which are used to give an
+ integrated development of Buchberger’s algorithm. An important
+ point of this work is that the elegance and brevity of the
+ original proofs are maintained while the new proofs also have a
+ direct constructive content. In the appendix we present a
+ computer formalisation of Dickson’s lemma and an abstract
+ existence proof of Groebner bases.",
+ paper = "Coqu98.pdf"
}
\end{chunk}
\index{Carette, Jacques}
\index{Farmer, William M.}
\index{Wajs, Jeremie}
+\index{Filliatre, JeanChristophe}
\begin{chunk}{axiom.bib}
@misc{Care11b,
 author = "Carette, Jacques and Farmer, William M. and Wajs, Jeremie",
 title = {{Trustable Communication Between Mathematics Systems}},
 year = "2011",
 link = "\url{https://pdfs.semanticscholar.org/0d0b/206edf7ef1c01d7bfa1284c85b469b2fbd29.pdf}",
+@article{Fill98,
+ author = "Filliatre, JeanChristophe",
+ title = {{Proof of Imperative Programs in Type Theory}},
+ journal = "LNCS",
+ volume = "1657",
+ year = "1998",
+ pages = "7892",
+ abstract =
+ "We present a new approach to certifying functional programs with
+ imperative aspects, in the context of Type Theory. The key is a
+ functional translation of imperative programs, based on a combination
+ of the type and effect discipline and monads. Then an incomplete proof
+ of the specification is built in the Type Theory, whose gaps would
+ corre spond to proof obligations. On sequential imperative programs,
+ we get the same proof obligations as those given by FloydHoare
+ logic. Compared to the latter, our approach also includes functional
+ constructions in a straightforward way. This work has been
+ implemented in the Coq Proof Assistant and applied on nontrivial
+ examples.",
+ paper = "Fill98.pdf"
+}
+
+\end{chunk}
+
+\index{Nipkow, Tobias}
+\begin{chunk}{axiom.bib}
+@article{Nipk02,
+ author = "Nipkow, Tobias",
+ title = {{Structured Proofs in Isar/HOL}},
+ journal = "LNCS",
+ volume = "2646",
+ year = "2002",
+ pages = "259278",
abstract =
 "This paper presents a rigorous, unified framework for facilitating
 communication between mathematics systems. A mathematics system is
 given one or more interfaces which offer deductive and computational
 services to other mathematics systems. To achieve communication
 between systems, a client interface is linked to a server interface by
 an asymmetric connection consisting of a pair of translations.
 Answers to requests are trustable in the sense that they are correct
 provided a small set of prescribed conditions are satisfied. The
 frame work is robust with respect to interface extension and can
 process requests for abstract services, where the server interface is
 not fully specified.",
 paper = "Care11b.pdf"
+ "Isar is an extension of the theorem prover Isabelle with a language
+ for writing humanreadable structured proofs. This paper is an
+ introduction to the basic constructs of this language.",
+ paper = "Nipk02.pdf"
}
\end{chunk}
\index{Carlisle, David}
\index{Ion, Patrick}
\index{Miner, Robert}
+\index{Carlstrom, Jesper}
\begin{chunk}{axiom.bib}
@misc{Carl14,
 author = "Carlisle, David and Ion, Patrick and Miner, Robert",
 title = {{Mathematical Markup Language}},
 year = "2014",
 link = "\url{https://www.w3.org/TR/MathML3/}"
+@article{Carl02,
+ author = "Carlstrom, Jesper",
+ title = {{Subsets, Quotients, and Partial Functions in MartinL\"of's
+ Type Theory}},
+ journal = "LNCS",
+ volume = "2646",
+ year = "2002",
+ pages = "7894",
+ abstract =
+ "We treat subsets, equivalence relations, and partial functions,
+ with subsets as propositional functions .In order for these three
+ notions to work well together, we propose some changes to the theory
+ of subsets as propositional functions .The method used is not to make
+ any changes to the type theory itself, but to view the new concepts as
+ defined ones.",
+ paper = "Carl02.pdf"
}
\end{chunk}
\index{Buswell, S.}
\index{Caprotti, O.}
\index{Carlisle, D.P.}
\index{Dewar, M.C.}
\index{Gaetano, M.}
\index{Kohlhase, M.}
+\index{Bove, Ana}
\begin{chunk}{axiom.bib}
@misc{Busw04,
 author = "Buswell, S. and Caprotti, O. and Carlisle, D.P. and Dewar, M.C.
 and Gaetano, M. and Kohlhase, M.",
 title = {{The OpenMath Standard}},
 year = "2004",
 link = "\url{https://www.openmath.org/standard/om2020040630/omstd20.pdf}",
 paper = "Busw04.pdf"
+@article{Bove02,
+ author = "Bove, Ana",
+ title = {{General Recursion in Type Theory}},
+ journal = "LNCS",
+ volume = "2646",
+ pages = "3958",
+ abstract =
+ "In this work, a method to formalise general recursive algorithms in
+ constructive type theory is presented throughout examples. The method
+ separates the computational and logical parts of the definitions. As
+ a consequence, the resulting typetheoretic algorithms are clear,
+ compact and easy to understand. They are as simple as their
+ equivalents in a functional programming language, where there is no
+ restriction on recursive calls. Given a general recursive algorithm,
+ the method consists in defining an inductive specialpurpose
+ accessibility predicate that characterises the inputs on which the
+ algorithm terminates. The typetheoretic version of the algorithm can
+ then be defined by structural recursion on the proof that the input
+ values satisfy this predicate. When formalising nested algorithms, the
+ specialpurpose accessibility predicate and the typetheoretic version
+ of the algorithm must be defined simultaneously because they depend on
+ each other. Since the method separates the computational part from
+ the logical part of a definition, formalising partial functions
+ becomes also possible.",
+ paper = "Bove02.pdf"
}
\end{chunk}
\index{Armando, Alessandro}
\index{Zini, Daniele}
+\index{Coen, Claudio Sacerdoti}
+\index{Tassi, Enrico}
\begin{chunk}{axiom.bib}
@misc{Arma00,
 author = "Armando, Alessandro and Zini, Daniele",
 title = {{Towards Interoperable Mechanized Reasoning Systems:
 The Logic Broker Architecture}},
 year = "2000",
+@article{Coen07,
+ author = "Coen, Claudio Sacerdoti and Tassi, Enrico",
+ title = {{Working with Mathematical Structures in Type Theory}},
+ journal = "LNCS",
+ volume = "4941",
+ year = "2007",
+ pages = "157172",
+ abstract =
+ "We address the problem of representing mathematical structures in a
+ proof assistant which: 1) is based on a type theory with depen dent
+ types, telescopes and a computational version of Leibniz equality; 2)
+ implements coercive subtyping, accepting multiple coherent paths
+ between type families; 3) implements a restricted form of higher order
+ unification and type reconstruction. We show how to exploit the
+ previous quite common features to reduce the ``syntactic'' gap between
+ pen and paper and formalised algebra. However, to reach our goal we need
+ to propose unification and type reconstruction heuristics that are
+ slightly different from the ones usually implemented. We have
+ implemented them in Matita.",
+ paper = "Coen07.pdf"
+}
+
+\end{chunk}
+
+\index{Coquand, Thierry}
+\begin{chunk}{axiom.bib}
+@article{Coqu93,
+ author = "Coquand, Thierry",
+ title = {{Infinite Objects in Type Theory}},
+ journal = "LNCS",
+ volume = "806",
+ year = "1993",
+ pages = "6278",
abstract =
 "There is a growing interest in the integration of mechanized
 reasoning systems such as automated theorem provers, computer algebra
 systems, and model checkers. Stateoftheart reasoning systems are
 the result of many manyears of careful development and engineering,
 and usually they provide a high degree of sophistication in their
 respective domain. Yet they often perform poorly when applied outside
 the domain they have been designed for. The problem of integrating
 mechanized reasoning systems is therefore being perceived as an
 important issue in automated reasoning. In this paper we present
 the Logic Broker Architecture, a framework which provides the needed
 infrastructure for making mechanized reasoning systems interoperate.
 The architecture provides location transparency, a way to forward
 requests for logical services to appropriate reasoning systems via a
 simple registration/subscription mechanism, and a translation
 mechanism which ensures the transparent and provably sound exchange of
 logical services.",
 paper = "Arma00.pdf"
+ "We show that infinite objects can be constructively understood
+ without the consideration of partial elements, or greatest fixed
+ points, through the explicit consideration of proof objects. We
+ present then a proof system based on these explanations. According to
+ this analysis, the proof expressions should have the same structure
+ as the program expressions of a pure functional lazy language:
+ variable, constructor, application, abstraction, case expressions,
+ and local let expressions.",
+ paper = "Coqu93.pdf"
}
\end{chunk}
\index{Lester, D.R.}
+\index{Barthe, Gilles}
\begin{chunk}{axiom.bib}
@inproceedings{Lest01,
 author = "Lester, D.R.",
 title = {{Effective Continued Fractions}},
 booktitle = "15th IEEE Symp. on Computer Arithmetic",
 publisher = "IEEE Computer Society Press",
 year = "2001",
 pages = "163170",
+@article{Bart95,
+ author = "Barthe, Gilles",
+ title = {{Implicit Coercions in Type Systems}},
+ journal = "LNCS",
+ volume = "1158",
+ year = "1995",
+ pages = "115",
abstract =
 "Only the leading seven terms of a continued fraction are needed to
 perform online arithmetic, provided the continued fractions are of
 the correct form. This forms the basis of a proof that there is an
 effective representation of the computable reals as continued
 fractions: we also demonstrate that the basic arithmetic operations
 are computable using this representation.",
 paper = "Lest01.pdf"
+ "We propose a notion of pure type system with implicit coercions. In
+ our framework, judgements are extended with a context of coercions Δ
+ and the application rule is modified so as to allow coercions to be
+ left implicit. The setting supports multiple inheritance and can be
+ applied to all type theories with $\Pi$types. One originality of our work
+ is to propose a computational interpretation for implicit
+ coercions. In this paper, we demonstrate how this interpretation
+ allows a strict control on the logical properties of pure type systems
+ with implicit coecions.",
+ paper = "Bart95.pdf"
}
\end{chunk}
\index{Vuillemin, J.}
+\index{Berger, U.}
+\index{Schwichtenberg, H.}
\begin{chunk}{axiom.bib}
@techreport{Vuil87,
 author = "Vuillemin, J.",
 title = {{Exact Real Computer Arithmetic with Continued Fractions}},
 institution = "Institut National de Recherche en Informatique et en
 Automatique",
 year = "1987",
 number = "760",
+@article{Berg95,
+ author = "Berger, U. and Schwichtenberg, H.",
+ title = {{The Greatest Common Divisor: A Case Study for Program
+ Extraction from Classical Proofs}},
+ journal = "LNCS",
+ volume = "1158",
+ year = "1995",
+ pages = "3646",
+ paper = "Berg95.pdf"
+}
+
+\end{chunk}
+
+\index{Magaud, Nicolas}
+\index{Bertot, Yves}
+\begin{chunk}{axiom.bib}
+@article{Maga00,
+ author = "Magaud, Nicolas and Bertot, Yves",
+ title = {{Changing Data Structures in Type Theory: A Study of
+ Natural Numbers}},
+ journal = "LNCS",
+ volume = "2277",
+ pages = "181196",
+ year = "2000",
abstract =
 "We discuss a representation of the {\sl computable real numbers} by
 continued fractions. This deals with the subtle points of undecidable
 and integer division, as well as representing the infinite
 $\infty=1/0$ and undefined $\bot=0/0$ numbers. Two general algorithms
 for performing arithmetic operations are introduced. The
 {\sl algebraic algorithm}, which computes sums and products of
 continued fractions as a special case, basically operates in a
 positional manner, producing one term of output for each term of
 input. The {\sl transcendental algorithm} uses a general formula of
 Gauss to compute the continued fractions of exponentials, logarithms,
 trigonometric functions, as well as a wide class of special
 functions. This work has been implemented in Le\_Lisp and the
 performance of these algorithms appears to be quite good; however, no
 competing system has been available for comparison",
 paper = "Vuil87.pdf"
+ "In typetheory based proof systems that provide inductive
+ structures, computation tools are automatically associated to
+ inductive definitions. Choosing a particular representation for a
+ given concept has a strong influence on proof structure. We
+ propose a method to make the change from one representation to
+ another easier, by systematically translating proofs from one
+ context to another. We show how this method works by using it on
+ natural numbers, for which a unary representation (based on Peano
+ axioms) and abinary representation are available. This method
+ leads to an automatic translation tool that we have implemented in
+ Coq and successfully applied to several arithmetical theorems.",
+ paper = "Maga00.pdf"
}
\end{chunk}
\index{Zinn, Claus}
+\index{Bailey, Anthony}
\begin{chunk}{axiom.bib}
@phdthesis{Zinn04,
 author = "Zinn, Claus",
 title = {{Understanding Informal Mathematical Discourse}},
 school = "Universitat Erlangen Nurnberg",
 year = "2004",
+@article{Bail96,
+ author = "Bailey, Anthony",
+ title = {{Coercion Synthesis in Computer Implementations of
+ TypeTheoretic Frameworks}},
+ journal = "LNCS",
+ year = "1996",
+ pages = "927",
abstract =
 "Automated reasoning is one of the most established disciplines in
 informatics and artificial intelligence, and formal methods become
 increasingly employed in practical applications. However, for the most
 part, such applications seem to be limited to informaticsspecific
 areas (e.g., the verification of correctness properties of software
 and hardware specifications) and areas close to informatics such as
 computational linguistics (e.g., the computation of consistence and
 informativeness properties of semantic representations). Naturally,
 there is also a potential for practical applications in the the area
 of mathematics: the generation of proofs for mathematically
 interesting and motivated theorems and, quite associated, the
 computersupported formalisation of (parts of elementary)
 mathematics. It is a matter of fact, however, that mathematicians
 rarely use computersupport for the construction and verification of
 proofs. This is mainly caused by the “unnaturalness” of the language
 and the reasoning that such proof engines support.

 In the past, researchers in the area of automated reasoning have
 focused their work on formalisms and algorithms that allow the
 construction and verification of proofs that are written in a
 formallogical language and that only use a limited number of
 inference rules. For the computer scientist, such formal proofs have
 the advantage of a simple and ambiguousfree syntax, which can thus be
 easily processed. Moreover, the limited number of inference rules has
 a direct impact on the complexity of the search space that needs to be
 conquered during the process of constructing proofs. The verification
 of given formal proofs is greatly facilitated by the complete
 explicitness of their logical argumentation where no reasoning step is
 left out. For mathematicians, however, such formal proofs are usually
 hard to understand. For them, they are written in an unfamiliar and
 artificial language and much too detailed. Moreover, the sheer number
 of inference steps, while logically relevant, describe only trivial
 mathematical details and make it difficult to follow a proof’s main
 underlying argumentation line. In practise, thus, mathematicians use
 proof generation engines rather seldom, if at all. The same is true
 with regard to proof verification tools. The amount of work that is
 required to verify a mathematical proof with such tools is
 considerable, if not prohibitive. Since proof verification systems
 only accept formal proofs as input, the mathematician’s first task is
 to manually translate the mathematical proof into the formal language
 that is accepted by the verifier. This in turn includes the
 translation of the proof’s underlying mathematical argumentation into
 inference rules that are supported by the proof engine. Such
 translations and refinements are usually very time consuming, tedious,
 and prone to error themselves. Hence, how the proof verifier then
 judges the result of proof translation and proof refinement is only
 of limited relevance to the original mathematical proof. From the
 mathematician’s point of view, there is thus a need for a proof
 verification system that is capable of processing mathematical proofs
 automatically, at least with regard to translating the mathematicians’
 expert language into the system’s artificial formal language. Such a
 system would have an enormous potential in the community of
 mathematics, and this potential has been recognised early. In the
 beginning of the 1960s, John McCarthy, one of the pioneers of
 artificial intelligence, remarked that ``[c]hecking mathematical proofs
 is potentially one of the most interesting and useful applications of
 automatic computers'' [111]. More than forty years thereafter, a tool
 that supports mathematicians with the verification of mathematical
 proofs is more science fiction than reality. Its realisation is
 associated with research questions within the disciplines of automated
 reasoning and computational linguistics that are still only partially
 answered.

 This thesis aims at contributing towards the realisation of a
 verifier for mathematical proofs. It attempts to provide a general
 framework as well as an implementation for such a proof
 engine. The dissertation’s objects of study are short and simple
 proofs that were taken from textbooks on elementary number
 theory. Fig. 1 depicts a proof of the mathematical truth that
 every positive integer greater than 1 can be represented as a
 product of one or more primes. The proof consists of only a few
 lines and little mathematical knowledge is necessary to follow the
 proof author’s argumentation. It is this kind of short proof that
 we attempt to check automatically.",
 paper = "Zinn04.pdf"
+ "A coercion is a function that acts on a representation of some object
+ in order to alter its type. The idea is that although applying a
+ coercion to an object changes its type, the result still represents
+ the ``same'' abject in some sense; perhaps it is some essential
+ underlying part of the original object, or a different representation
+ of that object. This paper examines some of the issues involved in
+ the computer implementation of systems that allow a user to define
+ coercions that may then be left implicit in the syntax of expressions
+ and synthesised automatically. From a typetheoretic perspective,
+ coercions are often left implicit in mathematical texts, so they can
+ be used to improve the readability of a formalisation, and to
+ implement other tricks of syntax if so desired.",
+ paper = "Bail96.pdf"
}
\end{chunk}
\index{Trybulec, Andrzej}
+\index{Barras, Bruno}
\begin{chunk}{axiom.bib}
@misc{Tryb02,
 author = "Trybulec, Andrzej",
 title = {{Towards Practical Formalizaiton of Mathematics}},
 comment = "abstract",
 link =
 "\url{http://www.macs.hw.ac.uk/~fairouz/forest//events/automath2002/abstracts/Andrzej.abst.html}",
+@article{Barr96,
+ author = "Barras, Bruno",
+ title = {{Verification of the Interface of a Small Proof System in Coq}},
+ journal = "LNCS",
+ volume = "1512",
+ pages = "2845",
+ year = "1996",
abstract =
 "In sixties the opinion that mathematics cannot be practically
 formalized was well established. So the main achievement of de Bruijn,
 among many others, is the decision that the problem must be reconsider
 and probably positively solved. And I believe that 1967 will be
 treated by future historians of mathematics as a turning point.

 It is not easy to say precisely what we learnt in the meantime, if we
 learnt anything at all. I believe that the most important results are:
 \begin{enumerate}
 \item we need experiments with much more advanced mathematics than
 already done
 \item a system for practical formalization of mathematics probably will
 not be a simple system based on small number of primitive notions
 \item integration with a computer algebra systems may be necessary or at
 least a feasible system must have bigger computational power.
 \end{enumerate}

 Still we should me more concerned with the original ideas of de
 Bruijn, the most important that eventually we have to be able to
 formalize new mathematical results, published in mathematical
 newspapers in this century."
+ "This article describes the formalization of the interface of a
+ proofchecker. The latter is based on a kernel consisting of
+ typechecking functions for the Calculus of Constructions, but it
+ seems the ideas can generalize to other type systems, as fax as they
+ axe based on the proofs asterms principle. We suppose that the
+ metatheory of the corresponding type system is proved (up to type
+ decidability). We specify and certify the toplevel loop, the system
+ invariant, and the error messages.",
+ paper = "Barr96.pdf"
}
\end{chunk}
\index{Hayes, Patrick J.}
+\index{Dowek, Gilles}
\begin{chunk}{axiom.bib}
@inproceedings{Haye74,
 author = "Hayes, Patrick J.",
 title = {{Some Problems and Nonproblems in Representation Theory}},
 booktitle = "AI and Simulation of Behaviour Conference",
 year = "1974",
 pages = "6379"
+@article{Dowe96,
+ author = "Dowek, Gilles",
+ title = {{A TypeFree Formalization of Mathematics Where Proofs are
+ Objects}},
+ journal = "LNCS",
+ volume = "1512",
+ year = "1996",
+ pages = "88111",
+ abstract =
+ "We present a firstorder typefree axiomatization of mathematics
+ where proofs are objects in the sense of HeytingKolmogorov functional
+ interpretation. The consistency of this theory is open.",
+ paper = "Dowe96.pdf"
}
\end{chunk}
\index{de Bruijn, N.G.}
+\index{Harrison, John}
\begin{chunk}{axiom.bib}
@incollection{Brui94a,
 author = "de Bruijn, N.G.",
 title = {{The Mathematical Vernacular, a Language for Mathematics
 with Typed Sets}},
 booktitle = "Selected Papers on Automath",
 pages = "865935",
 year = "1994",
 publisher = "NorthHolland",
 link = "\url{https://pure.tue.nl/ws/files/2073504/610209.pdf}",
 paper = "Brui94a.pdf"
+@article{Harr06,
+ author = "Harrison, John",
+ title = {{Proof Style}},
+ journal = "LNCS",
+ volume = "1512",
+ year = "2006",
+ pages = "154172",
+ abstract =
+ "We are concerned with how computer theorem provers should expect
+ users to communicate proofs to them. There are many stylistic choices
+ that still allow the machine to generate a completely formal proof
+ object. The most obvious choice is the amount of guidance required
+ from the user, or from the machine perspective, the degree of
+ automation provided. But another important consideration, which we
+ consider particularly significant, is the bias towards a
+ 'procedural' or 'declarative' proof style. We will explore this
+ choice in depth, and discuss the strengths and weaknesses of
+ declarative and procedural styles for proofs in pure mathematics and
+ for verification applications. We conclude with a brief summary of
+ our own experiments in trying to combine both approaches.",
+ paper = "Harr06.pdf"
}
\end{chunk}
\index{Elbers, Hugo Johannes}
+\index{Jones, Alex}
+\index{Luo, Zhaohui}
+\index{Soloviev, Sergei}
\begin{chunk}{axiom.bib}
@phdthesis{Elbe98,
 author = "Elbers, Hugo Johannes",
 title = {{Connecting Informal and Formal Mathematics}},
 year = "1998",
 school = "Technische Universiteit Eindhoven",
 paper = "Elbe98.pdf"
+@article{Jone96,
+ author = "Jones, Alex and Luo, Zhaohui and Soloviev, Sergei",
+ title = {{Some Algorithmic and ProofTheoretical Aspects of
+ Coercive Subtyping}},
+ journal = "LNCS",
+ volume = "1512",
+ year = "1996",
+ pages = "173195",
+ abstract =
+ "Coercive subtyping offers a conceptually simple but powerful
+ framework to understand subtyping and subset relationships in type
+ theory. In this paper we study some of its prooftheoretic and
+ computational properties.",
+ paper = "Jone96.pdf"
}
\end{chunk}
\index{Bundy, Alan}
+\index{Naraschewski, Wolfgang}
+\index{Nipkow, Tobias}
\begin{chunk}{axiom.bib}
@incollection{Bund91,
 author = "Bundy, Alan",
 title = {{A Science of Reasoning (Extended Abstract)}},
 booktitle = "Computational Logic: Essays in Honor of Alan
 Robinson",
 year = "1991",
 publisher = "MIT Press",
 abstract =
 "How can we understand reasoning in general and mathematical proofs
 in particular? It is argued that a highlevel understanding of proofs
 is needed to complement the lowlevel understanding provided by
 Logic. A role for computation is proposed to provide this highlevel
 understanding, namely by the association of proof plans with
 proofs. Criteria are given for assessing the association of a proof
 plan with a proof.",
 paper = "Bund91.pdf"
+@article{Nara99,
+ author = "Naraschewski, Wolfgang and Nipkow, Tobias",
+ title = {{Type Inference Verified: Algorithm W in Isabelle/HOL}},
+ journal = "LNCS",
+ volume = "1512",
+ year = "1999",
+ pages = "317332",
+ paper = "Nara99.pdf"
}
\end{chunk}
\index{Daly, Timothy}
\index{Botch, Mark}
+\index{Constable, R.L.}
+\index{Knoblock, T.B.}
+\index{Gates, J.L.}
\begin{chunk}{axiom.bib}
@misc{Daly17,
 author = "Daly, Timothy and Botch, Mark",
 title = {{Axiom Developer Website}},
 link = "\url{http://axiomdeveloper.org}",
 year = "2017"
+@article{Cons85a,
+ author = "Constable, R.L. and Knoblock, T.B. and Gates, J.L.",
+ title = {{Writing Programs that Construct Proofs}},
+ journal = "J. of Automated Reasoning",
+ volume = "1",
+ number = "3",
+ pages = "285326",
+ year = "1985",
+ abstract =
+ "When we learn mathematics, we learn more than definitions and
+ theorems. We learn techniques of proof. In this paper, we describe
+ a particular way to express these techniques and incorporate them
+ into formal theories and into computer systems used to build such
+ theories. We illustrate the methods as they were applied in the
+ $\lambda$PRL system, essentially using the ML programming
+ language from Edinburgh LCF [23] as the formalised
+ metalanguage. We report our experience with such an approach
+ emphasizing the ideas that go beyond the LCF work, such as
+ transformation tactics and special purpose reasoners. We also show
+ how the validity of tactics can be guaranteed. The introduction
+ places the work in historical context and the conclusion briefly
+ describes plans to carry the methods further. The majority of the
+ paper presents the $\lambda$PRL approach in detail.",
+ paper = "Cons85a.pdf"
}
\end{chunk}
\index{SpectorZabusky, Antal}
\index{Breitner, Joachim}
\index{Rizkallah, Christine}
\index{Weirich, Stephanie}
+\index{Trybulec, Zinaida}
+\index{Swieczkowska, Halina}
\begin{chunk}{axiom.bib}
@inproceedings{Spec18,
 author = "SpectorZabusky, Antal and Breitner, Joachim and
 Rizkallah, Christine and Weirich, Stephanie",
 title = {{Total Haskell is Reasonable Coq}},
 booktitle = "ACM SIGPLAN Int. Conf. on Certified Programs and
 Proofs",
 publisher = "ACM",
 year = "2018",
 abstract =
 "We would like to use the Coq proof assistant to mechanically
 verify properites of Haskell programs. To that end, we present a
 tool, named {\tt hstocoq}, that translates total Haskell
 programs into Coq programs via a shallow embedding. We apply our
 tool in three case studies  a lawful {\tt Monad} instance,
 ``Hutton's razor'', and an existing data structure library  and
 prove their correctness. These examples show that this approach is
 viable: both that {\tt hstocoq} applies to existing Haskell
 code, and that the output it produces is amenable to
 verification.",
 paper = "Spec18.pdf"
+@article{Tryb92,
+ author = "Trybulec, Zinaida and Swieczkowska, Halina",
+ title = {{Some Remarks on The Language of Mathematical Texts}},
+ journal = "Studies in Logic, Grammar and Rhetoric",
+ volume = "10/11",
+ pages = "103124",
+ year = "1992",
+ paper = "Tryb92.pdf"
+}
+
+\end{chunk}
+
+\index{Traytel, Bmytro}
+\begin{chunk}{axiom.bib}
+@misc{Tray10,
+ author = "Traytel, Bmytro",
+ title = {{Extensions of a Type Inference Algorithm with Coerce Subtyping}},
+ school = "Der Technischen Universitat Munchen",
+ year = "2010",
+ abstract =
+ "Subtyping with coercion semantics allows a type inference system to
+ correct some illtyped programs by the automatic insertion of
+ implicit type conversions at runtime. This simplifies programmer’s
+ life but has its price: the general typability problem for given base
+ type subtype dependencies is NPcomplete. Nevertheless, if the given
+ coercions define an order on types with certain properties, the
+ problem behaves in a sane way in terms of complexity. This thesis
+ presents an algorithm that can be used to extend HindleyMilner type
+ inference with coercive subtyping assuming a given partial order on
+ base types. Especially, we discuss restrictions on the subtype
+ dependencies that are necessary to achieve an efficient
+ implementation. Examples of problems that occur if these restrictions
+ are not met are given. The result of these considerations is that the
+ algorithm is complete if the given base type poset is a disjoint union
+ of lattices. Furthermore, the interaction of subtyping with type
+ classes is addressed. The algorithm that is extended to deal with
+ type classes requires even a stronger restriction to assure
+ completeness. An MLimplementation of the presented algorithm is used
+ in the generic proof assistant Isabelle.",
+ paper = "Tray10.pdf"
+}
+
+\end{chunk}
+
+\index{Luo, Zhaohui}
+\index{Soloviev, Sergei}
+\begin{chunk}{axiom.bib}
+@article{Luox99,
+ author = "Luo, Zhaohui and Soloviev, Sergei",
+ title = {{Dependent Coercions}},
+ journal = "Electr. Notes Theor. Comput. Sci.",
+ volume = "29",
+ year = "1999",
+ pages = "152168",
+ abstract =
+ "A notion of dependent coercion is introduced and studied in the
+ context of depen dent type theories. It extends our earlier work on
+ coercive subtyping into a uniform framework which increases the
+ expressive power with new applications. A dependent coercion
+ introduces a subtyping relation between a type and a family of types
+ in that an object of the type is mapped into one of the types in the
+ family. We present the formal framework, discuss its metatheory, and
+ consider applications such as its use in functional programming with
+ dependent types.",
+ paper = "Luox99.pdf"
}
\end{chunk}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 6e019b4..54ebd7c 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5862,6 +5862,8 @@ books/bookvolbib add references
books/bookvolbib add references
20171202.01.tpd.patch
books/bookvolbib add references
+20171206.01.tpd.patch
+books/bookvolbib add references

1.9.1