From 63557134b562927f78568829ce795f92f75f7880 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Sun, 14 Jan 2018 00:06:54 0500
Subject: [PATCH] books/bookvolbib add references
MIMEVersion: 1.0
ContentType: text/plain; charset=UTF8
ContentTransferEncoding: 8bit
Goal: Proving Axiom Correct
\index{Coer, Claudio Sacerdoti}
\index{Tassi, Enrico}
\begin{chunk}{axiom.bib}
@inproceedings{Aspe11a,
author = "Coer, Claudio Sacerdoti and Tassi, Enrico",
title = {{Nonuniform Coercions via Unification Hints}},
booktitle = "Proc. Types for Proofs and Programs",
volume = "53",
pages = "1926",
year = "2011",
abstract =
"We introduce the notion of nonuniform coercion, which is the
promotion of a value of one type to an enriched value of a different
type via a nonuniform procedure. Nonuniform coercions are a
generalization of the (uniform) coercions known in the literature and
they arise naturally when formalizing mathematics in an higher order
interactive theorem prover using convenient devices like canonical
structures, type classes or unification hints. We also show how
nonuniform coercions can be naturally implemented at the user level in
an interactive theorem prover that allows unification hints.",
paper = "Aspe11a.pdf"
}
\end{chunk}
\index{Asperti, Andrea}
\index{Ricciotti, Wilmer}
\index{Coer, Claudio Sacerdoti}
\index{Tassi, Enrico}
\begin{chunk}{axiom.bib}
@article{Aspe09a,
author = "Asperti, Andrea and Ricciotti, Wilmer and Coer, Claudio
Sacerdoti and Tassi, Enrico",
title = {{Hints in Unification}},
journal = "LNCS",
volume = "5674",
pages = "8498",
year = "2009",
isbn = "9783642033582",
abstract =
"Several mechanisms such as Canonical Structures, Type Classes, or
Pullbacks have been recently introduced with the aim to improve the
power and flexibility of the type inference algorithm for interactive
theorem provers. We claim that all these mechanisms are particular
instances of a simpler and more general technique, just consisting in
providing suitable hints to the unification procedure underlying type
inference. This allows a simple, modular and not intrusive
implementation of all the above mentioned techniques, opening at the
same time innovative and unexpected perspectives on its possible
applications.",
paper = "Aspe09a.pdf"
}
\end{chunk}
\index{Asperti, Andrea}
\index{Tassi, Enrico}
\begin{chunk}{axiom.bib}
@article{Aspe10,
author = "Asperti, Andrea and Tassi, Enrico",
title = {{Smart Matching}},
journal = "LNCS",
volume = "6167",
pages = "263277",
year = "2010",
isbn = "9783642141287",
abstract =
"One of the most annoying aspects in the formalization of mathematics
is the need of transforming notions to match a given, existing
result. This kind of transformations, often based on a conspicuous
background knowledge in the given scientific domain (mostly expressed
in the form of equalities or isomorphisms), are usually implicit in
the mathematical discourse, and it would be highly desirable to obtain
a similar behavior in interactive provers. The paper describes the
superpositionbased implementation of this feature inside the Matita
interactive theorem prover, focusing in particular on the so called
smart application tactic, supporting smart matching between a goal and
a given result.",
paper = "Aspe10.pdf"
}
\end{chunk}
\index{Asperti, Andrea}
\index{Ricciotti, Wilmer}
\index{Coer, Claudio Sacerdoti}
\index{Tassi, Enrico}
\begin{chunk}{axiom.bib}
@inproceedings{Aspe09b,
author = "Asperti, Andrea and Ricciotti, Wilmer and Coer, Claudio
Sacerdoti and Tassi, Enrico",
title = {{A New Type for Tactics}},
booktitle = "SIGSAM PLMMS 2009",
publisher = "ACM",
year = "2009",
isbn = "9781605587356",
abstract =
"The type of tactics in all (procedural) proof assistants is (a
variant of) the one introduced in LCF. We discuss why this is
inconvenient and we propose a new type for tactics that 1) allows the
implementation of more clever tactics; 2) improves the implementation
of declarative languages on top of procedural ones; 3) allows for
better proof structuring; 4) improves proof automation; 5) allows
tactics to rearrange and delay the goals to be proved (e.g. in case of
side conditions or PVS subtyping judgements).",
paper = "Aspe09b.pdf"
}
\end{chunk}
\index{Asperti, Andrea}
\index{Tassi, Enrico}
\begin{chunk}{axiom.bib}
@inproceedings{Aspe07,
author = "Asperti, Andrea and Tassi, Enrico",
title = {{Higher Order Proof Reconstruction from
Paramodulationbased Refutations: The Unit Equality Case}},
booktitle = "MKM 2007",
year = "2007",
abstract =
"In this paper we address the problem of reconstructing a higher
order, checkable proof object starting from a proof trace left by a
first order automatic proof searching procedure, in a restricted
equational framework. The automatic procedure is based on
superposition rules for the unit equality case. Proof transformation
techniques aimed to improve the readability of the final proof are
discussed.",
paper = "Aspe07.pdf"
}
\end{chunk}
\index{Asperti, Andrea}
\index{Coen, Claudio Sacerdoti}
\index{Tassi, Enrico}
\index{Zacchiroli, Stefano}
\begin{chunk}{axiom.bib}
@inproceedings{Aspe06,
author = "Asperti, Andrea and Coen, Claudio Sacerdoti and
Tassi, Enrico and Zacchiroli, Stefano",
title = {{Crafting a Proof Assistant}},
booktitle = "Proc. Types 2006: Conf. of the Types Project",
year = "2006",
abstract =
"Proof assistants are complex applications whose develop ment has
never been properly systematized or documented. This work is a
contribution in this direction, based on our experience with the
devel opment of Matita: a new interactive theorem prover based—as
Coq—on the Calculus of Inductive Constructions (CIC). In particular,
we analyze its architecture focusing on the dependencies of its
components, how they implement the main functionalities, and their
degree of reusability. The work is a first attempt to provide a ground
for a more direct com parison between different systems and to
highlight the common functionalities, not only in view of
reusability but also to encourage a more systematic comparison of
different softwares and architectural solutions.",
paper = "Aspe06.pdf"
}
\end{chunk}
\index{Asperti, Andrea}
\index{Coen, Claudio Sacerdoti}
\index{Tassi, Enrico}
\index{Zacchiroli, Stefano}
\begin{chunk}{axiom.bib}
@article{Aspe07a,
author = "Asperti, Andrea and Coen, Claudio Sacerdoti and Tassi, Enrico
and Zacchiroli, Stefano",
title = {{User Interaction with the Matita Proof Assistant}},
journal = "J. of Automated Reasoning",
volume = "39",
number = "2",
pages = "109139",
abstract =
"Matita is a new, documentcentric, tacticbased interactive theorem
prover. This paper focuses on some of the distinctive features of the
user interaction with Matita, characterized mostly by the organization
of the library as a searchable knowledge base, the emphasis on a
highquality notational rendering, and the complex interplay between
syntax, presentation, and semantics.",
paper = "Aspe07a.pdf"
}
\end{chunk}
\index{Coen, Claudio Sacerdoti}
\index{Tassi, Enrico}
\index{Zacchiroli, Stefano}
\begin{chunk}{axiom.bib}
@inproceedings{Coen06,
author = "Coen, Claudio Sacerdoti and Tassi, Enrico and
Zacchiroli, Stefano",
title = {{Tinycals: Step by Step Teacticals}},
booktitle = "Proc. User Interfaces for Theorem Provers",
year = "2006",
pages = "125142",
abstract =
"Most of the stateoftheart proof assistants are based on procedural
proof languages, scripts, and rely on LCF tacticals as the primary
tool for tactics composition. In this paper we discuss how these
ingredients do not interact well with user interfaces based on the
same interaction paradigm of Proof General (the de facto standard in
this field), identifying in the coarsegrainedness of tactical
evaluation the key problem. We propose tinycals as an alternative to a
subset of LCF tacticals, showing that the user does not experience the
same problem if tacticals are evaluated in a more finegrained
manner. We present the formal operational semantics of tinycals as
well as their implementation in the Matita proof assistant.",
paper = "Coen06.pdf"
}
\end{chunk}
\index{Padovani, Luca}
\index{Zacchiroli, Stefano}
\begin{chunk}{axiom.bib}
@inproceedings{Pado06,
author = "Padovani, Luca and Zacchiroli, Stefano",
title = {{From Notation to Semantics: There and Back Again}},
booktitle = "5th Conf. on Mathematical Knowledge Management",
year = "2006",
abstract =
"Mathematical notation is a structured, open, and ambiguous
language. In order to support mathematical notation in MKM
applications one must necessarily take into account presentational as
well as semantic aspects. The former are required to create a
familiar, comfortable, and usable interface to interact with. The
latter are necessary in order to process the information
meaningfully. In this paper we investigate a framework for dealing
with mathematical notation in a meaningful, extensible way, and we
show an effective instantiation of its architecture to the field of
interactive theorem proving. The framework builds upon wellknown
concepts and widelyused technologies and it can be easily adopted by
other MKM applications.",
paper = "Pado06.pdf"
}
\end{chunk}
\index{Asperti, Andrea}
\index{Guidi, Ferruccio}
\index{Coen, Claudio Sacerdoti}
\index{Tassi, Enrico}
\index{Zacchiroli, Stefano}
\begin{chunk}{axiom.bib}
@article{Aspe04,
author = "Asperti, Andrea and Guidi, Ferruccio and Coen, Claudio Sacerdoti
and Tassi, Enrico and Zacchiroli, Stefano",
title = {{A Content Based Mathematical Search Engine: Whelp}},
journal = "LNCS",
volume = "3839",
year = "2004",
pages = "1732",
isbn = "3540314288",
abstract =
"The prototype of a content based search engine for mathematical
knowledge supporting a small set of queries requiring matching and/or
typing operations is described. The prototype, called Whelp, exploits
a metadata approach for indexing the information that looks far more
flexible than traditional indexing techniques for structured
expressions like substitution, discrimination, or context trees. The
prototype has been instantiated to the standard library of the Coq
proof assistant extended with many user contributions.",
paper = "Aspe04.pdf"
}
\end{chunk}
\index{Coen, Claudio Sacerdoti}
\index{Zacchiroli, Stefano}
\begin{chunk}{axiom.bib}
@article{Coen04,
author = "Coen, Claudio Sacerdoti and Zacchiroli, Stefano",
title = {{Efficient Ambiguous Parsing of Mathematical Formulae}},
journal = "LNCS",
volume = "3119",
pages = "347362",
year = "2004",
isbn = "3540230297",
abstract =
"Mathematical notation has the characteristic of being ambiguous:
operators can be overloaded and information that can be deduced is
often omitted. Mathematicians are used to this ambiguity and can
easily disambiguate a formula making use of the context and of their
ability to find the right interpretation.
Software applications that have to deal with formulae usually avoid
these issues by fixing an unambiguous input notation. This solution is
annoying for mathematicians because of the resulting tricky syntaxes
and becomes a show stopper to the simultaneous adoption of tools
characterized by different input languages.
In this paper we present an efficient algorithm suitable for ambiguous
parsing of mathematical formulae. The only requirement of the
algorithm is the existence of a 'validity' predicate over abstract
syntax trees of incomplete formulae with placeholders. This
requirement can be easily fulfilled in the applicative area of
interactive proof assistants, and in several other areas of
Mathematical Knowledge Management.",
paper = "Coen04.pdf"
}
\end{chunk}
\index{Grabm\"uller, Martin}
\begin{chunk}{axiom.bib}
@misc{Grab06a,
author = "Grabmuller, Martin",
title = {{Algorithm W Step by Step}},
year = "2006",
link = "\url{http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7733&rep=rep1&type=pdf}",
abstract =
"In this paper we develop a complete implementation of the classic
algoirhtm W for HinleyMilner polymorphic type inference in Haskell",
paper = "Grab06a.pdf"
}
\end{chunk}
\index{Hoare, C.A.R}
\begin{chunk}{axiom.bib}
@article{Hoar87,
author = "Hoare, C.A.R",
title = {{An Overview of Some Formal Methods for Program Design}},
journal = "Computer",
year = "1987",
volume = "20",
number = "9",
paper = "Hoar87.pdf"
}
\end{chunk}
\index{Bowen, Jonathan P.}
\index{Hinchey, Michael G.}
\begin{chunk}{axiom.bib}
@article{Bowe95,
author = "Bowen, Jonathan P. and Hinchey, Michael G.",
title = {{Seven More Myths of Formal Methods}},
journal = "IEEE Software",
volume = "12",
number = "4",
pages = "3441",
year = "1995",
abstract =
"New myths about formal methods are gaining tacit acceptance both
outside and inside the systemdevelopment community. The authors
address and dispel these myths based on their observations of
industrial projects. The myths include: formal methods delay the
development process; they lack tools; they replace traditional
engineering design methods; they only apply to software; are
unnecessary; not supported; and formal methods people always use
formal methods.",
paper = "Bowe95.pdf",
keywords = "printed"
}
\end{chunk}
\index{McBride, Conor}
\begin{chunk}{axiom.bib}
@phdthesis{Mcbr99,
author = "McBride, Conor",
title = {{Dependently Typed Functional Programs and their Proofs}},
school = "University of Edinburgh",
year = "1999",
link = "\url{http://strictlypositive.org/thesis.pdf}",
abstract =
"Research in dependent type theories has, in the past, concentrated on
its use in the presentation of theorems and theoremproving. This
thesis is concerned mainly with the exploitation of the computational
aspects of type theory for programming, in a context where the
properties of programs may readily be specified and established. In
particular, it develops technology for programming with dependent
inductive families of datatypes and proving those programs correct. It
demonstrates the considerable advantage to be gained by indexing data
structures with pertinent characteristic information whose soundness
is ensured by typechecking, rather than human effort.
Type theory traditionally presents safe and terminating computation on
inductive datatypes by means of elimination rules which serve as
induction principles and, via their associated reduction behaviour,
recursion operators. In the programming language arena, these appear
somewhat cumbersome and give rise to unappealing code, complicated by
the inevitable interaction between case analysis on dependent types
and equational reasoning on their indices which must appear explicitly
in the terms. Thierry Coquand's proposal to equip type theory directly
with the kind of pattern matching notation to which functional
programmers have become used to over the past three decades offers a
remedy to many of these difficulties. However, the status of pattern
matching relative to the traditional elimination rules has until now
been in doubt. Pattern matching implies the uniqueness of identity
proofs, which Martin Hofmann showed underivable from the conventiaonal
definition of equality. This thesis shows that the adoption of this
uniqueness as axiomatic is sufficient to make pattern matching
admissible.
A datatype's elimination rule allows abstraction only over the whole
inductively defined family. In order to support pattern matching, the
application of such rules to specific instances of dependent families
has been systematised. The underlying analysis extends beyond
datatypes to other rules of a similar second order character,
suggesting they may have other roles to play in the specification,
verification and, perhaps, derivation of programs. The technique
developed shifts the specificity from the instantiation of the type's
indices into equational constraints on indices freely chosen, allowing
the elimination rule to be applied.
Elimination by this means leaves equational hypotheses in the
resulting subgoals, which must be solved if further progress is to be
made. The firstorder unification algorithm for constructor forms in
simmple types presented in [McB96] has been extended to cover
dependent datatypes as well, yielding completely automated solution of
a class of problems which can be syntactically defined.
The justification and operation of these techniques requires the
machine to construct and exploit a standardised collection of
auxiliary lemmas for each datatype. This is greatly facilitated by two
technical developments of interest in their own right:
\begin{itemize}
\item a more convenient definition of equality, with a relaxed
formulation rule allowing elements of different types to be compared,
but nonetheless equivalent to the usual equality plus the axiom of
uniqueness
\item a type theory, OLEG, which incorporates incomplete objects,
accounting for their 'holes' entirely within the typing judgments and,
novelly, not requiring any notion of explicit substitution to manage
their scopes.
\end{itemize}
A substantial prototype has been implemented, extending the proof
assistant LEGO. A number of programs are developed by way of
example. Chiefly, the increased expressivity of dependent datatypes is
shown to capture a standard firstorder unification algorithm within
the class of structurally recursive programs, removing any need for a
termination argument. Furthermore, the use of elimination rules in
specifying the components of the program simplifies significantly its
correctness proof.",
paper = "Mcbr99.pdf",
keywords = "printed"
}
\end{chunk}

books/axiom.bib  663 ++++++++++++++++++++++++++++++
books/bookvolbib.pamphlet  763 +++++++++++++++++++++++++++++++++++
changelog  2 +
patch  559 ++++++++++++++++++++
src/axiomwebsite/patches.html  2 +
5 files changed, 1615 insertions(+), 374 deletions()
diff git a/books/axiom.bib b/books/axiom.bib
index 76b00af..0812108 100644
 a/books/axiom.bib
+++ b/books/axiom.bib
@@ 1767,7 +1767,7 @@ paper = "Brea89.pdf"
algebraic algorithms at hand and a much better understanding of data
structures and programming constructs than only a few years ago.",
paper = "Loos74.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@book{Loos92,
@@ 2157,7 +2157,8 @@ paper = "Brea89.pdf"
author = "Anonymous",
title = {{The QED Manifesto}},
link = "\url{}",
 paper = "QED94.txt"
+ paper = "QED94.txt",
+ keywords = "printed"
}
@InCollection{Rect89,
@@ 2176,7 +2177,7 @@ paper = "Brea89.pdf"
general patterns rather than producing specific formulas understood in
advance. Furthermore, the range of algebraic constucts used in such
calculations is very wide.",
 keywords = "axiomref"
+ keywords = "axiomref, printed"
}
@article{Reed97,
@@ 6947,6 +6948,84 @@ paper = "Brea89.pdf"
paper = "Yous04.pdf"
}
+@article{Aspe04,
+ author = "Asperti, Andrea and Guidi, Ferruccio and Coen, Claudio Sacerdoti
+ and Tassi, Enrico and Zacchiroli, Stefano",
+ title = {{A Content Based Mathematical Search Engine: Whelp}},
+ journal = "LNCS",
+ volume = "3839",
+ year = "2004",
+ pages = "1732",
+ isbn = "3540314288",
+ abstract =
+ "The prototype of a content based search engine for mathematical
+ knowledge supporting a small set of queries requiring matching and/or
+ typing operations is described. The prototype, called Whelp, exploits
+ a metadata approach for indexing the information that looks far more
+ flexible than traditional indexing techniques for structured
+ expressions like substitution, discrimination, or context trees. The
+ prototype has been instantiated to the standard library of the Coq
+ proof assistant extended with many user contributions.",
+ paper = "Aspe04.pdf"
+}
+
+@inproceedings{Aspe06,
+ author = "Asperti, Andrea and Coen, Claudio Sacerdoti and
+ Tassi, Enrico and Zacchiroli, Stefano",
+ title = {{Crafting a Proof Assistant}},
+ booktitle = "Proc. Types 2006: Conf. of the Types Project",
+ year = "2006",
+ abstract =
+ "Proof assistants are complex applications whose develop ment has
+ never been properly systematized or documented. This work is a
+ contribution in this direction, based on our experience with the
+ devel opment of Matita: a new interactive theorem prover based—as
+ Coq—on the Calculus of Inductive Constructions (CIC). In particular,
+ we analyze its architecture focusing on the dependencies of its
+ components, how they implement the main functionalities, and their
+ degree of reusability. The work is a first attempt to provide a ground
+ for a more direct com parison between different systems and to
+ highlight the common functionalities, not only in view of
+ reusability but also to encourage a more systematic comparison of
+ different softwares and architectural solutions.",
+ paper = "Aspe06.pdf"
+}
+
+@inproceedings{Aspe07,
+ author = "Asperti, Andrea and Tassi, Enrico",
+ title = {{Higher Order Proof Reconstruction from
+ Paramodulationbased Refutations: The Unit Equality Case}},
+ booktitle = "MKM 2007",
+ year = "2007",
+ abstract =
+ "In this paper we address the problem of reconstructing a higher
+ order, checkable proof object starting from a proof trace left by a
+ first order automatic proof searching procedure, in a restricted
+ equational framework. The automatic procedure is based on
+ superposition rules for the unit equality case. Proof transformation
+ techniques aimed to improve the readability of the final proof are
+ discussed.",
+ paper = "Aspe07.pdf"
+}
+
+@article{Aspe07a,
+ author = "Asperti, Andrea and Coen, Claudio Sacerdoti and Tassi, Enrico
+ and Zacchiroli, Stefano",
+ title = {{User Interaction with the Matita Proof Assistant}},
+ journal = "J. of Automated Reasoning",
+ volume = "39",
+ number = "2",
+ pages = "109139",
+ abstract =
+ "Matita is a new, documentcentric, tacticbased interactive theorem
+ prover. This paper focuses on some of the distinctive features of the
+ user interaction with Matita, characterized mostly by the organization
+ of the library as a searchable knowledge base, the emphasis on a
+ highquality notational rendering, and the complex interplay between
+ syntax, presentation, and semantics.",
+ paper = "Aspe07a.pdf"
+}
+
@article{Aspe09,
author = "Asperti, Andrea and Ricciotti, Wilmer and Coer, Claudio
Sacerdoti and Tassi, Enrico",
@@ 6969,6 +7048,72 @@ paper = "Brea89.pdf"
paper = "Aspe09.pdf"
}
+@article{Aspe09a,
+ author = "Asperti, Andrea and Ricciotti, Wilmer and Coer, Claudio
+ Sacerdoti and Tassi, Enrico",
+ title = {{Hints in Unification}},
+ journal = "LNCS",
+ volume = "5674",
+ pages = "8498",
+ year = "2009",
+ isbn = "9783642033582",
+ abstract =
+ "Several mechanisms such as Canonical Structures, Type Classes, or
+ Pullbacks have been recently introduced with the aim to improve the
+ power and flexibility of the type inference algorithm for interactive
+ theorem provers. We claim that all these mechanisms are particular
+ instances of a simpler and more general technique, just consisting in
+ providing suitable hints to the unification procedure underlying type
+ inference. This allows a simple, modular and not intrusive
+ implementation of all the above mentioned techniques, opening at the
+ same time innovative and unexpected perspectives on its possible
+ applications.",
+ paper = "Aspe09a.pdf"
+}
+
+@inproceedings{Aspe09b,
+ author = "Asperti, Andrea and Ricciotti, Wilmer and Coer, Claudio
+ Sacerdoti and Tassi, Enrico",
+ title = {{A New Type for Tactics}},
+ booktitle = "SIGSAM PLMMS 2009",
+ publisher = "ACM",
+ year = "2009",
+ isbn = "9781605587356",
+ abstract =
+ "The type of tactics in all (procedural) proof assistants is (a
+ variant of) the one introduced in LCF. We discuss why this is
+ inconvenient and we propose a new type for tactics that 1) allows the
+ implementation of more clever tactics; 2) improves the implementation
+ of declarative languages on top of procedural ones; 3) allows for
+ better proof structuring; 4) improves proof automation; 5) allows
+ tactics to rearrange and delay the goals to be proved (e.g. in case of
+ side conditions or PVS subtyping judgements).",
+ paper = "Aspe09b.pdf"
+}
+
+@article{Aspe10,
+ author = "Asperti, Andrea and Tassi, Enrico",
+ title = {{Smart Matching}},
+ journal = "LNCS",
+ volume = "6167",
+ pages = "263277",
+ year = "2010",
+ isbn = "9783642141287",
+ abstract =
+ "One of the most annoying aspects in the formalization of mathematics
+ is the need of transforming notions to match a given, existing
+ result. This kind of transformations, often based on a conspicuous
+ background knowledge in the given scientific domain (mostly expressed
+ in the form of equalities or isomorphisms), are usually implicit in
+ the mathematical discourse, and it would be highly desirable to obtain
+ a similar behavior in interactive provers. The paper describes the
+ superpositionbased implementation of this feature inside the Matita
+ interactive theorem prover, focusing in particular on the so called
+ smart application tactic, supporting smart matching between a goal and
+ a given result.",
+ paper = "Aspe10.pdf"
+}
+
@inproceedings{Aspe11,
author = "Asperti, Andrea and Ricciotti, Wilmer and Coer, Claudio
Sacerdoti and Tassi, Enrico",
@@ 6990,6 +7135,47 @@ paper = "Brea89.pdf"
level. In this paper, we give an account of the whole system, its
peculiarities and its main applications.",
paper = "Aspe11.pdf",
+ keywords = "printed"
+}
+
+@article{Aspe12,
+ author = "Asperti, Andrea and Ricciotti, Wilmer and Coer, Claudio
+ Sacerdoti and Tassi, Enrico",
+ title = {{A Bidirectional Refinement Algorithm for the Calculus
+ of (Co)Inductive Constructions}},
+ journal = "Logical Methods in Computer Science",
+ volume = "8",
+ pages = "149",
+ abstract =
+ "The paper describes the refinement algorithm for the Calculus of
+ (Co)Inductive Constructions (CIC) implemented in the interactive
+ theorem prover Matita. The refinement algorithm is in charge of giving
+ a meaning to the terms, types and proof terms directly written by the
+ user or generated by using tactics, decision procedures or general
+ automation. The terms are written in an 'external syntax' meant to be
+ user friendly that allows omission of information, untyped binders and
+ a certain liberal use of user defined subtyping. The refiner modifies
+ the terms to obtain related well typed terms in the internal syntax
+ understood by the kernel of the ITP. In particular, it acts as a type
+ inference algorithm when all the binders are untyped. The proposed
+ algorithm is bidirectional: given a term in external syntax and a
+ type expected for the term, it propagates as much typing information
+ as possible towards the leaves of the term. Traditional
+ monodirectional algorithms, instead, proceed in a bottom up way by
+ inferring the type of a subterm and comparing (unifying) it with the
+ type expected by its context only at the end. We propose some novel
+ bidirectional rules for CIC that are particularly effective. Among
+ the benefits of bidirectionality we have better error message
+ reporting and better inference of dependent types. Moreover, thanks to
+ bidirectionality, the coercion system for subtyping is more
+ effective and type inference generates simpler unification problems
+ that are more likely to be solved by the inherently incomplete higher
+ order unification algorithms implemented. Finally we introduce in the
+ external syntax the notion of vector of placeholders that enables to
+ omit at once an arbitrary number of arguments. Vectors of placeholders
+ allow a trivial implementation of implicit arguments and greatly
+ simplify the implementation of primitive and simple tactics.",
+ paper = "Aspe12.pdf"
}
@book{Appe17,
@@ 7042,7 +7228,8 @@ paper = "Brea89.pdf"
formal explanations can be executed at various stages of
completion. The most incomplete explanations resemble applicative
programs, the most complete are formal proofs.",
 paper = "Bate85.pdf"
+ paper = "Bate85.pdf",
+ keywords = "printed"
}
@book{Bish12,
@@ 7059,7 +7246,29 @@ paper = "Brea89.pdf"
booktitle = "Proc. 1996 New Security Paradigms Workshop",
publisher = "ACM",
year = "1996",
 paper = "Blak96.pdf"
+ paper = "Blak96.pdf",
+ keywords = "printed"
+}
+
+@article{Bowe95,
+ author = "Bowen, Jonathan P. and Hinchey, Michael G.",
+ title = {{Seven More Myths of Formal Methods}},
+ journal = "IEEE Software",
+ volume = "12",
+ number = "4",
+ pages = "3441",
+ year = "1995",
+ abstract =
+ "New myths about formal methods are gaining tacit acceptance both
+ outside and inside the systemdevelopment community. The authors
+ address and dispel these myths based on their observations of
+ industrial projects. The myths include: formal methods delay the
+ development process; they lack tools; they replace traditional
+ engineering design methods; they only apply to software; are
+ unnecessary; not supported; and formal methods people always use
+ formal methods.",
+ paper = "Bowe95.pdf",
+ keywords = "printed"
}
@article{Broo87,
@@ 7075,7 +7284,8 @@ paper = "Brea89.pdf"
tasks arise in representing the constructs in language. Past progress
has so reduced the accidental tasks that future progress now depends
upon addressing the essence.",
 paper = "Broo87.pdf"
+ paper = "Broo87.pdf",
+ keywords = "printed"
}
@techreport{Calu07,
@@ 7096,7 +7306,8 @@ paper = "Brea89.pdf"
differently. Programming gives mathematics a new form of
understanding. The computer is the driving force behind these
changes.",
 paper = "Calu07.pdf"
+ paper = "Calu07.pdf",
+ keywords = "printed"
}
@misc{Chli17a,
@@ 7238,6 +7449,76 @@ paper = "Brea89.pdf"
paper = "Chli17.pdf"
}
+@article{Coen04,
+ author = "Coen, Claudio Sacerdoti and Zacchiroli, Stefano",
+ title = {{Efficient Ambiguous Parsing of Mathematical Formulae}},
+ journal = "LNCS",
+ volume = "3119",
+ pages = "347362",
+ year = "2004",
+ isbn = "3540230297",
+ abstract =
+ "Mathematical notation has the characteristic of being ambiguous:
+ operators can be overloaded and information that can be deduced is
+ often omitted. Mathematicians are used to this ambiguity and can
+ easily disambiguate a formula making use of the context and of their
+ ability to find the right interpretation.
+
+ Software applications that have to deal with formulae usually avoid
+ these issues by fixing an unambiguous input notation. This solution is
+ annoying for mathematicians because of the resulting tricky syntaxes
+ and becomes a show stopper to the simultaneous adoption of tools
+ characterized by different input languages.
+
+ In this paper we present an efficient algorithm suitable for ambiguous
+ parsing of mathematical formulae. The only requirement of the
+ algorithm is the existence of a 'validity' predicate over abstract
+ syntax trees of incomplete formulae with placeholders. This
+ requirement can be easily fulfilled in the applicative area of
+ interactive proof assistants, and in several other areas of
+ Mathematical Knowledge Management.",
+ paper = "Coen04.pdf"
+}
+
+@inproceedings{Coen06,
+ author = "Coen, Claudio Sacerdoti and Tassi, Enrico and
+ Zacchiroli, Stefano",
+ title = {{Tinycals: Step by Step Teacticals}},
+ booktitle = "Proc. User Interfaces for Theorem Provers",
+ year = "2006",
+ pages = "125142",
+ abstract =
+ "Most of the stateoftheart proof assistants are based on procedural
+ proof languages, scripts, and rely on LCF tacticals as the primary
+ tool for tactics composition. In this paper we discuss how these
+ ingredients do not interact well with user interfaces based on the
+ same interaction paradigm of Proof General (the de facto standard in
+ this field), identifying in the coarsegrainedness of tactical
+ evaluation the key problem. We propose tinycals as an alternative to a
+ subset of LCF tacticals, showing that the user does not experience the
+ same problem if tacticals are evaluated in a more finegrained
+ manner. We present the formal operational semantics of tinycals as
+ well as their implementation in the Matita proof assistant.",
+ paper = "Coen06.pdf"
+}
+
+@inproceedings{Coen07a,
+ author = "Coen, Claudio Sacerdoti and Zacchiroli, Stefano",
+ title = {{Spurious Disambiguation Error Detection}},
+ booktitle = "MKM 2007 Mathematical Knowledge Management",
+ year = "2007",
+ abstract =
+ "The disambiguation approach to the input of formulae enables the user
+ to type correct formulae in a terse syntax close to the usual
+ ambiguous mathematical notation. When it comes to incorrect formulae
+ we want to present only errors related to the interpretation meant by
+ the user, hiding errors related to other interpretations (spurious
+ errors). We propose a heuristic to recognize spurious errors, which
+ has been integrated with our former efficient disambiguation
+ algorithm.",
+ paper = "Coen07a.pdf"
+}
+
@article{Coen10,
author = "Coen, Claudio Sacerdoti",
title = {{Declarative Representation of Proof Terms}},
@@ 7257,6 +7538,26 @@ paper = "Brea89.pdf"
paper = "Coen10.pdf"
}
+@inproceedings{Coen11,
+ author = "Coer, Claudio Sacerdoti and Tassi, Enrico",
+ title = {{Nonuniform Coercions via Unification Hints}},
+ booktitle = "Proc. Types for Proofs and Programs",
+ volume = "53",
+ pages = "1926",
+ year = "2011",
+ abstract =
+ "We introduce the notion of nonuniform coercion, which is the
+ promotion of a value of one type to an enriched value of a different
+ type via a nonuniform procedure. Nonuniform coercions are a
+ generalization of the (uniform) coercions known in the literature and
+ they arise naturally when formalizing mathematics in an higher order
+ interactive theorem prover using convenient devices like canonical
+ structures, type classes or unification hints. We also show how
+ nonuniform coercions can be naturally implemented at the user level in
+ an interactive theorem prover that allows unification hints.",
+ paper = "Coen11.pdf"
+}
+
@article{Cons85a,
author = "Constable, R.L. and Knoblock, T.B. and Gates, J.L.",
title = {{Writing Programs that Construct Proofs}},
@@ 7305,7 +7606,8 @@ paper = "Brea89.pdf"
year = "2017",
abstract = "Wherein existing methods for building secure systems are
examined and found wanting",
 paper = "Cyph17.pdf"
+ paper = "Cyph17.pdf",
+ keywords = "printed"
}
@article{Fass04,
@@ 7354,7 +7656,8 @@ paper = "Brea89.pdf"
inadequate use of measurement. Numerous empirical studies are flawed
because of their poor experimental design and lack of adherence to
proper measurement principles.",
 paper = "Fent93.pdf"
+ paper = "Fent93.pdf",
+ keywords = "printed"
}
@article{Fetz88,
@@ 7372,7 +7675,8 @@ paper = "Brea89.pdf"
those structures, are not. The success of program verification as a
generally applicable and completely reliable method for guaranteeing
program performance is not even a theoretical possibility.",
 paper = "Fetz88.pdf"
+ paper = "Fetz88.pdf",
+ keywords = "printed"
}
@book{Font16,
@@ 7394,7 +7698,8 @@ paper = "Brea89.pdf"
"With the advantage of more than 25 years' hindsight, this twentyfirst
century author looks askance at the 'crisis' in software practice and
expresses deep concern for a crisis in software research.",
 paper = "Glas94.pdf"
+ paper = "Glas94.pdf",
+ keywords = "printed"
}
@article{Glas02,
@@ 7405,7 +7710,20 @@ paper = "Brea89.pdf"
number = "8",
year = "2002",
pages = "1921",
 paper = "Glas02.pdf"
+ paper = "Glas02.pdf",
+ keywords = "printed"
+}
+
+@misc{Grab06a,
+ author = "Grabmuller, Martin",
+ title = {{Algorithm W Step by Step}},
+ year = "2006",
+ link = "\url{http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7733&rep=rep1&type=pdf}",
+ abstract =
+ "In this paper we develop a complete implementation of the classic
+ algoirhtm W for HinleyMilner polymorphic type inference in Haskell",
+ paper = "Grab06a.pdf",
+ keywords = "printed"
}
@article{Hall90,
@@ 7420,7 +7738,19 @@ paper = "Brea89.pdf"
"Formal methods are difficult, expensive, and not widely useful,
detractors say. Using a case study and other realworld examples, this
article challenges such common myths.",
 paper = "Hall80.pdf"
+ paper = "Hall80.pdf",
+ keywords = "printed"
+}
+
+@article{Hoar87,
+ author = "Hoare, Charles Antony Richard",
+ title = {{An Overview of Some Formal Methods for Program Design}},
+ journal = "Computer",
+ year = "1987",
+ volume = "20",
+ number = "9",
+ paper = "Hoar87.pdf",
+ keywords = "printed"
}
@article{Hoar96,
@@ 7442,7 +7772,8 @@ paper = "Brea89.pdf"
provide a conceptual framework and basic understanding to promote the
best of current practice, and point directions for future
improvement.",
 paper = "Hoar96.pdf"
+ paper = "Hoar96.pdf",
+ keywords = "printed"
}
@incollection{Lams00,
@@ 7473,7 +7804,8 @@ paper = "Brea89.pdf"
number = "1",
year = "1988",
pages = "327",
 paper = "Lind88.pdf"
+ paper = "Lind88.pdf",
+ keywords = "printed"
}
@inproceedings{Luox96,
@@ 7601,7 +7933,8 @@ paper = "Brea89.pdf"
that my theory no longer contains intuitionistic simple type theory as
it originally did. Instead, its proof theoretic strength should be
close to that of predicative analysis.",
 paper = "Mart73.pdf"
+ paper = "Mart73.pdf",
+ keywords = "printed"
}
@inproceedings{Mart79,
@@ 7630,7 +7963,89 @@ paper = "Brea89.pdf"
synthesis. Thus the correctness of a program written in the theory of
types is proved formally at the same time as it is being
synthesized.",
 paper = "Mart79.pdf"
+ paper = "Mart79.pdf",
+ keywords = "printed"
+}
+
+@phdthesis{Mcbr99,
+ author = "McBride, Conor",
+ title = {{Dependently Typed Functional Programs and their Proofs}},
+ school = "University of Edinburgh",
+ year = "1999",
+ link = "\url{http://strictlypositive.org/thesis.pdf}",
+ abstract =
+ "Research in dependent type theories has, in the past, concentrated on
+ its use in the presentation of theorems and theoremproving. This
+ thesis is concerned mainly with the exploitation of the computational
+ aspects of type theory for programming, in a context where the
+ properties of programs may readily be specified and established. In
+ particular, it develops technology for programming with dependent
+ inductive families of datatypes and proving those programs correct. It
+ demonstrates the considerable advantage to be gained by indexing data
+ structures with pertinent characteristic information whose soundness
+ is ensured by typechecking, rather than human effort.
+
+ Type theory traditionally presents safe and terminating computation on
+ inductive datatypes by means of elimination rules which serve as
+ induction principles and, via their associated reduction behaviour,
+ recursion operators. In the programming language arena, these appear
+ somewhat cumbersome and give rise to unappealing code, complicated by
+ the inevitable interaction between case analysis on dependent types
+ and equational reasoning on their indices which must appear explicitly
+ in the terms. Thierry Coquand's proposal to equip type theory directly
+ with the kind of pattern matching notation to which functional
+ programmers have become used to over the past three decades offers a
+ remedy to many of these difficulties. However, the status of pattern
+ matching relative to the traditional elimination rules has until now
+ been in doubt. Pattern matching implies the uniqueness of identity
+ proofs, which Martin Hofmann showed underivable from the conventiaonal
+ definition of equality. This thesis shows that the adoption of this
+ uniqueness as axiomatic is sufficient to make pattern matching
+ admissible.
+
+ A datatype's elimination rule allows abstraction only over the whole
+ inductively defined family. In order to support pattern matching, the
+ application of such rules to specific instances of dependent families
+ has been systematised. The underlying analysis extends beyond
+ datatypes to other rules of a similar second order character,
+ suggesting they may have other roles to play in the specification,
+ verification and, perhaps, derivation of programs. The technique
+ developed shifts the specificity from the instantiation of the type's
+ indices into equational constraints on indices freely chosen, allowing
+ the elimination rule to be applied.
+
+ Elimination by this means leaves equational hypotheses in the
+ resulting subgoals, which must be solved if further progress is to be
+ made. The firstorder unification algorithm for constructor forms in
+ simmple types presented in [McB96] has been extended to cover
+ dependent datatypes as well, yielding completely automated solution of
+ a class of problems which can be syntactically defined.
+
+ The justification and operation of these techniques requires the
+ machine to construct and exploit a standardised collection of
+ auxiliary lemmas for each datatype. This is greatly facilitated by two
+ technical developments of interest in their own right:
+ \begin{itemize}
+ \item a more convenient definition of equality, with a relaxed
+ formulation rule allowing elements of different types to be compared,
+ but nonetheless equivalent to the usual equality plus the axiom of
+ uniqueness
+ \item a type theory, OLEG, which incorporates incomplete objects,
+ accounting for their 'holes' entirely within the typing judgments and,
+ novelly, not requiring any notion of explicit substitution to manage
+ their scopes.
+ \end{itemize}
+
+ A substantial prototype has been implemented, extending the proof
+ assistant LEGO. A number of programs are developed by way of
+ example. Chiefly, the increased expressivity of dependent datatypes is
+ shown to capture a standard firstorder unification algorithm within
+ the class of structurally recursive programs, removing any need for a
+ termination argument. Furthermore, the use of elimination rules in
+ specifying the components of the program simplifies significantly its
+ correctness proof.",
+ paper = "Mcbr99.pdf",
+ keywords = "printed"
}
@misc{Mull13,
@@ 7643,7 +8058,29 @@ paper = "Brea89.pdf"
LCFstyle implementation of higherorder logic using Haskell as a
metalanguage. We discuss details of the logic implemented, kernel
design, and novel proof state and tactic representations.",
 paper = "Mull13.pdf"
+ paper = "Mull13.pdf",
+ keywords = "printed"
+}
+
+@inproceedings{Pado06,
+ author = "Padovani, Luca and Zacchiroli, Stefano",
+ title = {{From Notation to Semantics: There and Back Again}},
+ booktitle = "5th Conf. on Mathematical Knowledge Management",
+ year = "2006",
+ abstract =
+ "Mathematical notation is a structured, open, and ambiguous
+ language. In order to support mathematical notation in MKM
+ applications one must necessarily take into account presentational as
+ well as semantic aspects. The former are required to create a
+ familiar, comfortable, and usable interface to interact with. The
+ latter are necessary in order to process the information
+ meaningfully. In this paper we investigate a framework for dealing
+ with mathematical notation in a meaningful, extensible way, and we
+ show an effective instantiation of its architecture to the field of
+ interactive theorem proving. The framework builds upon wellknown
+ concepts and widelyused technologies and it can be easily adopted by
+ other MKM applications.",
+ paper = "Pado06.pdf"
}
@techreport{Pier97,
@@ 7813,7 +8250,8 @@ paper = "Brea89.pdf"
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"
+ paper = "Soze06.pdf",
+ keywords = "printed"
}
@article{Aban16,
@@ 7984,7 +8422,7 @@ paper = "Brea89.pdf"
by including parametric limits of integration and queries with side
conditions.",
paper = "Adam99.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@InProceedings{Adam01,
@@ 8007,7 +8445,7 @@ paper = "Brea89.pdf"
library. These examples provide proofs which are both illustrative and
applicable to genuine symbolic computation problems.",
paper = "Adam01.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@misc{Ager88,
@@ 8265,7 +8703,7 @@ paper = "Brea89.pdf"
is based on theorem templates, which provide formal specifications for
the algorithms.",
paper = "Ball98.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
@article{Ball99,
@@ 8298,7 +8736,7 @@ paper = "Brea89.pdf"
system on the tacticlevel of Isabelle and its integration into proof
procedures.",
paper = "Ball99.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@article{Bare01,
@@ 8339,7 +8777,7 @@ paper = "Brea89.pdf"
Some examples of communication forms are given that show how the
participants benefit",
paper = "Bare01.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
@article{Baue16,
@@ 8576,7 +9014,7 @@ paper = "Brea89.pdf"
software development process from the specification of requirements to
the finished system. These methos are potentially applicable to the
development of correct hardware systems as well",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@@ 8756,7 +9194,8 @@ paper = "Brea89.pdf"
for describing a hierarchy of Drecords in an incremental way. In
mixDrecs, fields can be only declared or they can be
redefined. MixDrecs can be extended by inheritance.",
 paper = "Boul00a.pdf"
+ paper = "Boul00a.pdf",
+ keywords = "printed"
}
@InProceedings{Boul99,
@@ 8786,7 +9225,7 @@ paper = "Brea89.pdf"
exactly the mathematical dependencies between different structures.
This may ease the achievement of proofs.",
paper = "Boul99.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@techreport{Boul94,
@@ 8989,7 +9428,7 @@ paper = "Brea89.pdf"
year = "1994",
volume = "125",
paper = "Brui68.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
@article{Buch97,
@@ 9000,7 +9439,8 @@ paper = "Brea89.pdf"
publisher = "SpringerVerlag",
pages = "220",
isbn = "9783211828441",
 paper = "Buch97.pdf"
+ paper = "Buch97.pdf",
+ keywords = "printed"
}
@article{Buch01,
@@ 9011,7 +9451,8 @@ paper = "Brea89.pdf"
number = "2",
pages = "247252",
year = "2001",
 paper = "Buch01.pdf"
+ paper = "Buch01.pdf",
+ keywords = "printed"
}
@misc{Buch00,
@@ 9076,7 +9517,8 @@ paper = "Brea89.pdf"
can be used for dening and proving properties of mathematical models
and algorithms, while a specially provided ``computing engine'' can
execute directly the logical description of these algorithms.",
 paper = "Buch03.pdf"
+ paper = "Buch03.pdf",
+ keywords = "printed"
}
@article{Buch16,
@@ 9255,7 +9697,8 @@ paper = "Brea89.pdf"
systems may be based on different logics, formalisms, data structures,
interfaces. A result of this work is illustrated by a prototype
implementation of an interface between Isabelle and Maple.",
 paper = "Calm95.pdf"
+ paper = "Calm95.pdf",
+ keywords = "printed"
}
@inproceedings{Calm96a,
@@ 9295,7 +9738,8 @@ paper = "Brea89.pdf"
wellknown examples. The needs and requirements for the Mathematics
Software Bus and its architecture are demonstrated through some
implementations of powerful interfaces between mathematical services.",
 paper = "Calm97a.pdf"
+ paper = "Calm97a.pdf",
+ keywords = "printed"
}
@book{Cann05,
@@ 9437,7 +9881,7 @@ paper = "Brea89.pdf"
year = "1991",
link = "\url{http://www.cs.cmu.edu/~emc/papers/Conference%20Papers/Analytica%20A%20Theorem%20Prover%20in%20Mathematica.pdf}",
paper = "Clar91.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
@article{Clar93,
@@ 9576,7 +10020,8 @@ paper = "Brea89.pdf"
as the program expressions of a pure functional lazy language:
variable, constructor, application, abstraction, case expressions,
and local let expressions.",
 paper = "Coqu93.pdf"
+ paper = "Coqu93.pdf",
+ keywords = "printed"
}
@article{Coqu96,
@@ 9658,7 +10103,7 @@ paper = "Brea89.pdf"
our claim that the Nuprl proof development system is especially well
suited to support this kind of mathematics.",
paper = "Cons98.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@book{Crol93,
@@ 9801,7 +10246,8 @@ paper = "Brea89.pdf"
make the formal verification process difficult to justify and manage.
It is felt that ease of formal verification should not dominate program
language design.",
 paper = "Demi79.pdf"
+ paper = "Demi79.pdf",
+ keywords = "printed"
}
@article{Denn00,
@@ 9964,7 +10410,7 @@ paper = "Brea89.pdf"
a modest cost. Our approach is based on retargeting the code generator
of the OpenAxiom compiler to the Poly/ML abstract machine.",
paper = "Dosr11.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@misc{Duns00,
@@ 10098,7 +10544,8 @@ paper = "Brea89.pdf"
foundation for mechanized mathematics. It is the basis for the logic
of IMPS, an Interactive Mathematical Proof System developed at The
MITRE Corporation.",
 paper = "Farm93b.pdf"
+ paper = "Farm93b.pdf",
+ keywords = "printed"
}
@article{Farm93a,
@@ 10210,7 +10657,7 @@ paper = "Brea89.pdf"
related approach to a version of a Bessel function algorithm for J0(x)
based on a recurrence.",
paper = "Fate03a.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
@book{Fitt90,
@@ 10522,7 +10969,7 @@ paper = "Brea89.pdf"
of verification conditions, harnesses to ensure more reliable
differential equation solvers, and verifiable lookup tables.",
paper = "Gott05.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@misc{Grab17,
@@ 10677,7 +11124,7 @@ paper = "Brea89.pdf"
reals which combines the rigour of a theorem prover with the power of
a computer algebra system.",
paper = "Harr94.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@techreport{Harr95,
@@ 10959,7 +11406,7 @@ paper = "Brea89.pdf"
algebra system and the relevance of this work for abstract functional
programming.",
paper = "Jack94.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@phdthesis{Jack95,
@@ 11066,7 +11513,7 @@ paper = "Brea89.pdf"
prototype, but can be straightforwardly scaled up to a practical
computer algebra system.",
paper = "Kali07.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@phdthesis{Kali09,
@@ 11150,7 +11597,7 @@ paper = "Brea89.pdf"
wellsuited for producing a highlevel verbalised explication as well
as for a lowlevel (machine checkable) calculuslevel proof.",
paper = "Kerb96.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@article{Kerb07,
@@ 11169,7 +11616,8 @@ paper = "Brea89.pdf"
providing a highlevel language, we argue that more should be learned
from the mathematical practice in order to improve the applicability
of formal systems.",
 paper = "Kerb07.pdf"
+ paper = "Kerb07.pdf",
+ keywords = "printed"
}
@article{Kome11,
@@ 11193,7 +11641,7 @@ paper = "Brea89.pdf"
OpenMath terms produced by a CAS in the calculus of Coq, as well as
viewing pure Coq terms in a simpler type system that is behind OpenMath.",
paper = "Kome11.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
@article{Kowa79,
@@ 11475,7 +11923,7 @@ paper = "Brea89.pdf"
times), and a comprehensive facility for defining conditionally
applicable transformations.",
paper = "Lond74.pdf",
 keywords = "axiomref"
+ keywords = "axiomref, printed"
}
@article{Mahb06,
@@ 11645,7 +12093,7 @@ paper = "Brea89.pdf"
disadvantages of these approaches. We also discuss some possible case
studies.",
paper = "Mart97.ps",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@book{Maso86,
@@ 11820,7 +12268,7 @@ paper = "Brea89.pdf"
functional language Haskell and implementing certain piece of
commutative algebra",
paper = "Mesh01.pdf",
 keywords = "axiomref"
+ keywords = "axiomref, printed"
}
@@ 11948,8 +12396,8 @@ paper = "Brea89.pdf"
tyhpes ({\tt Agda}). There are given several examples illustrating
particular points of implementing the approach of constructive
mathematics.",
 paper = "Mesh16a.pdf"

+ paper = "Mesh16a.pdf",
+ keywords = "printed"
}
@article{Mitc88,
@@ 12010,7 +12458,8 @@ paper = "Brea89.pdf"
these results to richer languages; a typechecking algorithm based on
$W$ is in fact already implemented and working, for the metalanguage ML
in the Edinburgh LCF system,",
 paper = "Miln78.pdf"
+ paper = "Miln78.pdf",
+ keywords = "printed"
}
@article{Miln84,
@@ 12149,7 +12598,7 @@ paper = "Brea89.pdf"
year = "2013",
link = "\url{http://ceurws.org/Vol1010/paper09.pdf}",
paper = "Neup13.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
@misc{Newc13,
@@ 12246,7 +12695,8 @@ paper = "Brea89.pdf"
title = {{Programming in MartinL\"of's Type Theory}},
year = "1990",
publisher = "Oxford University Press",
 paper = "Nord90.pdf"
+ paper = "Nord90.pdf",
+ keywords = "printed"
}
@misc{OCon15,
@@ 12341,7 +12791,8 @@ 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.pdf"
+ paper = "Pare93.pdf",
+ keywords = "printed"
}
@techreport{Pare94,
@@ 12522,7 +12973,8 @@ paper = "Brea89.pdf"
algorithm for partial type inference in the $omega$order polymorphic
$\lambda$calculus. We present an implementation in $\lambda$Prolog in
full.",
 paper = "Pfen88.pdf"
+ paper = "Pfen88.pdf",
+ keywords = "printed"
}
@techreport{Pfen89,
@@ 12675,7 +13127,7 @@ paper = "Brea89.pdf"
The paper shows an interesting way to decorate Axiom with pre and
postconditions.",
paper = "Poll98.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@misc{Poll99,
@@ 13370,7 +13822,8 @@ paper = "Brea89.pdf"
at RISC. In this talk, we want to present the current status of the
new implementation, in particular the new user interface of the
system.",
 paper = "Wind14.pdf"
+ paper = "Wind14.pdf",
+ keywords = "printed"
}
@article{Wind06,
@@ 19971,7 +20424,7 @@ paper = "Brea89.pdf"
introduce notations prepresentable and pnegligible where p denotes
precision, and show how this helps in our applications.",
paper = "Fate03.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
@misc{Fate15,
@@ 24058,7 +24511,7 @@ paper = "Brea89.pdf"
mathematical equality and with data structure equality, and to
explain how necessary it is to keep a clear distintion between the two.",
paper = "Dave02.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@misc{Dave07,
@@ 25235,7 +25688,7 @@ paper = "Brea89.pdf"
are inspired by the IMPS Interactive Mathematical Proof System and the
Axiom computer algebra system.",
paper = "Farm03.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@inproceedings{Fate79,
@@ 26593,7 +27046,7 @@ paper = "Brea89.pdf"
of computer algebra results proved formally in the HOL theorem prover
with the aid of Maple.",
paper = "Harr98.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@misc{Harr12,
@@ 28107,7 +28560,7 @@ paper = "Brea89.pdf"
and (iii) interface specifications which assist the verification of
pre and post conditions of implemented code.",
paper = "Kels00a.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@article{Kend01,
@@ 28212,7 +28665,7 @@ paper = "Brea89.pdf"
calculuslevel proof. We present an implementation of our ideas and
exemplify them using an automatically solved example.",
paper = "Kerb98.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@phdthesis{King70,
@@ 31778,7 +32231,8 @@ paper = "Brea89.pdf"
proving theorems. ITP grew out of a more general project  called
Symbolic Incidence Geometry  which is concerned with the problem of
the systematic use of the computer in incidence geometry.",
 paper = "Uebe94.pdf"
+ paper = "Uebe94.pdf",
+ keywords = "printed"
}
@misc{Unkn13,
@@ 33107,7 +33561,8 @@ paper = "Brea89.pdf"
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"
+ paper = "Bail96.pdf",
+ keywords = "printed"
}
@phdthesis{Bail98,
@@ 33165,7 +33620,8 @@ paper = "Brea89.pdf"
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"
+ paper = "Barr96.pdf",
+ keywords = "printed"
}
@article{Bart95,
@@ 33185,7 +33641,8 @@ paper = "Brea89.pdf"
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"
+ paper = "Bart95.pdf",
+ keywords = "printed"
}
@article{Bart72,
@@ 33244,7 +33701,7 @@ paper = "Brea89.pdf"
theorems. In this paper, we show how it can prove a series of lemmas
that lead to the Bernstein approximation theorem.",
paper = "Baue98.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
@article{Bees90,
@@ 33324,7 +33781,7 @@ paper = "Brea89.pdf"
algebra system. We show how the integrated system solves a problem
which could not be tackled by each single system alone.",
paper = "Bert98.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
@article{Bert95,
@@ 33417,7 +33874,8 @@ paper = "Brea89.pdf"
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"
+ paper = "Bove02.pdf",
+ keywords = "printed"
}
@inproceedings{Brad86,
@@ 33586,7 +34044,8 @@ paper = "Brea89.pdf"
of ``propositions as types'' (Section 14). Finally the survey will be
used to ventilate opinions and views in mathematics which are not
easily set down in more technical reports.",
 paper = "Brui94.pdf"
+ paper = "Brui94.pdf",
+ keywords = "printed"
}
@incollection{Brui94a,
@@ 33682,7 +34141,7 @@ paper = "Brea89.pdf"
practical importance of functors and show how they can be naturally
embedded into Mathematica.",
paper = "Buch96.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
@article{Buch14,
@@ 33817,7 +34276,7 @@ paper = "Brea89.pdf"
encoding, encryption, and knowledge sharing. The latter concerns the
semantic aspects of architectures for cooperative problem solving.",
paper = "Calm96.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
@article{Cant87,
@@ 33853,7 +34312,8 @@ paper = "Brea89.pdf"
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"
+ paper = "Carl02.pdf",
+ keywords = "printed"
}
@book{Char92,
@@ 33951,7 +34411,7 @@ paper = "Brea89.pdf"
challenge problems completely automatically. The axioms and inference
rules for constructing the proofs are also briefly discussed.",
paper = "Clar94.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
@article{Coen07,
@@ 33973,7 +34433,8 @@ paper = "Brea89.pdf"
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"
+ paper = "Coen07.pdf",
+ keywords = "printed"
}
@book{Cohn65,
@@ 34199,7 +34660,7 @@ paper = "Brea89.pdf"
its functionality as it appears to the user, and explain the design
issues and implementation techniques. REDLOG is available on the WWW.",
paper = "Dolz97b.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
@misc{blas01,
@@ 34241,7 +34702,8 @@ paper = "Brea89.pdf"
"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"
+ paper = "Dowe96.pdf",
+ keywords = "printed"
}
@misc{Duns01,
@@ 34271,7 +34733,8 @@ paper = "Brea89.pdf"
type system and discusses their merits and effectiveness. We conclude
by a brief comparison with similar developments using other theorem
provers.",
 paper = "Dute96.pdf"
+ paper = "Dute96.pdf",
+ keywords = "printed"
}
@article{Duva96a,
@@ 34535,7 +34998,8 @@ paper = "Brea89.pdf"
constructions in a straightforward way. This work has been
implemented in the Coq Proof Assistant and applied on nontrivial
examples.",
 paper = "Fill98.pdf"
+ paper = "Fill98.pdf",
+ keywords = "printed"
}
@misc{Fitc74,
@@ 34981,7 +35445,7 @@ paper = "Brea89.pdf"
consisting of type and algorithm schemata, algebraic algorithms and
theorems.",
paper = "Homa94.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@article{Homa96,
@@ 35001,7 +35465,7 @@ paper = "Brea89.pdf"
framework for the specification of symbolic mathematical problem
solving by cooperation of algorithms and theorems.",
paper = "Homa96.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
@book{Hous81,
@@ 35190,7 +35654,8 @@ paper = "Brea89.pdf"
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"
+ paper = "Jone96.pdf",
+ keywords = "printed"
}
@phdthesis{Kalk91,
@@ 35465,7 +35930,8 @@ paper = "Brea89.pdf"
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"
+ paper = "Kies03.pdf",
+ keywords = "printed"
}
@book{Knut92,
@@ 35792,7 +36258,7 @@ paper = "Brea89.pdf"
pages = "239239",
year = "2002",
paper = "Lint02.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
@article{Lisk77,
@@ 35924,7 +36390,8 @@ paper = "Brea89.pdf"
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"
+ paper = "Luox99.pdf",
+ keywords = "printed"
}
@book{Lutz90,
@@ 35966,7 +36433,8 @@ paper = "Brea89.pdf"
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"
+ paper = "Maga00.pdf",
+ keywords = "printed"
}
@article{Maga08,
@@ 36308,7 +36776,8 @@ paper = "Brea89.pdf"
volume = "1512",
year = "1999",
pages = "317332",
 paper = "Nara99.pdf"
+ paper = "Nara99.pdf",
+ keywords = "printed"
}
@article{Naud98,
@@ 36434,7 +36903,8 @@ paper = "Brea89.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"
+ paper = "Nipk02.pdf",
+ keywords = "printed"
}
@misc{OCAM14,
@@ 37157,7 +37627,7 @@ paper = "Brea89.pdf"
computation. We demonstrate our approach with the concrete
implementation in the $\Omega$MEGA system.",
paper = "Sorg00.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
@book{Stee90,
@@ 37221,7 +37691,8 @@ paper = "Brea89.pdf"
symbolic computation program REDUCE. The use of REDUCE in a
theoremproving context is described in detail. Sample proofs are
given with data on computation time per step on an IBM4381.",
 paper = "Supp89.pdf"
+ paper = "Supp89.pdf",
+ keywords = "printed"
}
@techreport{Swee86,
@@ 37306,7 +37777,8 @@ paper = "Brea89.pdf"
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"
+ paper = "Tray10.pdf",
+ keywords = "printed"
}
@misc{Tryb02,
@@ 37501,7 +37973,8 @@ paper = "Brea89.pdf"
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"
+ paper = "Wied03.pdf",
+ keywords = "printed"
}
@misc{Wiki14a,
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index a03fab5..3f392ad 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 2554,7 +2554,7 @@ paper = "Brea89.pdf"
algebraic algorithms at hand and a much better understanding of data
structures and programming constructs than only a few years ago.",
paper = "Loos74.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 3062,7 +3062,8 @@ paper = "Brea89.pdf"
author = "Anonymous",
title = {{The QED Manifesto}},
link = "\url{}",
 paper = "QED94.txt"
+ paper = "QED94.txt",
+ keywords = "printed"
}
\end{chunk}
@@ 3087,7 +3088,7 @@ paper = "Brea89.pdf"
general patterns rather than producing specific formulas understood in
advance. Furthermore, the range of algebraic constucts used in such
calculations is very wide.",
 keywords = "axiomref"
+ keywords = "axiomref, printed"
}
\end{chunk}
@@ 9449,8 +9450,113 @@ when shown in factored form.
\section{Proving Axiom Correct  The Project} %%%%%%%%%%%%%%%%%%%%
\index{Asperti, Andrea}
+\index{Guidi, Ferruccio}
+\index{Coen, Claudio Sacerdoti}
+\index{Tassi, Enrico}
+\index{Zacchiroli, Stefano}
+\begin{chunk}{axiom.bib}
+@article{Aspe04,
+ author = "Asperti, Andrea and Guidi, Ferruccio and Coen, Claudio Sacerdoti
+ and Tassi, Enrico and Zacchiroli, Stefano",
+ title = {{A Content Based Mathematical Search Engine: Whelp}},
+ journal = "LNCS",
+ volume = "3839",
+ year = "2004",
+ pages = "1732",
+ isbn = "3540314288",
+ abstract =
+ "The prototype of a content based search engine for mathematical
+ knowledge supporting a small set of queries requiring matching and/or
+ typing operations is described. The prototype, called Whelp, exploits
+ a metadata approach for indexing the information that looks far more
+ flexible than traditional indexing techniques for structured
+ expressions like substitution, discrimination, or context trees. The
+ prototype has been instantiated to the standard library of the Coq
+ proof assistant extended with many user contributions.",
+ paper = "Aspe04.pdf"
+}
+
+\end{chunk}
+
+\index{Asperti, Andrea}
+\index{Coen, Claudio Sacerdoti}
+\index{Tassi, Enrico}
+\index{Zacchiroli, Stefano}
+\begin{chunk}{axiom.bib}
+@inproceedings{Aspe06,
+ author = "Asperti, Andrea and Coen, Claudio Sacerdoti and
+ Tassi, Enrico and Zacchiroli, Stefano",
+ title = {{Crafting a Proof Assistant}},
+ booktitle = "Proc. Types 2006: Conf. of the Types Project",
+ year = "2006",
+ abstract =
+ "Proof assistants are complex applications whose develop ment has
+ never been properly systematized or documented. This work is a
+ contribution in this direction, based on our experience with the
+ devel opment of Matita: a new interactive theorem prover based—as
+ Coq—on the Calculus of Inductive Constructions (CIC). In particular,
+ we analyze its architecture focusing on the dependencies of its
+ components, how they implement the main functionalities, and their
+ degree of reusability. The work is a first attempt to provide a ground
+ for a more direct com parison between different systems and to
+ highlight the common functionalities, not only in view of
+ reusability but also to encourage a more systematic comparison of
+ different softwares and architectural solutions.",
+ paper = "Aspe06.pdf"
+}
+
+\end{chunk}
+
+\index{Asperti, Andrea}
+\index{Tassi, Enrico}
+\begin{chunk}{axiom.bib}
+@inproceedings{Aspe07,
+ author = "Asperti, Andrea and Tassi, Enrico",
+ title = {{Higher Order Proof Reconstruction from
+ Paramodulationbased Refutations: The Unit Equality Case}},
+ booktitle = "MKM 2007",
+ year = "2007",
+ abstract =
+ "In this paper we address the problem of reconstructing a higher
+ order, checkable proof object starting from a proof trace left by a
+ first order automatic proof searching procedure, in a restricted
+ equational framework. The automatic procedure is based on
+ superposition rules for the unit equality case. Proof transformation
+ techniques aimed to improve the readability of the final proof are
+ discussed.",
+ paper = "Aspe07.pdf"
+}
+
+\end{chunk}
+
+\index{Asperti, Andrea}
+\index{Coen, Claudio Sacerdoti}
+\index{Tassi, Enrico}
+\index{Zacchiroli, Stefano}
+\begin{chunk}{axiom.bib}
+@article{Aspe07a,
+ author = "Asperti, Andrea and Coen, Claudio Sacerdoti and Tassi, Enrico
+ and Zacchiroli, Stefano",
+ title = {{User Interaction with the Matita Proof Assistant}},
+ journal = "J. of Automated Reasoning",
+ volume = "39",
+ number = "2",
+ pages = "109139",
+ abstract =
+ "Matita is a new, documentcentric, tacticbased interactive theorem
+ prover. This paper focuses on some of the distinctive features of the
+ user interaction with Matita, characterized mostly by the organization
+ of the library as a searchable knowledge base, the emphasis on a
+ highquality notational rendering, and the complex interplay between
+ syntax, presentation, and semantics.",
+ paper = "Aspe07a.pdf"
+}
+
+\end{chunk}
+
+\index{Asperti, Andrea}
\index{Ricciotti, Wilmer}
\index{Coer, Claudio Sacerdoti}
+\index{Coen, Claudio Sacerdoti}
\index{Tassi, Enrico}
\begin{chunk}{axiom.bib}
@article{Aspe09,
@@ 9479,7 +9585,92 @@ when shown in factored form.
\index{Asperti, Andrea}
\index{Ricciotti, Wilmer}
\index{Coer, Claudio Sacerdoti}
+\index{Coen, Claudio Sacerdoti}
+\index{Tassi, Enrico}
+\begin{chunk}{axiom.bib}
+@article{Aspe09a,
+ author = "Asperti, Andrea and Ricciotti, Wilmer and Coer, Claudio
+ Sacerdoti and Tassi, Enrico",
+ title = {{Hints in Unification}},
+ journal = "LNCS",
+ volume = "5674",
+ pages = "8498",
+ year = "2009",
+ isbn = "9783642033582",
+ abstract =
+ "Several mechanisms such as Canonical Structures, Type Classes, or
+ Pullbacks have been recently introduced with the aim to improve the
+ power and flexibility of the type inference algorithm for interactive
+ theorem provers. We claim that all these mechanisms are particular
+ instances of a simpler and more general technique, just consisting in
+ providing suitable hints to the unification procedure underlying type
+ inference. This allows a simple, modular and not intrusive
+ implementation of all the above mentioned techniques, opening at the
+ same time innovative and unexpected perspectives on its possible
+ applications.",
+ paper = "Aspe09a.pdf"
+}
+
+\end{chunk}
+
+\index{Asperti, Andrea}
+\index{Ricciotti, Wilmer}
+\index{Coen, Claudio Sacerdoti}
+\index{Tassi, Enrico}
+\begin{chunk}{axiom.bib}
+@inproceedings{Aspe09b,
+ author = "Asperti, Andrea and Ricciotti, Wilmer and Coer, Claudio
+ Sacerdoti and Tassi, Enrico",
+ title = {{A New Type for Tactics}},
+ booktitle = "SIGSAM PLMMS 2009",
+ publisher = "ACM",
+ year = "2009",
+ isbn = "9781605587356",
+ abstract =
+ "The type of tactics in all (procedural) proof assistants is (a
+ variant of) the one introduced in LCF. We discuss why this is
+ inconvenient and we propose a new type for tactics that 1) allows the
+ implementation of more clever tactics; 2) improves the implementation
+ of declarative languages on top of procedural ones; 3) allows for
+ better proof structuring; 4) improves proof automation; 5) allows
+ tactics to rearrange and delay the goals to be proved (e.g. in case of
+ side conditions or PVS subtyping judgements).",
+ paper = "Aspe09b.pdf"
+}
+
+\end{chunk}
+
+\index{Asperti, Andrea}
+\index{Tassi, Enrico}
+\begin{chunk}{axiom.bib}
+@article{Aspe10,
+ author = "Asperti, Andrea and Tassi, Enrico",
+ title = {{Smart Matching}},
+ journal = "LNCS",
+ volume = "6167",
+ pages = "263277",
+ year = "2010",
+ isbn = "9783642141287",
+ abstract =
+ "One of the most annoying aspects in the formalization of mathematics
+ is the need of transforming notions to match a given, existing
+ result. This kind of transformations, often based on a conspicuous
+ background knowledge in the given scientific domain (mostly expressed
+ in the form of equalities or isomorphisms), are usually implicit in
+ the mathematical discourse, and it would be highly desirable to obtain
+ a similar behavior in interactive provers. The paper describes the
+ superpositionbased implementation of this feature inside the Matita
+ interactive theorem prover, focusing in particular on the so called
+ smart application tactic, supporting smart matching between a goal and
+ a given result.",
+ paper = "Aspe10.pdf"
+}
+
+\end{chunk}
+
+\index{Asperti, Andrea}
+\index{Ricciotti, Wilmer}
+\index{Coen, Claudio Sacerdoti}
\index{Tassi, Enrico}
\begin{chunk}{axiom.bib}
@inproceedings{Aspe11,
@@ 9503,10 +9694,58 @@ when shown in factored form.
level. In this paper, we give an account of the whole system, its
peculiarities and its main applications.",
paper = "Aspe11.pdf",
+ keywords = "printed"
}
\end{chunk}
+\index{Asperti, Andrea}
+\index{Ricciotti, Wilmer}
+\index{Coen, Claudio Sacerdoti}
+\index{Tassi, Enrico}
+\begin{chunk}{axiom.bib}
+@article{Aspe12,
+ author = "Asperti, Andrea and Ricciotti, Wilmer and Coer, Claudio
+ Sacerdoti and Tassi, Enrico",
+ title = {{A Bidirectional Refinement Algorithm for the Calculus
+ of (Co)Inductive Constructions}},
+ journal = "Logical Methods in Computer Science",
+ volume = "8",
+ pages = "149",
+ abstract =
+ "The paper describes the refinement algorithm for the Calculus of
+ (Co)Inductive Constructions (CIC) implemented in the interactive
+ theorem prover Matita. The refinement algorithm is in charge of giving
+ a meaning to the terms, types and proof terms directly written by the
+ user or generated by using tactics, decision procedures or general
+ automation. The terms are written in an 'external syntax' meant to be
+ user friendly that allows omission of information, untyped binders and
+ a certain liberal use of user defined subtyping. The refiner modifies
+ the terms to obtain related well typed terms in the internal syntax
+ understood by the kernel of the ITP. In particular, it acts as a type
+ inference algorithm when all the binders are untyped. The proposed
+ algorithm is bidirectional: given a term in external syntax and a
+ type expected for the term, it propagates as much typing information
+ as possible towards the leaves of the term. Traditional
+ monodirectional algorithms, instead, proceed in a bottom up way by
+ inferring the type of a subterm and comparing (unifying) it with the
+ type expected by its context only at the end. We propose some novel
+ bidirectional rules for CIC that are particularly effective. Among
+ the benefits of bidirectionality we have better error message
+ reporting and better inference of dependent types. Moreover, thanks to
+ bidirectionality, the coercion system for subtyping is more
+ effective and type inference generates simpler unification problems
+ that are more likely to be solved by the inherently incomplete higher
+ order unification algorithms implemented. Finally we introduce in the
+ external syntax the notion of vector of placeholders that enables to
+ omit at once an arbitrary number of arguments. Vectors of placeholders
+ allow a trivial implementation of implicit arguments and greatly
+ simplify the implementation of primitive and simple tactics.",
+ paper = "Aspe12.pdf"
+}
+
+\end{chunk}
+
\index{Appel, Andrew W.}
\begin{chunk}{axiom.bib}
@book{Appe17,
@@ 9569,7 +9808,8 @@ when shown in factored form.
formal explanations can be executed at various stages of
completion. The most incomplete explanations resemble applicative
programs, the most complete are formal proofs.",
 paper = "Bate85.pdf"
+ paper = "Bate85.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 9594,7 +9834,34 @@ when shown in factored form.
booktitle = "Proc. 1996 New Security Paradigms Workshop",
publisher = "ACM",
year = "1996",
 paper = "Blak96.pdf"
+ paper = "Blak96.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Bowen, Jonathan P.}
+\index{Hinchey, Michael G.}
+\begin{chunk}{axiom.bib}
+@article{Bowe95,
+ author = "Bowen, Jonathan P. and Hinchey, Michael G.",
+ title = {{Seven More Myths of Formal Methods}},
+ journal = "IEEE Software",
+ volume = "12",
+ number = "4",
+ pages = "3441",
+ year = "1995",
+ abstract =
+ "New myths about formal methods are gaining tacit acceptance both
+ outside and inside the systemdevelopment community. The authors
+ address and dispel these myths based on their observations of
+ industrial projects. The myths include: formal methods delay the
+ development process; they lack tools; they replace traditional
+ engineering design methods; they only apply to software; are
+ unnecessary; not supported; and formal methods people always use
+ formal methods.",
+ paper = "Bowe95.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 9614,7 +9881,8 @@ when shown in factored form.
tasks arise in representing the constructs in language. Past progress
has so reduced the accidental tasks that future progress now depends
upon addressing the essence.",
 paper = "Broo87.pdf"
+ paper = "Broo87.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 9641,7 +9909,8 @@ when shown in factored form.
differently. Programming gives mathematics a new form of
understanding. The computer is the driving force behind these
changes.",
 paper = "Calu07.pdf"
+ paper = "Calu07.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 9794,6 +10063,92 @@ when shown in factored form.
\end{chunk}
\index{Coen, Claudio Sacerdoti}
+\index{Zacchiroli, Stefano}
+\begin{chunk}{axiom.bib}
+@article{Coen04,
+ author = "Coen, Claudio Sacerdoti and Zacchiroli, Stefano",
+ title = {{Efficient Ambiguous Parsing of Mathematical Formulae}},
+ journal = "LNCS",
+ volume = "3119",
+ pages = "347362",
+ year = "2004",
+ isbn = "3540230297",
+ abstract =
+ "Mathematical notation has the characteristic of being ambiguous:
+ operators can be overloaded and information that can be deduced is
+ often omitted. Mathematicians are used to this ambiguity and can
+ easily disambiguate a formula making use of the context and of their
+ ability to find the right interpretation.
+
+ Software applications that have to deal with formulae usually avoid
+ these issues by fixing an unambiguous input notation. This solution is
+ annoying for mathematicians because of the resulting tricky syntaxes
+ and becomes a show stopper to the simultaneous adoption of tools
+ characterized by different input languages.
+
+ In this paper we present an efficient algorithm suitable for ambiguous
+ parsing of mathematical formulae. The only requirement of the
+ algorithm is the existence of a 'validity' predicate over abstract
+ syntax trees of incomplete formulae with placeholders. This
+ requirement can be easily fulfilled in the applicative area of
+ interactive proof assistants, and in several other areas of
+ Mathematical Knowledge Management.",
+ paper = "Coen04.pdf"
+}
+
+\end{chunk}
+
+\index{Coen, Claudio Sacerdoti}
+\index{Tassi, Enrico}
+\index{Zacchiroli, Stefano}
+\begin{chunk}{axiom.bib}
+@inproceedings{Coen06,
+ author = "Coen, Claudio Sacerdoti and Tassi, Enrico and
+ Zacchiroli, Stefano",
+ title = {{Tinycals: Step by Step Teacticals}},
+ booktitle = "Proc. User Interfaces for Theorem Provers",
+ year = "2006",
+ pages = "125142",
+ abstract =
+ "Most of the stateoftheart proof assistants are based on procedural
+ proof languages, scripts, and rely on LCF tacticals as the primary
+ tool for tactics composition. In this paper we discuss how these
+ ingredients do not interact well with user interfaces based on the
+ same interaction paradigm of Proof General (the de facto standard in
+ this field), identifying in the coarsegrainedness of tactical
+ evaluation the key problem. We propose tinycals as an alternative to a
+ subset of LCF tacticals, showing that the user does not experience the
+ same problem if tacticals are evaluated in a more finegrained
+ manner. We present the formal operational semantics of tinycals as
+ well as their implementation in the Matita proof assistant.",
+ paper = "Coen06.pdf"
+}
+
+\end{chunk}
+
+\index{Coen, Claudio Sacerdoti}
+\index{Zacchiroli, Stefano}
+\begin{chunk}{axiom.bib}
+@inproceedings{Coen07a,
+ author = "Coen, Claudio Sacerdoti and Zacchiroli, Stefano",
+ title = {{Spurious Disambiguation Error Detection}},
+ booktitle = "MKM 2007 Mathematical Knowledge Management",
+ year = "2007",
+ abstract =
+ "The disambiguation approach to the input of formulae enables the user
+ to type correct formulae in a terse syntax close to the usual
+ ambiguous mathematical notation. When it comes to incorrect formulae
+ we want to present only errors related to the interpretation meant by
+ the user, hiding errors related to other interpretations (spurious
+ errors). We propose a heuristic to recognize spurious errors, which
+ has been integrated with our former efficient disambiguation
+ algorithm.",
+ paper = "Coen07a.pdf"
+}
+
+\end{chunk}
+
+\index{Coen, Claudio Sacerdoti}
\begin{chunk}{axiom.bib}
@article{Coen10,
author = "Coen, Claudio Sacerdoti",
@@ 9816,6 +10171,31 @@ when shown in factored form.
\end{chunk}
+\index{Coen, Claudio Sacerdoti}
+\index{Tassi, Enrico}
+\begin{chunk}{axiom.bib}
+@inproceedings{Coen11,
+ author = "Coer, Claudio Sacerdoti and Tassi, Enrico",
+ title = {{Nonuniform Coercions via Unification Hints}},
+ booktitle = "Proc. Types for Proofs and Programs",
+ volume = "53",
+ pages = "1926",
+ year = "2011",
+ abstract =
+ "We introduce the notion of nonuniform coercion, which is the
+ promotion of a value of one type to an enriched value of a different
+ type via a nonuniform procedure. Nonuniform coercions are a
+ generalization of the (uniform) coercions known in the literature and
+ they arise naturally when formalizing mathematics in an higher order
+ interactive theorem prover using convenient devices like canonical
+ structures, type classes or unification hints. We also show how
+ nonuniform coercions can be naturally implemented at the user level in
+ an interactive theorem prover that allows unification hints.",
+ paper = "Coen11.pdf"
+}
+
+\end{chunk}
+
\index{Constable, R.L.}
\index{Knoblock, T.B.}
\index{Gates, J.L.}
@@ 9876,7 +10256,8 @@ when shown in factored form.
year = "2017",
abstract = "Wherein existing methods for building secure systems are
examined and found wanting",
 paper = "Cyph17.pdf"
+ paper = "Cyph17.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 9933,7 +10314,8 @@ when shown in factored form.
inadequate use of measurement. Numerous empirical studies are flawed
because of their poor experimental design and lack of adherence to
proper measurement principles.",
 paper = "Fent93.pdf"
+ paper = "Fent93.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 9955,7 +10337,8 @@ when shown in factored form.
those structures, are not. The success of program verification as a
generally applicable and completely reliable method for guaranteeing
program performance is not even a theoretical possibility.",
 paper = "Fetz88.pdf"
+ paper = "Fetz88.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 9985,7 +10368,8 @@ when shown in factored form.
"With the advantage of more than 25 years' hindsight, this twentyfirst
century author looks askance at the 'crisis' in software practice and
expresses deep concern for a crisis in software research.",
 paper = "Glas94.pdf"
+ paper = "Glas94.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 10000,7 +10384,24 @@ when shown in factored form.
number = "8",
year = "2002",
pages = "1921",
 paper = "Glas02.pdf"
+ paper = "Glas02.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Grabm\"uller, Martin}
+\begin{chunk}{axiom.bib}
+@misc{Grab06a,
+ author = "Grabmuller, Martin",
+ title = {{Algorithm W Step by Step}},
+ year = "2006",
+ link = "\url{http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7733&rep=rep1&type=pdf}",
+ abstract =
+ "In this paper we develop a complete implementation of the classic
+ algoirhtm W for HinleyMilner polymorphic type inference in Haskell",
+ paper = "Grab06a.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 10019,7 +10420,23 @@ when shown in factored form.
"Formal methods are difficult, expensive, and not widely useful,
detractors say. Using a case study and other realworld examples, this
article challenges such common myths.",
 paper = "Hall80.pdf"
+ paper = "Hall80.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Hoare, Charles Antony Richard}
+\begin{chunk}{axiom.bib}
+@article{Hoar87,
+ author = "Hoare, Charles Antony Richard",
+ title = {{An Overview of Some Formal Methods for Program Design}},
+ journal = "Computer",
+ year = "1987",
+ volume = "20",
+ number = "9",
+ paper = "Hoar87.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 10045,7 +10462,8 @@ when shown in factored form.
provide a conceptual framework and basic understanding to promote the
best of current practice, and point directions for future
improvement.",
 paper = "Hoar96.pdf"
+ paper = "Hoar96.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 10084,7 +10502,8 @@ when shown in factored form.
number = "1",
year = "1988",
pages = "327",
 paper = "Lind88.pdf"
+ paper = "Lind88.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 10239,7 +10658,8 @@ when shown in factored form.
that my theory no longer contains intuitionistic simple type theory as
it originally did. Instead, its proof theoretic strength should be
close to that of predicative analysis.",
 paper = "Mart73.pdf"
+ paper = "Mart73.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 10272,7 +10692,93 @@ when shown in factored form.
synthesis. Thus the correctness of a program written in the theory of
types is proved formally at the same time as it is being
synthesized.",
 paper = "Mart79.pdf"
+ paper = "Mart79.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{McBride, Conor}
+\begin{chunk}{axiom.bib}
+@phdthesis{Mcbr99,
+ author = "McBride, Conor",
+ title = {{Dependently Typed Functional Programs and their Proofs}},
+ school = "University of Edinburgh",
+ year = "1999",
+ link = "\url{http://strictlypositive.org/thesis.pdf}",
+ abstract =
+ "Research in dependent type theories has, in the past, concentrated on
+ its use in the presentation of theorems and theoremproving. This
+ thesis is concerned mainly with the exploitation of the computational
+ aspects of type theory for programming, in a context where the
+ properties of programs may readily be specified and established. In
+ particular, it develops technology for programming with dependent
+ inductive families of datatypes and proving those programs correct. It
+ demonstrates the considerable advantage to be gained by indexing data
+ structures with pertinent characteristic information whose soundness
+ is ensured by typechecking, rather than human effort.
+
+ Type theory traditionally presents safe and terminating computation on
+ inductive datatypes by means of elimination rules which serve as
+ induction principles and, via their associated reduction behaviour,
+ recursion operators. In the programming language arena, these appear
+ somewhat cumbersome and give rise to unappealing code, complicated by
+ the inevitable interaction between case analysis on dependent types
+ and equational reasoning on their indices which must appear explicitly
+ in the terms. Thierry Coquand's proposal to equip type theory directly
+ with the kind of pattern matching notation to which functional
+ programmers have become used to over the past three decades offers a
+ remedy to many of these difficulties. However, the status of pattern
+ matching relative to the traditional elimination rules has until now
+ been in doubt. Pattern matching implies the uniqueness of identity
+ proofs, which Martin Hofmann showed underivable from the conventiaonal
+ definition of equality. This thesis shows that the adoption of this
+ uniqueness as axiomatic is sufficient to make pattern matching
+ admissible.
+
+ A datatype's elimination rule allows abstraction only over the whole
+ inductively defined family. In order to support pattern matching, the
+ application of such rules to specific instances of dependent families
+ has been systematised. The underlying analysis extends beyond
+ datatypes to other rules of a similar second order character,
+ suggesting they may have other roles to play in the specification,
+ verification and, perhaps, derivation of programs. The technique
+ developed shifts the specificity from the instantiation of the type's
+ indices into equational constraints on indices freely chosen, allowing
+ the elimination rule to be applied.
+
+ Elimination by this means leaves equational hypotheses in the
+ resulting subgoals, which must be solved if further progress is to be
+ made. The firstorder unification algorithm for constructor forms in
+ simmple types presented in [McB96] has been extended to cover
+ dependent datatypes as well, yielding completely automated solution of
+ a class of problems which can be syntactically defined.
+
+ The justification and operation of these techniques requires the
+ machine to construct and exploit a standardised collection of
+ auxiliary lemmas for each datatype. This is greatly facilitated by two
+ technical developments of interest in their own right:
+ \begin{itemize}
+ \item a more convenient definition of equality, with a relaxed
+ formulation rule allowing elements of different types to be compared,
+ but nonetheless equivalent to the usual equality plus the axiom of
+ uniqueness
+ \item a type theory, OLEG, which incorporates incomplete objects,
+ accounting for their 'holes' entirely within the typing judgments and,
+ novelly, not requiring any notion of explicit substitution to manage
+ their scopes.
+ \end{itemize}
+
+ A substantial prototype has been implemented, extending the proof
+ assistant LEGO. A number of programs are developed by way of
+ example. Chiefly, the increased expressivity of dependent datatypes is
+ shown to capture a standard firstorder unification algorithm within
+ the class of structurally recursive programs, removing any need for a
+ termination argument. Furthermore, the use of elimination rules in
+ specifying the components of the program simplifies significantly its
+ correctness proof.",
+ paper = "Mcbr99.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 10289,7 +10795,34 @@ when shown in factored form.
LCFstyle implementation of higherorder logic using Haskell as a
metalanguage. We discuss details of the logic implemented, kernel
design, and novel proof state and tactic representations.",
 paper = "Mull13.pdf"
+ paper = "Mull13.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Padovani, Luca}
+\index{Zacchiroli, Stefano}
+\begin{chunk}{axiom.bib}
+@inproceedings{Pado06,
+ author = "Padovani, Luca and Zacchiroli, Stefano",
+ title = {{From Notation to Semantics: There and Back Again}},
+ booktitle = "5th Conf. on Mathematical Knowledge Management",
+ year = "2006",
+ abstract =
+ "Mathematical notation is a structured, open, and ambiguous
+ language. In order to support mathematical notation in MKM
+ applications one must necessarily take into account presentational as
+ well as semantic aspects. The former are required to create a
+ familiar, comfortable, and usable interface to interact with. The
+ latter are necessary in order to process the information
+ meaningfully. In this paper we investigate a framework for dealing
+ with mathematical notation in a meaningful, extensible way, and we
+ show an effective instantiation of its architecture to the field of
+ interactive theorem proving. The framework builds upon wellknown
+ concepts and widelyused technologies and it can be easily adopted by
+ other MKM applications.",
+ paper = "Pado06.pdf"
}
\end{chunk}
@@ 10500,7 +11033,8 @@ when shown in factored form.
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"
+ paper = "Soze06.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 10742,7 +11276,7 @@ when shown in factored form.
by including parametric limits of integration and queries with side
conditions.",
paper = "Adam99.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 10774,7 +11308,7 @@ when shown in factored form.
library. These examples provide proofs which are both illustrative and
applicable to genuine symbolic computation problems.",
paper = "Adam01.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 11101,7 +11635,7 @@ when shown in factored form.
is based on theorem templates, which provide formal specifications for
the algorithms.",
paper = "Ball98.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
\end{chunk}
@@ 11139,7 +11673,7 @@ when shown in factored form.
system on the tacticlevel of Isabelle and its integration into proof
procedures.",
paper = "Ball99.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 11185,7 +11719,7 @@ when shown in factored form.
Some examples of communication forms are given that show how the
participants benefit",
paper = "Bare01.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
\end{chunk}
@@ 11474,7 +12008,7 @@ when shown in factored form.
software development process from the specification of requirements to
the finished system. These methos are potentially applicable to the
development of correct hardware systems as well",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
@@ 11708,7 +12242,8 @@ when shown in factored form.
for describing a hierarchy of Drecords in an incremental way. In
mixDrecs, fields can be only declared or they can be
redefined. MixDrecs can be extended by inheritance.",
 paper = "Boul00a.pdf"
+ paper = "Boul00a.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 11746,7 +12281,7 @@ when shown in factored form.
exactly the mathematical dependencies between different structures.
This may ease the achievement of proofs.",
paper = "Boul99.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 11996,7 +12531,7 @@ when shown in factored form.
year = "1994",
volume = "125",
paper = "Brui68.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
\end{chunk}
@@ 12011,7 +12546,8 @@ when shown in factored form.
publisher = "SpringerVerlag",
pages = "220",
isbn = "9783211828441",
 paper = "Buch97.pdf"
+ paper = "Buch97.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 12026,7 +12562,8 @@ when shown in factored form.
number = "2",
pages = "247252",
year = "2001",
 paper = "Buch01.pdf"
+ paper = "Buch01.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 12131,7 +12668,8 @@ when shown in factored form.
can be used for dening and proving properties of mathematical models
and algorithms, while a specially provided ``computing engine'' can
execute directly the logical description of these algorithms.",
 paper = "Buch03.pdf"
+ paper = "Buch03.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 12367,7 +12905,8 @@ when shown in factored form.
systems may be based on different logics, formalisms, data structures,
interfaces. A result of this work is illustrated by a prototype
implementation of an interface between Isabelle and Maple.",
 paper = "Calm95.pdf"
+ paper = "Calm95.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 12417,7 +12956,8 @@ when shown in factored form.
wellknown examples. The needs and requirements for the Mathematics
Software Bus and its architecture are demonstrated through some
implementations of powerful interfaces between mathematical services.",
 paper = "Calm97a.pdf"
+ paper = "Calm97a.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 12613,7 +13153,7 @@ when shown in factored form.
year = "1991",
link = "\url{http://www.cs.cmu.edu/~emc/papers/Conference%20Papers/Analytica%20A%20Theorem%20Prover%20in%20Mathematica.pdf}",
paper = "Clar91.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
\end{chunk}
@@ 12798,7 +13338,8 @@ when shown in factored form.
as the program expressions of a pure functional lazy language:
variable, constructor, application, abstraction, case expressions,
and local let expressions.",
 paper = "Coqu93.pdf"
+ paper = "Coqu93.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 12911,7 +13452,7 @@ when shown in factored form.
our claim that the Nuprl proof development system is especially well
suited to support this kind of mathematics.",
paper = "Cons98.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 13099,7 +13640,8 @@ when shown in factored form.
make the formal verification process difficult to justify and manage.
It is felt that ease of formal verification should not dominate program
language design.",
 paper = "Demi79.pdf"
+ paper = "Demi79.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 13315,7 +13857,7 @@ when shown in factored form.
a modest cost. Our approach is based on retargeting the code generator
of the OpenAxiom compiler to the Poly/ML abstract machine.",
paper = "Dosr11.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 13491,7 +14033,8 @@ when shown in factored form.
foundation for mechanized mathematics. It is the basis for the logic
of IMPS, an Interactive Mathematical Proof System developed at The
MITRE Corporation.",
 paper = "Farm93b.pdf"
+ paper = "Farm93b.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 13630,7 +14173,7 @@ when shown in factored form.
related approach to a version of a Bessel function algorithm for J0(x)
based on a recurrence.",
paper = "Fate03a.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
\end{chunk}
@@ 14044,7 +14587,7 @@ when shown in factored form.
of verification conditions, harnesses to ensure more reliable
differential equation solvers, and verifiable lookup tables.",
paper = "Gott05.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 14257,7 +14800,7 @@ when shown in factored form.
reals which combines the rigour of a theorem prover with the power of
a computer algebra system.",
paper = "Harr94.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 14597,7 +15140,7 @@ when shown in factored form.
algebra system and the relevance of this work for abstract functional
programming.",
paper = "Jack94.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 14726,7 +15269,7 @@ when shown in factored form.
prototype, but can be straightforwardly scaled up to a practical
computer algebra system.",
paper = "Kali07.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 14832,7 +15375,7 @@ when shown in factored form.
wellsuited for producing a highlevel verbalised explication as well
as for a lowlevel (machine checkable) calculuslevel proof.",
paper = "Kerb96.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 14856,7 +15399,8 @@ when shown in factored form.
providing a highlevel language, we argue that more should be learned
from the mathematical practice in order to improve the applicability
of formal systems.",
 paper = "Kerb07.pdf"
+ paper = "Kerb07.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 14886,7 +15430,7 @@ when shown in factored form.
OpenMath terms produced by a CAS in the calculus of Coq, as well as
viewing pure Coq terms in a simpler type system that is behind OpenMath.",
paper = "Kome11.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
\end{chunk}
@@ 15244,7 +15788,7 @@ when shown in factored form.
times), and a comprehensive facility for defining conditionally
applicable transformations.",
paper = "Lond74.pdf",
 keywords = "axiomref"
+ keywords = "axiomref, printed"
}
\end{chunk}
@@ 15452,7 +15996,7 @@ when shown in factored form.
disadvantages of these approaches. We also discuss some possible case
studies.",
paper = "Mart97.ps",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 15677,7 +16221,7 @@ when shown in factored form.
functional language Haskell and implementing certain piece of
commutative algebra",
paper = "Mesh01.pdf",
 keywords = "axiomref"
+ keywords = "axiomref, printed"
}
@@ 15833,8 +16377,8 @@ when shown in factored form.
tyhpes ({\tt Agda}). There are given several examples illustrating
particular points of implementing the approach of constructive
mathematics.",
 paper = "Mesh16a.pdf"

+ paper = "Mesh16a.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 15908,7 +16452,8 @@ when shown in factored form.
these results to richer languages; a typechecking algorithm based on
$W$ is in fact already implemented and working, for the metalanguage ML
in the Edinburgh LCF system,",
 paper = "Miln78.pdf"
+ paper = "Miln78.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 16083,7 +16628,7 @@ when shown in factored form.
year = "2013",
link = "\url{http://ceurws.org/Vol1010/paper09.pdf}",
paper = "Neup13.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
\end{chunk}
@@ 16206,7 +16751,8 @@ when shown in factored form.
title = {{Programming in MartinL\"of's Type Theory}},
year = "1990",
publisher = "Oxford University Press",
 paper = "Nord90.pdf"
+ paper = "Nord90.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 16327,7 +16873,8 @@ 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.pdf"
+ paper = "Pare93.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 16545,7 +17092,8 @@ when shown in factored form.
algorithm for partial type inference in the $omega$order polymorphic
$\lambda$calculus. We present an implementation in $\lambda$Prolog in
full.",
 paper = "Pfen88.pdf"
+ paper = "Pfen88.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 16739,7 +17287,7 @@ when shown in factored form.
The paper shows an interesting way to decorate Axiom with pre and
postconditions.",
paper = "Poll98.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 17631,7 +18179,8 @@ when shown in factored form.
at RISC. In this talk, we want to present the current status of the
new implementation, in particular the new user interface of the
system.",
 paper = "Wind14.pdf"
+ paper = "Wind14.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 27322,7 +27871,7 @@ Proc ISSAC 97 pp172175 (1997)
introduce notations prepresentable and pnegligible where p denotes
precision, and show how this helps in our applications.",
paper = "Fate03.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
\end{chunk}
@@ 33474,7 +34023,7 @@ VM/370 SPAD.SCRIPTS August 24, 1979 SPAD.SCRIPT
mathematical equality and with data structure equality, and to
explain how necessary it is to keep a clear distintion between the two.",
paper = "Dave02.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 35387,7 +35936,7 @@ Grant citation GR/L48256 Nov 1, 1997Feb 28, 2001
are inspired by the IMPS Interactive Mathematical Proof System and the
Axiom computer algebra system.",
paper = "Farm03.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 37660,7 +38209,7 @@ April 1976 (private copy)
of computer algebra results proved formally in the HOL theorem prover
with the aid of Maple.",
paper = "Harr98.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 39951,7 +40500,7 @@ SIGSAM Communications in Computer Algebra, 157 2006
and (iii) interface specifications which assist the verification of
pre and post conditions of implemented code.",
paper = "Kels00a.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 40120,7 +40669,7 @@ SIGSAM Communications in Computer Algebra, 157 2006
calculuslevel proof. We present an implementation of our ideas and
exemplify them using an automatically solved example.",
paper = "Kerb98.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 46085,7 +46634,8 @@ IBM Manual, March 1988
proving theorems. ITP grew out of a more general project  called
Symbolic Incidence Geometry  which is concerned with the problem of
the systematic use of the computer in incidence geometry.",
 paper = "Uebe94.pdf"
+ paper = "Uebe94.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 48329,7 +48879,8 @@ National Physical Laboratory. (1982)
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"
+ paper = "Bail96.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 48441,7 +48992,8 @@ Academic Press. 1974
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"
+ paper = "Barr96.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 48484,7 +49036,8 @@ Comm. ACM. 17, 6 319320. (1974)
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"
+ paper = "Bart95.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 48562,7 +49115,7 @@ Comm. ACM. 17, 6 319320. (1974)
theorems. In this paper, we show how it can prove a series of lemmas
that lead to the Bernstein approximation theorem.",
paper = "Baue98.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
\end{chunk}
@@ 48694,7 +49247,7 @@ J. Symbolic Computation (1993) 15, 393413
algebra system. We show how the integrated system solves a problem
which could not be tackled by each single system alone.",
paper = "Bert98.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
\end{chunk}
@@ 48837,7 +49390,8 @@ Ginn \& Co., Boston and New York. (1962)
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"
+ paper = "Bove02.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 49137,7 +49691,8 @@ ISBN 3764359013 (1998)
of ``propositions as types'' (Section 14). Finally the survey will be
used to ventilate opinions and views in mathematics which are not
easily set down in more technical reports.",
 paper = "Brui94.pdf"
+ paper = "Brui94.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 49257,7 +49812,7 @@ ISBN 3764359013 (1998)
practical importance of functors and show how they can be naturally
embedded into Mathematica.",
paper = "Buch96.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
\end{chunk}
@@ 49429,7 +49984,7 @@ ISBN 3764359013 (1998)
encoding, encryption, and knowledge sharing. The latter concerns the
semantic aspects of architectures for cooperative problem solving.",
paper = "Calm96.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
\end{chunk}
@@ 49519,7 +50074,8 @@ Math. Comput. 51 267280. (1988)
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"
+ paper = "Carl02.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 49692,7 +50248,7 @@ Lecture Notes in Computer Science. 76 (1979) SpringerVerlag
challenge problems completely automatically. The axioms and inference
rules for constructing the proofs are also briefly discussed.",
paper = "Clar94.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
\end{chunk}
@@ 49762,7 +50318,8 @@ Rocky Mountain J. Math. 14 119139. (1984)
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"
+ paper = "Coen07.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 50299,7 +50856,7 @@ SIAM J. Numer. Anal. 19 12861304. (1982)
its functionality as it appears to the user, and explain the design
issues and implementation techniques. REDLOG is available on the WWW.",
paper = "Dolz97b.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
\end{chunk}
@@ 50443,7 +51000,8 @@ pp 1828
"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"
+ paper = "Dowe96.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 50501,7 +51059,8 @@ A.E.R.E. Report R.8730. HMSO. (1977)
type system and discusses their merits and effectiveness. We conclude
by a brief comparison with similar developments using other theorem
provers.",
 paper = "Dute96.pdf"
+ paper = "Dute96.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 50837,7 +51396,8 @@ A.E.R.E. Report R.8730. HMSO. (1977)
constructions in a straightforward way. This work has been
implemented in the Coq Proof Assistant and applied on nontrivial
examples.",
 paper = "Fill98.pdf"
+ paper = "Fill98.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 51949,7 +52509,7 @@ Lecture Notes in Economics and Mathematical Systems. 187 SpringerVerlag. 1981
consisting of type and algorithm schemata, algebraic algorithms and
theorems.",
paper = "Homa94.pdf",
 keywords = "axiomref, CASProof"
+ keywords = "axiomref, CASProof, printed"
}
\end{chunk}
@@ 51974,7 +52534,7 @@ Lecture Notes in Economics and Mathematical Systems. 187 SpringerVerlag. 1981
framework for the specification of symbolic mathematical problem
solving by cooperation of algorithms and theorems.",
paper = "Homa96.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
\end{chunk}
@@ 52286,7 +52846,8 @@ Comput. J. 9 281285. (1966)
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"
+ paper = "Jone96.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 52664,7 +53225,8 @@ Springer Verlag Heidelberg, 1989, ISBN 0387969802
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"
+ paper = "Kies03.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 53217,7 +53779,7 @@ AddisonWesley (March 1979) ISBN 0201144611
pages = "239239",
year = "2002",
paper = "Lint02.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
\end{chunk}
@@ 53412,7 +53974,8 @@ AddisonWesley (March 1979) ISBN 0201144611
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"
+ paper = "Luox99.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 53486,7 +54049,8 @@ AMS Chelsea Publishing ISBN 0821816462
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"
+ paper = "Maga00.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 54058,7 +54622,8 @@ Journal of the ACM, Vol. 25, No. 2, April 1978, pp. 271282
volume = "1512",
year = "1999",
pages = "317332",
 paper = "Nara99.pdf"
+ paper = "Nara99.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 54223,7 +54788,8 @@ ACM Trans. Math. Softw. 5 118125. (1979)
"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"
+ paper = "Nipk02.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 55720,7 +56286,7 @@ The University of Chicago Press. 1974
computation. We demonstrate our approach with the concrete
implementation in the $\Omega$MEGA system.",
paper = "Sorg00.pdf",
 keywords = "CASProof"
+ keywords = "CASProof, printed"
}
\end{chunk}
@@ 55825,7 +56391,8 @@ PrenticeHall 1971
symbolic computation program REDUCE. The use of REDUCE in a
theoremproving context is described in detail. Sample proofs are
given with data on computation time per step on an IBM4381.",
 paper = "Supp89.pdf"
+ paper = "Supp89.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 55987,7 +56554,8 @@ J. Comput. Phys. 52 340350. (1983)
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"
+ paper = "Tray10.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ 56335,7 +56903,8 @@ SIAM J. Sci. Statist. Comput. 3 387407. (1982)
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"
+ paper = "Wied03.pdf",
+ keywords = "printed"
}
\end{chunk}
diff git a/changelog b/changelog
index 63bee41..7cd5b99 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20180113 tpd src/axiomwebsite/patches.html 20180113.01.tpd.patch
+20180113 tpd books/bookvolbib add references
20180109 tpd src/axiomwebsite/patches.html 20180109.01.tpd.patch
20180109 tpd books/bookvolbib add references
20180106 tpd src/axiomwebsite/patches.html 20180106.01.tpd.patch
diff git a/patch b/patch
index da2642a..262506b 100644
 a/patch
+++ b/patch
@@ 2,35 +2,85 @@ books/bookvolbib add references
Goal: Proving Axiom Correct
\index{Scott, Dana}
+\index{Coer, Claudio Sacerdoti}
+\index{Tassi, Enrico}
\begin{chunk}{axiom.bib}
@article{Scot76,
 author = "Scott, Dana",
 title = {{Data Types as Lattices}},
 journal = "SIAM J. Comput.",
 volume = "5",
 year = "1976",
 pages = "522587",
+@inproceedings{Aspe11a,
+ author = "Coer, Claudio Sacerdoti and Tassi, Enrico",
+ title = {{Nonuniform Coercions via Unification Hints}},
+ booktitle = "Proc. Types for Proofs and Programs",
+ volume = "53",
+ pages = "1926",
+ year = "2011",
abstract =
 "The meaning of many kinds of expressions in programming languages can
 be taken as elements of certain spaces of 'partial' objects. In this
 report these spaces are modeled in one univeral domain $P_\omega$, the
 set of all subsets of the integers. This domain renders the connection
 of this semantic theory with the ordinary theor of number theoretic
 (especailly general recursive) functions clear and straightforward.",
 paper = "Scot76.pdf"
+ "We introduce the notion of nonuniform coercion, which is the
+ promotion of a value of one type to an enriched value of a different
+ type via a nonuniform procedure. Nonuniform coercions are a
+ generalization of the (uniform) coercions known in the literature and
+ they arise naturally when formalizing mathematics in an higher order
+ interactive theorem prover using convenient devices like canonical
+ structures, type classes or unification hints. We also show how
+ nonuniform coercions can be naturally implemented at the user level in
+ an interactive theorem prover that allows unification hints.",
+ paper = "Aspe11a.pdf"
}
\end{chunk}
\index{Bishop, Errett}
+\index{Asperti, Andrea}
+\index{Ricciotti, Wilmer}
+\index{Coer, Claudio Sacerdoti}
+\index{Tassi, Enrico}
\begin{chunk}{axiom.bib}
@book{Bish12,
 author = "Bishop, Errett",
 title = {{Foundations of Constructive Analysis}},
 publisher = "ISHI Press",
 year = "2012",
 isbn = "9784871877145"
+@article{Aspe09a,
+ author = "Asperti, Andrea and Ricciotti, Wilmer and Coer, Claudio
+ Sacerdoti and Tassi, Enrico",
+ title = {{Hints in Unification}},
+ journal = "LNCS",
+ volume = "5674",
+ pages = "8498",
+ year = "2009",
+ isbn = "9783642033582",
+ abstract =
+ "Several mechanisms such as Canonical Structures, Type Classes, or
+ Pullbacks have been recently introduced with the aim to improve the
+ power and flexibility of the type inference algorithm for interactive
+ theorem provers. We claim that all these mechanisms are particular
+ instances of a simpler and more general technique, just consisting in
+ providing suitable hints to the unification procedure underlying type
+ inference. This allows a simple, modular and not intrusive
+ implementation of all the above mentioned techniques, opening at the
+ same time innovative and unexpected perspectives on its possible
+ applications.",
+ paper = "Aspe09a.pdf"
+}
+
+\end{chunk}
+
+\index{Asperti, Andrea}
+\index{Tassi, Enrico}
+\begin{chunk}{axiom.bib}
+@article{Aspe10,
+ author = "Asperti, Andrea and Tassi, Enrico",
+ title = {{Smart Matching}},
+ journal = "LNCS",
+ volume = "6167",
+ pages = "263277",
+ year = "2010",
+ isbn = "9783642141287",
+ abstract =
+ "One of the most annoying aspects in the formalization of mathematics
+ is the need of transforming notions to match a given, existing
+ result. This kind of transformations, often based on a conspicuous
+ background knowledge in the given scientific domain (mostly expressed
+ in the form of equalities or isomorphisms), are usually implicit in
+ the mathematical discourse, and it would be highly desirable to obtain
+ a similar behavior in interactive provers. The paper describes the
+ superpositionbased implementation of this feature inside the Matita
+ interactive theorem prover, focusing in particular on the so called
+ smart application tactic, supporting smart matching between a goal and
+ a given result.",
+ paper = "Aspe10.pdf"
}
\end{chunk}
@@ 40,214 +90,359 @@ Goal: Proving Axiom Correct
\index{Coer, Claudio Sacerdoti}
\index{Tassi, Enrico}
\begin{chunk}{axiom.bib}
@article{Aspe09,
+@inproceedings{Aspe09b,
author = "Asperti, Andrea and Ricciotti, Wilmer and Coer, Claudio
Sacerdoti and Tassi, Enrico",
 title = {{A Compact Kernel for the Calculus of Inductive Constructions}},
 journal = "Sadhana",
 volume = "34",
 number = "1",
+ title = {{A New Type for Tactics}},
+ booktitle = "SIGSAM PLMMS 2009",
+ publisher = "ACM",
year = "2009",
 pages = "71104",
+ isbn = "9781605587356",
abstract =
 "The paper describes the new kernel for the Calculus of Inductive
 Constructions (CIC) implemented inside the Matita Interactive
 Theorem Prover. The design of the new kernel has been completely
 revisited since the first release, resulting in a remarkably compact
 implementation of about 2300 lines of OCaml code. The work is meant
 for people interested in implementation aspects of Interactive
 Provers, and is not self contained . In particular, it requires good
 acquaintance with Type Theory and functional programming
 languages.",
 paper = "Aspe09.pdf"
+ "The type of tactics in all (procedural) proof assistants is (a
+ variant of) the one introduced in LCF. We discuss why this is
+ inconvenient and we propose a new type for tactics that 1) allows the
+ implementation of more clever tactics; 2) improves the implementation
+ of declarative languages on top of procedural ones; 3) allows for
+ better proof structuring; 4) improves proof automation; 5) allows
+ tactics to rearrange and delay the goals to be proved (e.g. in case of
+ side conditions or PVS subtyping judgements).",
+ paper = "Aspe09b.pdf"
}
\end{chunk}
\index{Asperti, Andrea}
\index{Ricciotti, Wilmer}
\index{Coer, Claudio Sacerdoti}
\index{Tassi, Enrico}
\begin{chunk}{axiom.bib}
@inproceedings{Aspe11,
 author = "Asperti, Andrea and Ricciotti, Wilmer and Coer, Claudio
 Sacerdoti and Tassi, Enrico",
 title = {{The Matita Interactive Theorem Prover}},
 booktitle = "CADE23 Automated Deduction",
 year = "2011",
 pages = "6469",
+@inproceedings{Aspe07,
+ author = "Asperti, Andrea and Tassi, Enrico",
+ title = {{Higher Order Proof Reconstruction from
+ Paramodulationbased Refutations: The Unit Equality Case}},
+ booktitle = "MKM 2007",
+ year = "2007",
abstract =
 "Matita is an interactive theorem prover being developed by the Helm
 team at the University of Bologna. Its stable version 0.5.x may be
 downloaded at http://matita.cs.unibo.it . The tool originated in the
 European project MoWGLI as a set of XMLbased tools aimed to provide a
 mathematicianfriendly webinterface to repositories of formal
 mathematical knoweldge, supporting advanced contentbased
 functionalities for querying, searching and browsing the library. It
 has since then evolved into a fully fledged ITP, specifically designed
 as a lightweight, but competitive system, particularly suited for the
 assessment of innovative ideas, both at foundational and logical
 level. In this paper, we give an account of the whole system, its
 peculiarities and its main applications.",
 paper = "Aspe11.pdf",
+ "In this paper we address the problem of reconstructing a higher
+ order, checkable proof object starting from a proof trace left by a
+ first order automatic proof searching procedure, in a restricted
+ equational framework. The automatic procedure is based on
+ superposition rules for the unit equality case. Proof transformation
+ techniques aimed to improve the readability of the final proof are
+ discussed.",
+ paper = "Aspe07.pdf"
}
\end{chunk}
+\end{chunk}
\index{Spitters, Bas}
\index{van der Weegen, Eelis}
+\index{Asperti, Andrea}
+\index{Coen, Claudio Sacerdoti}
+\index{Tassi, Enrico}
+\index{Zacchiroli, Stefano}
\begin{chunk}{axiom.bib}
@article{Spit11,
 author = "Spitters, Bas and van der Weegen, Eelis",
 title = {{Type Classes for Mathematics in Type Theory}},
 journal = "Math. Struct. Comput. Sci.",
 volume = "21",
 number = "4",
 pages = "795825",
 year = "2011",
+@inproceedings{Aspe06,
+ author = "Asperti, Andrea and Coen, Claudio Sacerdoti and
+ Tassi, Enrico and Zacchiroli, Stefano",
+ title = {{Crafting a Proof Assistant}},
+ booktitle = "Proc. Types 2006: Conf. of the Types Project",
+ year = "2006",
abstract =
 "The introduction of firstclass type classes in the Coq system calls
 for reexamination of the basic interfaces used for mathematical
 formalization in type theory. We present a new set of type classes for
 mathematics and take full advantage of their unique features to make
 practical a particularly flexible approach formerly thought
 infeasible. Thus, we address both traditional proof engineering
 challenges as well as new ones resulting from our ambition to build
 upon this development a library of constructive analysis in which
 abstraction penalties inhibiting efficient computation are reduced to
 a minimum.

 The base of our development consists of type classes representing a
 standard algebraic hierarchy, as well as portions of category theory
 and universal algebra. On this foundation we build a set of
 mathematically sound abstract interfaces for different kinds of
 numbers, succinctly expressed using categorical language and universal
 algebra constructions. Strategic use of type classes lets us support
 these highlevel theoryfriendly definitions while still enabling
 efficient implementations unhindered by gratuitous indirection,
 conversion or projection.

 Algebra thrives on the interplay between syntax and semantics. The
 Prologlike abilities of type class instance resolution allow us to
 conveniently define a quote function, thus facilitating the use of
 reflective techniques.",
 paper = "Spit11.pdf"
+ "Proof assistants are complex applications whose develop ment has
+ never been properly systematized or documented. This work is a
+ contribution in this direction, based on our experience with the
+ devel opment of Matita: a new interactive theorem prover based—as
+ Coq—on the Calculus of Inductive Constructions (CIC). In particular,
+ we analyze its architecture focusing on the dependencies of its
+ components, how they implement the main functionalities, and their
+ degree of reusability. The work is a first attempt to provide a ground
+ for a more direct com parison between different systems and to
+ highlight the common functionalities, not only in view of
+ reusability but also to encourage a more systematic comparison of
+ different softwares and architectural solutions.",
+ paper = "Aspe06.pdf"
}

+
\end{chunk}
+\index{Asperti, Andrea}
\index{Coen, Claudio Sacerdoti}
+\index{Tassi, Enrico}
+\index{Zacchiroli, Stefano}
\begin{chunk}{axiom.bib}
@article{Coen10,
 author = "Coen, Claudio Sacerdoti",
 title = {{Declarative Representation of Proof Terms}},
 journal = "J. Automated Reasoning",
 volume = "44",
 number = "12",
 pages = "2552",
 year = "2010",
+@article{Aspe07a,
+ author = "Asperti, Andrea and Coen, Claudio Sacerdoti and Tassi, Enrico
+ and Zacchiroli, Stefano",
+ title = {{User Interaction with the Matita Proof Assistant}},
+ journal = "J. of Automated Reasoning",
+ volume = "39",
+ number = "2",
+ pages = "109139",
abstract =
 "We present a declarative language inspired by the pseudonatural
 language previously used in Matita for the explanation of proof
 terms. We show how to compile the language to proof terms and how to
 automatically generate declarative scripts from proof terms. Then we
 investigate the relationship between the two translations, identifying
 the amount of proof structure preserved by compilation and
 regeneration of declarative scripts.",
 paper = "Coen10.pdf"
+ "Matita is a new, documentcentric, tacticbased interactive theorem
+ prover. This paper focuses on some of the distinctive features of the
+ user interaction with Matita, characterized mostly by the organization
+ of the library as a searchable knowledge base, the emphasis on a
+ highquality notational rendering, and the complex interplay between
+ syntax, presentation, and semantics.",
+ paper = "Aspe07a.pdf"
}
\end{chunk}
\index{Luo, Zhaohui}
+\index{Coen, Claudio Sacerdoti}
+\index{Tassi, Enrico}
+\index{Zacchiroli, Stefano}
\begin{chunk}{axiom.bib}
@inproceedings{Luox96,
 author = "Luo, Zhaohui",
 title = {{Coercive Subtyping in Type Theory}},
 booktitle = "CSL'96 Euro. Ass. for Comput. Sci. Logic",
 year = "1996",
+@inproceedings{Coen06,
+ author = "Coen, Claudio Sacerdoti and Tassi, Enrico and
+ Zacchiroli, Stefano",
+ title = {{Tinycals: Step by Step Teacticals}},
+ booktitle = "Proc. User Interfaces for Theorem Provers",
+ year = "2006",
+ pages = "125142",
abstract =
 "We propose and study coercive subtyping, a formal extension with
 subtyping of dependent type theories such as MartinLof's type theory
 [NPS90] and the type theory UTT [Luo94]. In this approach, subtyping
 with specied implicit coercions is treated as a feature at the level
 of the logical framework; in particular, subsumption and coercion are
 combined in such a way that the meaning of an object being in a
 supertype is given by coercive definition rules for the definitional
 equality. It is shown that this provides a conceptually simple and
 uniform framework to understand subtyping and coercion relations in
 type theories with sophisticated type structures such as inductive
 types and universes. The use of coercive subtyping in formal
 development and in reasoning about subsets of objects is discussed in
 the context of computerassisted formal reasoning.",
 paper = "Luox96.pdf"
+ "Most of the stateoftheart proof assistants are based on procedural
+ proof languages, scripts, and rely on LCF tacticals as the primary
+ tool for tactics composition. In this paper we discuss how these
+ ingredients do not interact well with user interfaces based on the
+ same interaction paradigm of Proof General (the de facto standard in
+ this field), identifying in the coarsegrainedness of tactical
+ evaluation the key problem. We propose tinycals as an alternative to a
+ subset of LCF tacticals, showing that the user does not experience the
+ same problem if tacticals are evaluated in a more finegrained
+ manner. We present the formal operational semantics of tinycals as
+ well as their implementation in the Matita proof assistant.",
+ paper = "Coen06.pdf"
}
\end{chunk}
\index{Luo, Zhaohui}
+\index{Padovani, Luca}
+\index{Zacchiroli, Stefano}
\begin{chunk}{axiom.bib}
@misc{Luox11,
 author = "Luo, Zhaohui",
 title = {{TypeTheoretical Semantics with Coercive Subtyping}},
 year = "2011",
 comment = "Lecture Notes 2011 ESSLLI Summer School, Ljubljana,
 Slovenia",
 paper = "Luox11.pdf"
+@inproceedings{Pado06,
+ author = "Padovani, Luca and Zacchiroli, Stefano",
+ title = {{From Notation to Semantics: There and Back Again}},
+ booktitle = "5th Conf. on Mathematical Knowledge Management",
+ year = "2006",
+ abstract =
+ "Mathematical notation is a structured, open, and ambiguous
+ language. In order to support mathematical notation in MKM
+ applications one must necessarily take into account presentational as
+ well as semantic aspects. The former are required to create a
+ familiar, comfortable, and usable interface to interact with. The
+ latter are necessary in order to process the information
+ meaningfully. In this paper we investigate a framework for dealing
+ with mathematical notation in a meaningful, extensible way, and we
+ show an effective instantiation of its architecture to the field of
+ interactive theorem proving. The framework builds upon wellknown
+ concepts and widelyused technologies and it can be easily adopted by
+ other MKM applications.",
+ paper = "Pado06.pdf"
}
\end{chunk}
\index{Bailey, Anthony}
+\index{Asperti, Andrea}
+\index{Guidi, Ferruccio}
+\index{Coen, Claudio Sacerdoti}
+\index{Tassi, Enrico}
+\index{Zacchiroli, Stefano}
\begin{chunk}{axiom.bib}
@phdthesis{Bail98,
 author = "Bailey, Anthony",
 title = {{The MachineChecked Literate Formalisation of Algebra
 in Type Theory}},
 school = "University of Manchester",
 year = "1998",
 link =
 "\url{http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.464.1249&rep=rep1&type=pdf}",
+@article{Aspe04,
+ author = "Asperti, Andrea and Guidi, Ferruccio and Coen, Claudio Sacerdoti
+ and Tassi, Enrico and Zacchiroli, Stefano",
+ title = {{A Content Based Mathematical Search Engine: Whelp}},
+ journal = "LNCS",
+ volume = "3839",
+ year = "2004",
+ pages = "1732",
+ isbn = "3540314288",
abstract =
 "I present a largescale formalisation within a type theory of a
 proof of a result from abstract algebra. The formalisation body
 consists of files that are machinechecked to ensure their
 correctness, and also processed to produce a report on the proof that
 is humanreadable. The resulting presentation is intended to approach
 being a standard informal account of some mathematics. In addition
 to presenting this proof, the thesis also identifies and examines
 problems in reconciling the formal nature of the development with the
 wish for it to be easy to read. It presents some tools and methodologies
 for solving these problems, and discusses the advantages and
 disadvantages of these solutions. In particular, it addresses the
 implementation and use of implicit coercions within the type theory,
 the styles of proof that can be used, and the borrowing of concepts
 from the literate programming paradigm. To be more specific, the
 algebra in question is a constructive version of the fundamental
 theorem of Galois Theory. The formalisation is developed within a
 variant of the Unified Theory of Types that is implemented by a
 modified version of the LEGO proofchecker.",
 paper = "Bail98.pdf",
 keywords = "axiomref"
+ "The prototype of a content based search engine for mathematical
+ knowledge supporting a small set of queries requiring matching and/or
+ typing operations is described. The prototype, called Whelp, exploits
+ a metadata approach for indexing the information that looks far more
+ flexible than traditional indexing techniques for structured
+ expressions like substitution, discrimination, or context trees. The
+ prototype has been instantiated to the standard library of the Coq
+ proof assistant extended with many user contributions.",
+ paper = "Aspe04.pdf"
}
\end{chunk}
\index{Mulligan, Dominic P.}
+\index{Coen, Claudio Sacerdoti}
+\index{Zacchiroli, Stefano}
\begin{chunk}{axiom.bib}
@misc{Mull13,
 author = "Mulligan, Dominic P.",
 title = {{Mosquito: An Aimplementation for HigherOrder Logic}},
 school = "University of Cambridge",
 year = "2013",
+@article{Coen04,
+ author = "Coen, Claudio Sacerdoti and Zacchiroli, Stefano",
+ title = {{Efficient Ambiguous Parsing of Mathematical Formulae}},
+ journal = "LNCS",
+ volume = "3119",
+ pages = "347362",
+ year = "2004",
+ isbn = "3540230297",
abstract =
 "We present Mosquito: an experimental stateless, pure, largely total
 LCFstyle implementation of higherorder logic using Haskell as a
 metalanguage. We discuss details of the logic implemented, kernel
 design, and novel proof state and tactic representations.",
 paper = "Mull13.pdf"
+ "Mathematical notation has the characteristic of being ambiguous:
+ operators can be overloaded and information that can be deduced is
+ often omitted. Mathematicians are used to this ambiguity and can
+ easily disambiguate a formula making use of the context and of their
+ ability to find the right interpretation.
+
+ Software applications that have to deal with formulae usually avoid
+ these issues by fixing an unambiguous input notation. This solution is
+ annoying for mathematicians because of the resulting tricky syntaxes
+ and becomes a show stopper to the simultaneous adoption of tools
+ characterized by different input languages.
+
+ In this paper we present an efficient algorithm suitable for ambiguous
+ parsing of mathematical formulae. The only requirement of the
+ algorithm is the existence of a 'validity' predicate over abstract
+ syntax trees of incomplete formulae with placeholders. This
+ requirement can be easily fulfilled in the applicative area of
+ interactive proof assistants, and in several other areas of
+ Mathematical Knowledge Management.",
+ paper = "Coen04.pdf"
}
\end{chunk}
+\index{Grabm\"uller, Martin}
+\begin{chunk}{axiom.bib}
+@misc{Grab06a,
+ author = "Grabmuller, Martin",
+ title = {{Algorithm W Step by Step}},
+ year = "2006",
+ link = "\url{http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7733&rep=rep1&type=pdf}",
+ abstract =
+ "In this paper we develop a complete implementation of the classic
+ algoirhtm W for HinleyMilner polymorphic type inference in Haskell",
+ paper = "Grab06a.pdf"
+}
+
+\end{chunk}
+\index{Hoare, C.A.R}
+\begin{chunk}{axiom.bib}
+@article{Hoar87,
+ author = "Hoare, C.A.R",
+ title = {{An Overview of Some Formal Methods for Program Design}},
+ journal = "Computer",
+ year = "1987",
+ volume = "20",
+ number = "9",
+ paper = "Hoar87.pdf"
+}
+
+\end{chunk}
+
+\index{Bowen, Jonathan P.}
+\index{Hinchey, Michael G.}
+\begin{chunk}{axiom.bib}
+@article{Bowe95,
+ author = "Bowen, Jonathan P. and Hinchey, Michael G.",
+ title = {{Seven More Myths of Formal Methods}},
+ journal = "IEEE Software",
+ volume = "12",
+ number = "4",
+ pages = "3441",
+ year = "1995",
+ abstract =
+ "New myths about formal methods are gaining tacit acceptance both
+ outside and inside the systemdevelopment community. The authors
+ address and dispel these myths based on their observations of
+ industrial projects. The myths include: formal methods delay the
+ development process; they lack tools; they replace traditional
+ engineering design methods; they only apply to software; are
+ unnecessary; not supported; and formal methods people always use
+ formal methods.",
+ paper = "Bowe95.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{McBride, Conor}
+\begin{chunk}{axiom.bib}
+@phdthesis{Mcbr99,
+ author = "McBride, Conor",
+ title = {{Dependently Typed Functional Programs and their Proofs}},
+ school = "University of Edinburgh",
+ year = "1999",
+ link = "\url{http://strictlypositive.org/thesis.pdf}",
+ abstract =
+ "Research in dependent type theories has, in the past, concentrated on
+ its use in the presentation of theorems and theoremproving. This
+ thesis is concerned mainly with the exploitation of the computational
+ aspects of type theory for programming, in a context where the
+ properties of programs may readily be specified and established. In
+ particular, it develops technology for programming with dependent
+ inductive families of datatypes and proving those programs correct. It
+ demonstrates the considerable advantage to be gained by indexing data
+ structures with pertinent characteristic information whose soundness
+ is ensured by typechecking, rather than human effort.
+
+ Type theory traditionally presents safe and terminating computation on
+ inductive datatypes by means of elimination rules which serve as
+ induction principles and, via their associated reduction behaviour,
+ recursion operators. In the programming language arena, these appear
+ somewhat cumbersome and give rise to unappealing code, complicated by
+ the inevitable interaction between case analysis on dependent types
+ and equational reasoning on their indices which must appear explicitly
+ in the terms. Thierry Coquand's proposal to equip type theory directly
+ with the kind of pattern matching notation to which functional
+ programmers have become used to over the past three decades offers a
+ remedy to many of these difficulties. However, the status of pattern
+ matching relative to the traditional elimination rules has until now
+ been in doubt. Pattern matching implies the uniqueness of identity
+ proofs, which Martin Hofmann showed underivable from the conventiaonal
+ definition of equality. This thesis shows that the adoption of this
+ uniqueness as axiomatic is sufficient to make pattern matching
+ admissible.
+
+ A datatype's elimination rule allows abstraction only over the whole
+ inductively defined family. In order to support pattern matching, the
+ application of such rules to specific instances of dependent families
+ has been systematised. The underlying analysis extends beyond
+ datatypes to other rules of a similar second order character,
+ suggesting they may have other roles to play in the specification,
+ verification and, perhaps, derivation of programs. The technique
+ developed shifts the specificity from the instantiation of the type's
+ indices into equational constraints on indices freely chosen, allowing
+ the elimination rule to be applied.
+
+ Elimination by this means leaves equational hypotheses in the
+ resulting subgoals, which must be solved if further progress is to be
+ made. The firstorder unification algorithm for constructor forms in
+ simmple types presented in [McB96] has been extended to cover
+ dependent datatypes as well, yielding completely automated solution of
+ a class of problems which can be syntactically defined.
+
+ The justification and operation of these techniques requires the
+ machine to construct and exploit a standardised collection of
+ auxiliary lemmas for each datatype. This is greatly facilitated by two
+ technical developments of interest in their own right:
+ \begin{itemize}
+ \item a more convenient definition of equality, with a relaxed
+ formulation rule allowing elements of different types to be compared,
+ but nonetheless equivalent to the usual equality plus the axiom of
+ uniqueness
+ \item a type theory, OLEG, which incorporates incomplete objects,
+ accounting for their 'holes' entirely within the typing judgments and,
+ novelly, not requiring any notion of explicit substitution to manage
+ their scopes.
+ \end{itemize}
+
+ A substantial prototype has been implemented, extending the proof
+ assistant LEGO. A number of programs are developed by way of
+ example. Chiefly, the increased expressivity of dependent datatypes is
+ shown to capture a standard firstorder unification algorithm within
+ the class of structurally recursive programs, removing any need for a
+ termination argument. Furthermore, the use of elimination rules in
+ specifying the components of the program simplifies significantly its
+ correctness proof.",
+ paper = "Mcbr99.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 81a0747..85b1be5 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5890,6 +5890,8 @@ src/axiomwebsite/documentation.html add Pierce quote about TeX
books/bookvolbib add references
20180109.01.tpd.patch
books/bookvolbib add references
+20180113.01.tpd.patch
+books/bookvolbib add references

1.9.1