From ecce66faf39352fb637bc6bf2e84585fd5276b56 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Fri, 9 Feb 2018 19:32:13 -0500
Subject: [PATCH] books/bookvolbib add references
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Goal: Proving Axiom Correct
\index{Hickey, Rich}
\begin{chunk}{axiom.bib}
@misc{Hick18,
author = "Hickey, Rich",
title = {{Effective Programs - 10 Years of Clojure}},
link = "\url{https://www.youtube.com/watch?v=2V1FtfBDsLU}",
year = "2018"
}
\end{chunk}
\index{Thiemann, Rene}
\index{Yamada, Akihisa}
\begin{chunk}{axiom.bib}
@article{Thie17,
author = "Thiemann, Rene and Yamada, Akihisa",
title = {{Polynomial Factorization: Proof Outline}},
journal = "Archive of Formal Proofs",
year = "2017",
link = "\url{https://www.isa-afp.org/browser_info/current/AFP/Polynomial_Factorization/outline.pdf}",
abstract =
"Based on existing libraries for polynomial interpolation and
matrices, we formalized several factorization algorihms for
polynomials, including Kronecker's algorithm for intgeer polynomials,
Yun's square-free factorization algorithm for field polynomials, and a
factorization algorithm which delivers root-free polynomials.
As side products, we developed division algorithms for polynomials
over integral domains, as well as primality-testing and prime
factorization algorithms for integers.",
paper = "Thie17.pdf",
keywords = "printed"
}
\end{chunk}
\index{Thiemann, Rene}
\index{Yamada, Akihisa}
\begin{chunk}{axiom.bib}
@article{Thie17a,
author = "Thiemann, Rene and Yamada, Akihisa",
title = {{Polynomial Factorization: Proof Document}},
journal = "Archive of Formal Proofs",
year = "2017",
link = "\url{https://www.isa-afp.org/browser_info/current/AFP/Polynomial_Factorization/document.pdf}",
abstract =
"Based on existing libraries for polynomial interpolation and
matrices, we formalized several factorization algorihms for
polynomials, including Kronecker's algorithm for intgeer polynomials,
Yun's square-free factorization algorithm for field polynomials, and a
factorization algorithm which delivers root-free polynomials.
As side products, we developed division algorithms for polynomials
over integral domains, as well as primality-testing and prime
factorization algorithms for integers.",
paper = "Thie17a.pdf"
}
\end{chunk}
\begin{Crocker, David}
\begin{chunk}{axiom.bib}
@inproceedings{Croc14,
author = "Crocker, David",
title = {{Can C++ Be Made as Safe as SPARK?}},
booktitle = "Proc 2014 HILT",
isbn = "978-1-4503-3217-0",
year = "2014",
abstract =
"SPARK offers a way to develop formally-verified software in a
language (Ada) that is designed with safety in mind and is further
restricted by the SPARK language subset. However, much critical
embedded software is developed in C or C++ We look at whether and how
benefits similar to those offered by the SPARK language subset and
associated tools can be brought to a C++ development environment.",
paper = "Croc14.pdf",
keywords = "printed"
}
\end{chunk}
\index{Filliatre, Jean-Christophe}
\begin{chunk}{axiom.bib}
@article{Fill03,
author = "Filliatre, Jean-Christophe",
title = {{Verification of Non-Functional Programs using Interpretations
in Type Theory}},
journal = "J. Functional Programming",
volume = "13",
number = "4",
pages = "709-745",
year = "2003",
abstract =
"We study the problem of certifying programs combining imperative
and functional features within the general framework of type
theory.
Type theory is a powerful specification language, which is
naturally suited for the proof of purely functional programs. To
deal with imperative programs, we propose a logical interpretation
of an annotated program as a partial proof of its
specification. The construction of the corresponding partial proof
term is based on a static analysis of the effects of the program
which excludes aliases. The missing subterms in the partial proof
term are seen as proof obligations, whose actual proofs are left
to the user. We show that the validity of those proof obligations
implies the total correctness of the program.
This work has been implemented in the Coq proof assistant. It
appears as a tactic taking an annotated program as argument and
generating a set of proof obligations. Several nontrivial
algorithms have been certified using this tactic.",
paper = "Fill03.pdf",
keywords = "printed"
}
\end{chunk}
\index{Garret, Ron}
\begin{chunk}{axiom.bib}
@misc{Garr14,
author = "Garret, Ron",
title = {{The Awesome Power of Theory}},
link = "\url{http://www.flownet.com/ron/lambda-calculus.html}",
year = "2014"
}
\end{chunk}
\index{Hoare, Charles Antony Richard}
\begin{chunk}{axiom.bib}
@article{Hoar71,
author = "Hoare, Charles Antony Richard",
title = {{Proof of a Program: FIND}},
journal = "Communications of the ACM",
volume = "14",
number = "1",
year = "1971",
abstract =
"A proof is given of the correctness of the algorithm 'Find.'
First, an informal description is given of the purpose of the
program and the method used. A systematic technique is described
for constructing the program proof during the process of coding
it, in such a way as to prevent the intrusion of logical
errors. The prrof of termination is treated as a separate
exercie. Finally, some conclusions related to general programming
methodology are drawn.",
paper = "Hoar71.pdf",
keywords = "printed"
}
\end{chunk}
\index{Filliatre, Jean-Christophe}
\begin{chunk}{axiom.bib}
@article{Fill07,
author = "Filliatre, Jean-Christophe",
title = {{Formal Proof of a Program: FIND}},
journal = "Science of Computer Programming",
volume = "64",
pages = "332-340",
year = "2007",
abstract =
"In 1971, C.A.R. Hoare gave the proof of correctness and
termination of a rather complex algorithm, in a paper entitled
{\sl Proof of a program: Find}. It is a handmade proof, where the
program is given together with its formal specification and where
each step is fully justified by mathematical reasoning. We present
here a formal proof of the same program in the system Coq, using
the recent tactic of the system developed to establish the total
correctness of imperative programs. We follow Hoare's paper as
closely as possible, keeping the same program and the same
specification. We show that we get exactly the same proof
obligations, which are proved in a straightforward way, following
the original paper. We also explain how more informal aspects of
Hoare's proof are formalized in the system Coq. This demonstrates
the adequacy of the system Coq in the process of certifying
imperative programs.",
paper = "Fill07.pdf",
keywords = "printed"
}
\end{chunk}
\index{Morris, F.L.}
\index{Jones, C.B.}
\begin{chunk}{axiom.bib}
@article{Morr84,
author = "Morris, F.L. and Jones, C.B.",
title = {{An Early Program Proof by Alan Turing}},
journal = "Annals of the History of Computing",
volume = "6",
number = "2",
year = "1984",
pages = "139-143",
abstract =
"The paper reproduces, with typographical corrections and
comments, a 1949 paper by Alan Turing that foreshadoes much
subsequent work in program proving.",
paper = "Morr84.pdf",
keywords = "printed"
}
\end{chunk}
\index{Kovacs, Laura}
\begin{chunk}{axiom.bib}
@article{Kova16,
author = "Kovacs, Laura",
title = {{Symbolic Computation and Automated Reasoning for Program
Analysis}},
journal = "LNCS",
volume = "9681",
pages = "20-27",
year = "2016",
abstract =
"This talk describes how a combination of symbolic computation
techniques with first-order theorem proving can be used for solving
some challenges of automating program analysis, in particular for
generating and proving properties about the logically complex parts of
software. The talk will first present how computer algebra methods,
such as Gröbner basis computation, quantifier elimination and
algebraic recurrence solving, help us in inferring properties of
program loops with non-trivial arithmetic. Typical properties inferred
by our work are loop invariants and expressions bounding the number of
loop iterations. The talk will then describe our work to generate
first-order properties of programs with unbounded data structures,
such as arrays. For doing so, we use saturation-based first-order
theorem proving and extend first- order provers with support for
program analysis. Since program analysis requires reasoning in the
combination of first-order theories of data structures, the talk
also discusses new features in first-order theorem proving, such as
inductive reasoning and built-in boolean sort. These extensions allow
us to express program properties directly in first-order logic and
hence use further first-order theorem provers to reason about program
properties.",
paper = "Kova16.pdf",
keywords = "printed"
}
\end{chunk}
\index{Avigad, Jeremy}
\begin{chunk}{axiom.bib}
@misc{Avig17a,
author = "Avigad, Jeremy",
title = {{Proof Theory}},
year = "2017",
abstract =
"Proof theory began in the 1920's as part of Hilbert's program,
which aimed to secrure the foundations of mathematics by modeling
infinitary mathematics with formal axiomatic systems and proving
those systems consistent using restricted, finitary means. The
program thus viewed mathematics as a system of reasoning with
precise linguistic norms, govenered by rules that can be described
and studied in concrete terms. Today such a viewpoint has
applications in mathematics, computer science, and the philosophy
of mathematics.",
paper = "Avig17a.pdf",
keywords = "private communication"
}
\end{chunk}
---
books/axiom.bib | 294 +++++++++++++++++++++++++++++++----
books/bookvolbib.pamphlet | 341 +++++++++++++++++++++++++++++++++++++----
changelog | 2 +
patch | 268 +++++++++++++++++++++++++++++++-
src/axiom-website/patches.html | 2 +
5 files changed, 845 insertions(+), 62 deletions(-)
diff --git a/books/axiom.bib b/books/axiom.bib
index d376861..e0c95db 100644
--- a/books/axiom.bib
+++ b/books/axiom.bib
@@ -611,7 +611,8 @@ paper = "Brea89.pdf"
than those of existing programming languages. In particular, it
provides a basis for the design of strongly typed object-oriented
languages",
- paper = "Card85.pdf"
+ paper = "Card85.pdf",
+ keywords = "printed"
}
@inproceedings{Card86,
@@ -1021,7 +1022,8 @@ paper = "Brea89.pdf"
characterization of type inference and type checking. This
characterization was facilitated by the use of logic programs to
represent types.",
- paper = "Frue91.pdf"
+ paper = "Frue91.pdf",
+ keywords = "printed"
}
@article{Fuhx89,
@@ -1548,7 +1550,8 @@ paper = "Brea89.pdf"
in TPC, these declarations can be queried the same way as any other
data. Type reflexivity is useful for browsing knowledge bases and,
potentially, for debugging logic programs.",
- paper = "Kife91.pdf"
+ paper = "Kife91.pdf",
+ keywords = "printed"
}
@book{Kirk89,
@@ -2402,7 +2405,8 @@ paper = "Brea89.pdf"
title = {{Logic Programming over Polymorphically Order-Sorted Types}},
school = "Fachbereich Informatik, Universitat Kaiserslautern",
year = "1989",
- paper = "Smol89a.pdf"
+ paper = "Smol89a.pdf",
+ keywords = "printed"
}
@misc{Stac17,
@@ -2837,7 +2841,7 @@ paper = "Brea89.pdf"
a variety of examples which will show some of the problems that remain
and that will require further research.",
paper = "Webe92b.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, printed"
}
@inproceedings{Wirs82,
@@ -7218,6 +7222,24 @@ paper = "Brea89.pdf"
paper = "Atte15.pdf, printed"
}
+@misc{Avig17b,
+ author = "Avigad, Jeremy",
+ title = {{Proof Theory}},
+ year = "2017",
+ abstract =
+ "Proof theory began in the 1920's as part of Hilbert's program,
+ which aimed to secrure the foundations of mathematics by modeling
+ infinitary mathematics with formal axiomatic systems and proving
+ those systems consistent using restricted, finitary means. The
+ program thus viewed mathematics as a system of reasoning with
+ precise linguistic norms, govenered by rules that can be described
+ and studied in concrete terms. Today such a viewpoint has
+ applications in mathematics, computer science, and the philosophy
+ of mathematics.",
+ paper = "Avig17b.pdf",
+ keywords = "private communication"
+}
+
@article{Bate85,
author = "Bates, Joseph L. and Constable, Robert L.",
title = {{Proofs as Programs}},
@@ -7608,6 +7630,23 @@ paper = "Brea89.pdf"
paper = "Coqu85.pdf, printed"
}
+@inproceedings{Croc14,
+ author = "Crocker, David",
+ title = {{Can C++ Be Made as Safe as SPARK?}},
+ booktitle = "Proc 2014 HILT",
+ isbn = "978-1-4503-3217-0",
+ year = "2014",
+ abstract =
+ "SPARK offers a way to develop formally-verified software in a
+ language (Ada) that is designed with safety in mind and is further
+ restricted by the SPARK language subset. However, much critical
+ embedded software is developed in C or C++ We look at whether and how
+ benefits similar to those offered by the SPARK language subset and
+ associated tools can be brought to a C++ development environment.",
+ paper = "Croc14.pdf",
+ keywords = "printed"
+}
+
@misc{Cyph17,
author = "Cypherpunks",
title = {{Chapter 4: Verification Techniques}},
@@ -7688,6 +7727,33 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@article{Fill07,
+ author = "Filliatre, Jean-Christophe",
+ title = {{Formal Proof of a Program: FIND}},
+ journal = "Science of Computer Programming",
+ volume = "64",
+ pages = "332-340",
+ year = "2007",
+ abstract =
+ "In 1971, C.A.R. Hoare gave the proof of correctness and
+ termination of a rather complex algorithm, in a paper entitled
+ {\sl Proof of a program: Find}. It is a handmade proof, where the
+ program is given together with its formal specification and where
+ each step is fully justified by mathematical reasoning. We present
+ here a formal proof of the same program in the system Coq, using
+ the recent tactic of the system developed to establish the total
+ correctness of imperative programs. We follow Hoare's paper as
+ closely as possible, keeping the same program and the same
+ specification. We show that we get exactly the same proof
+ obligations, which are proved in a straightforward way, following
+ the original paper. We also explain how more informal aspects of
+ Hoare's proof are formalized in the system Coq. This demonstrates
+ the adequacy of the system Coq in the process of certifying
+ imperative programs.",
+ paper = "Fill07.pdf",
+ keywords = "printed"
+}
+
@book{Font16,
author = "Font, Josep Marie",
title = {{Abstract Algebraic Logic: An Introductory Textbook}},
@@ -7696,6 +7762,13 @@ paper = "Brea89.pdf"
isbn = "978-1-84890-207-7"
}
+@misc{Garr14,
+ author = "Garret, Ron",
+ title = {{The Awesome Power of Theory}},
+ link = "\url{http://www.flownet.com/ron/lambda-calculus.html}",
+ year = "2014"
+}
+
@article{Glas94,
author = "Glass, Robert L.",
title = {{The Software-Research Crisis}},
@@ -7751,6 +7824,33 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@misc{Hick18,
+ author = "Hickey, Rich",
+ title = {{Effective Programs - 10 Years of Clojure}},
+ link = "\url{https://www.youtube.com/watch?v=2V1FtfBDsLU}",
+ year = "2018"
+}
+
+@article{Hoar71,
+ author = "Hoare, Charles Antony Richard",
+ title = {{Proof of a Program: FIND}},
+ journal = "Communications of the ACM",
+ volume = "14",
+ number = "1",
+ year = "1971",
+ abstract =
+ "A proof is given of the correctness of the algorithm 'Find.'
+ First, an informal description is given of the purpose of the
+ program and the method used. A systematic technique is described
+ for constructing the program proof during the process of coding
+ it, in such a way as to prevent the intrusion of logical
+ errors. The prrof of termination is treated as a separate
+ exercie. Finally, some conclusions related to general programming
+ methodology are drawn.",
+ paper = "Hoar71.pdf",
+ keywords = "printed"
+}
+
@article{Hoar87,
author = "Hoare, Charles Antony Richard",
title = {{An Overview of Some Formal Methods for Program Design}},
@@ -7785,6 +7885,39 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@article{Kova16,
+ author = "Kovacs, Laura",
+ title = {{Symbolic Computation and Automated Reasoning for Program
+ Analysis}},
+ journal = "LNCS",
+ volume = "9681",
+ pages = "20-27",
+ year = "2016",
+ abstract =
+ "This talk describes how a combination of symbolic computation
+ techniques with first-order theorem proving can be used for solving
+ some challenges of automating program analysis, in particular for
+ generating and proving properties about the logically complex parts of
+ software. The talk will first present how computer algebra methods,
+ such as Gröbner basis computation, quantifier elimination and
+ algebraic recurrence solving, help us in inferring properties of
+ program loops with non-trivial arithmetic. Typical properties inferred
+ by our work are loop invariants and expressions bounding the number of
+ loop iterations. The talk will then describe our work to generate
+ first-order properties of programs with unbounded data structures,
+ such as arrays. For doing so, we use saturation-based first-order
+ theorem proving and extend first- order provers with support for
+ program analysis. Since program analysis requires reasoning in the
+ combination of first-order theories of data structures, the talk
+ also discusses new features in first-order theorem proving, such as
+ inductive reasoning and built-in boolean sort. These extensions allow
+ us to express program properties directly in first-order logic and
+ hence use further first-order theorem provers to reason about program
+ properties.",
+ paper = "Kova16.pdf",
+ keywords = "printed"
+}
+
@book{Laka76,
author = "Lakatos, Imre",
title = {{Proofs and Refutations}},
@@ -8087,6 +8220,22 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@article{Morr84,
+ author = "Morris, F.L. and Jones, C.B.",
+ title = {{An Early Program Proof by Alan Turing}},
+ journal = "Annals of the History of Computing",
+ volume = "6",
+ number = "2",
+ year = "1984",
+ pages = "139-143",
+ abstract =
+ "The paper reproduces, with typographical corrections and
+ comments, a 1949 paper by Alan Turing that foreshadoes much
+ subsequent work in program proving.",
+ paper = "Morr84.pdf",
+ keywords = "printed"
+}
+
@misc{Mull13,
author = "Mulligan, Dominic P.",
title = {{Mosquito: An Aimplementation for Higher-Order Logic}},
@@ -8245,6 +8394,45 @@ paper = "Brea89.pdf"
paper = "Scot76.pdf"
}
+@article{Thie17,
+ author = "Thiemann, Rene and Yamada, Akihisa",
+ title = {{Polynomial Factorization: Proof Outline}},
+ journal = "Archive of Formal Proofs",
+ year = "2017",
+ link = "\url{https://www.isa-afp.org/browser_info/current/AFP/Polynomial_Factorization/outline.pdf}",
+ abstract =
+ "Based on existing libraries for polynomial interpolation and
+ matrices, we formalized several factorization algorihms for
+ polynomials, including Kronecker's algorithm for intgeer polynomials,
+ Yun's square-free factorization algorithm for field polynomials, and a
+ factorization algorithm which delivers root-free polynomials.
+
+ As side products, we developed division algorithms for polynomials
+ over integral domains, as well as primality-testing and prime
+ factorization algorithms for integers.",
+ paper = "Thie17.pdf",
+ keywords = "printed"
+}
+
+@article{Thie17a,
+ author = "Thiemann, Rene and Yamada, Akihisa",
+ title = {{Polynomial Factorization: Proof Document}},
+ journal = "Archive of Formal Proofs",
+ year = "2017",
+ link = "\url{https://www.isa-afp.org/browser_info/current/AFP/Polynomial_Factorization/document.pdf}",
+ abstract =
+ "Based on existing libraries for polynomial interpolation and
+ matrices, we formalized several factorization algorihms for
+ polynomials, including Kronecker's algorithm for intgeer polynomials,
+ Yun's square-free factorization algorithm for field polynomials, and a
+ factorization algorithm which delivers root-free polynomials.
+
+ As side products, we developed division algorithms for polynomials
+ over integral domains, as well as primality-testing and prime
+ factorization algorithms for integers.",
+ paper = "Thie17a.pdf"
+}
+
@article{Tryb92,
author = "Trybulec, Zinaida and Swieczkowska, Halina",
title = {{Some Remarks on The Language of Mathematical Texts}},
@@ -8354,7 +8542,8 @@ paper = "Brea89.pdf"
and similarities in their approaches, highlight potentials of
combining their strengths, and discuss the challenges that come with
this task.",
- paper = "Abra15.pdf"
+ paper = "Abra15.pdf",
+ keywords = "printed"
}
@inproceedings{Abra16a,
@@ -8549,7 +8738,7 @@ paper = "Brea89.pdf"
discovering closed recursive forms. Thus, its proof is both more
straightforward to construct and easier to validate than a direct
proof of the inference algorithm would be.",
- paper = "Aker93.pdf"
+ paper = "Aker93.pdf, printed"
}
@inproceedings{Aran05,
@@ -8666,7 +8855,7 @@ paper = "Brea89.pdf"
link =
"\url{http://github.com/leanprover/lean2/blob/master/library/data/nat/gcd.lean}",
year = "2014",
- keywords = "CAS-Proof"
+ keywords = "CAS-Proof, printed"
}
@misc{Avig16,
@@ -10671,7 +10860,7 @@ paper = "Brea89.pdf"
execution of the algorithms, equivalent to testing over infinite test
sets, aids in debugging, while strengthening beliefs that the correctness
of results is an algebraic truth rather than an accident.",
- paper = "Fate02a.pdf, CAS-Proof"
+ paper = "Fate02a.pdf, CAS-Proof, printed"
}
@inproceedings{Fate03a,
@@ -10737,7 +10926,8 @@ paper = "Brea89.pdf"
title = {{Function and Concept}},
year = "1891",
link = "\url{http://fitelson.org/proseminar/frege_fac.pdf}",
- paper = "Frege.pdf"
+ paper = "Frege.pdf",
+ keywords = "printed"
}
@book{Frey90,
@@ -11292,7 +11482,8 @@ paper = "Brea89.pdf"
summer school in 2011. The course consists of an introduction to
separation logic, with a slant towards its use in automatic program
verification and analysis.",
- paper = "Hear12.pdf"
+ paper = "Hear12.pdf",
+ keywords = "printed"
}
@misc{Heer02,
@@ -11334,7 +11525,8 @@ paper = "Brea89.pdf"
a formal proof of a simple theorem is displayed. Finally, it is argued
that important advantages, both theoretical and practical, may follow
from a pursuance of these topics",
- paper = "Hoar69.pdf"
+ paper = "Hoar69.pdf",
+ keywords = "printed"
}
@inproceedings{Homa94a,
@@ -12257,7 +12449,8 @@ paper = "Brea89.pdf"
automated theorem-proving program Otter was used extensively to
construct sets of candidate axioms and to search for and nd proofs
that given candidate axioms are in fact single axioms.",
- paper = "Mccu93.pdf"
+ paper = "Mccu93.pdf",
+ keywords = "printed"
}
@article{Medi04,
@@ -12302,7 +12495,8 @@ paper = "Brea89.pdf"
a multi-radix and multi-precision implementation free from underflow
and overflow. It provides the basic arithmetic operators and a few
elementary functions.",
- paper = "Melq12.pdf"
+ paper = "Melq12.pdf",
+ keywords = "printed"
}
@book{Mend87,
@@ -12601,7 +12795,7 @@ paper = "Brea89.pdf"
balance efficiency and usability. We describe the central design
goals, and the means by which they are achieved.",
paper = "Mour15.pdf",
- keywords = "coercion"
+ keywords = "coercion, printed"
}
@misc{Mour16,
@@ -13012,7 +13206,8 @@ paper = "Brea89.pdf"
pages = "538-543",
year = "1991",
publisher = "Morgan Kaufmann",
- paper = "Pell91.pdf"
+ paper = "Pell91.pdf",
+ keywords = "printed"
}
@inproceedings{Pfen88,
@@ -13323,7 +13518,8 @@ paper = "Brea89.pdf"
including extensions that permit unrestricted address arithmetic,
dynamically allocated arrays, and recursive procedures. We will also
discuss promising future directions.",
- paper = "Reyn02.pdf"
+ paper = "Reyn02.pdf",
+ keywords = "printed"
}
@article{Reyn05,
@@ -13340,6 +13536,7 @@ paper = "Brea89.pdf"
imperative programs that use shared mutable data structures or
shared-memory concurrency",
paper = "Reyn05.pdf",
+ keywords = "printed"
}
@misc{Robe15,
@@ -14882,7 +15079,8 @@ paper = "Brea89.pdf"
formal literature, and where they have been, there is one recent
development indicating that the question is more delicate than had
been supposed.",
- paper = "Dave16.pdf"
+ paper = "Dave16.pdf",
+ keywords = "printed"
}
@inproceedings{Gedd89,
@@ -18980,7 +19178,8 @@ paper = "Brea89.pdf"
prove them with computer algebra using the Cylindrical Algebraic
Decomposition algorithm. This is an example collection for standard
applications of this algorithm, intended as a guide for potential users.",
- paper = "Kaue11.pdf"
+ paper = "Kaue11.pdf",
+ keywords = "printed"
}
@book{LaVa06,
@@ -20780,7 +20979,8 @@ paper = "Brea89.pdf"
title = {{Dependently Typed Programming in Agda}},
link = "\url{http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf}",
year = "2008",
- paper = "Nore08.pdf"
+ paper = "Nore08.pdf",
+ keywords = "printed"
}
@phdthesis{Paul14,
@@ -22936,7 +23136,7 @@ paper = "Brea89.pdf"
language facilities as well as the underlying manipulation routines
may be interactively extended by an experienced user.",
paper = "Blai70a.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, printed"
}
@InProceedings{Bosm94,
@@ -23732,7 +23932,7 @@ paper = "Brea89.pdf"
pages = "1-18",
year = "1985",
paper = "Cavi85.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, printed"
}
@misc{Cavi03,
@@ -24396,7 +24596,7 @@ paper = "Brea89.pdf"
number = "TR5/92",
year = "1992",
paper = "Dave92a.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, printed"
}
@misc{Dave99,
@@ -25373,7 +25573,7 @@ paper = "Brea89.pdf"
exists. Finally, we present a demonstration implementation of this
automated coerion algorithm in Axiom.",
paper = "Doye97.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, printed"
}
@inproceedings{Doye99,
@@ -28017,7 +28217,7 @@ paper = "Brea89.pdf"
functor of RUSSELL) and leads to a very powerful notion of abstract
algorithms missing from other work on data types known to the authors.",
paper = "Jenk81.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, printed"
}
@inproceedings{Jenk84a,
@@ -28080,7 +28280,7 @@ paper = "Brea89.pdf"
be covered in the SCRATCHPAD System Programming Manual [SCRA84] and an
expanded version of this paper will serve as a primer for SCRATCHPAD
users [JESU84].",
- keywords = "axiomref",
+ keywords = "axiomref, printed",
beebe = "Jenks:1984:PKN"
}
@@ -28675,7 +28875,7 @@ paper = "Brea89.pdf"
on stochastic differentials, of the Mardia-Dryden distribution from
statistical shape theory.",
paper = "Kend01.pdf",
- keywords = "axiomref, CAS-Proof",
+ keywords = "axiomref, CAS-Proof, printed",
beebe = "Kendall:2001:SIC"
}
@@ -32187,7 +32387,7 @@ paper = "Brea89.pdf"
user friendly and relatively weakly typed front end for the strongly
typed programming language.",
paper = "Suto87.pdf",
- keywords = "axiomref",
+ keywords = "axiomref, printed",
beebe = "Sutor:1987:TICb"
}
@@ -32350,7 +32550,8 @@ paper = "Brea89.pdf"
author = "Unknown",
title = {{Hindley-Milner Type Inference}},
link = "\url{https://www7.in.tum.de/um/courses/seminar/sove/SS2013/final/hindley-milner.slides.pdf}",
- paper = "Unkn13.pdf"
+ paper = "Unkn13.pdf",
+ keywords = "printed"
}
@@ -33640,7 +33841,7 @@ paper = "Brea89.pdf"
year = "2012",
comment = "slides",
paper = "Avig12.pdf",
- keywords ="CAS-Proof"
+ keywords ="CAS-Proof, printed"
}
@misc{Avig14a,
@@ -35168,6 +35369,39 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@article{Fill03,
+ author = "Filliatre, Jean-Christophe",
+ title = {{Verification of Non-Functional Programs using Interpretations
+ in Type Theory}},
+ journal = "J. Functional Programming",
+ volume = "13",
+ number = "4",
+ pages = "709-745",
+ year = "2003",
+ abstract =
+ "We study the problem of certifying programs combining imperative
+ and functional features within the general framework of type
+ theory.
+
+ Type theory is a powerful specification language, which is
+ naturally suited for the proof of purely functional programs. To
+ deal with imperative programs, we propose a logical interpretation
+ of an annotated program as a partial proof of its
+ specification. The construction of the corresponding partial proof
+ term is based on a static analysis of the effects of the program
+ which excludes aliases. The missing subterms in the partial proof
+ term are seen as proof obligations, whose actual proofs are left
+ to the user. We show that the validity of those proof obligations
+ implies the total correctness of the program.
+
+ This work has been implemented in the Coq proof assistant. It
+ appears as a tactic taking an annotated program as argument and
+ generating a set of proof obligations. Several nontrivial
+ algorithms have been certified using this tactic.",
+ paper = "Fill03.pdf",
+ keywords = "printed"
+}
+
@misc{Fitc74,
author = "Fitch, J.P.",
title = {{CAMAL Users Manual}},
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 1cedf33..cf087df 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -1029,7 +1029,8 @@ paper = "Brea89.pdf"
than those of existing programming languages. In particular, it
provides a basis for the design of strongly typed object-oriented
languages",
- paper = "Card85.pdf"
+ paper = "Card85.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ -1567,7 +1568,8 @@ paper = "Brea89.pdf"
characterization of type inference and type checking. This
characterization was facilitated by the use of logic programs to
represent types.",
- paper = "Frue91.pdf"
+ paper = "Frue91.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ -2278,7 +2280,8 @@ paper = "Brea89.pdf"
in TPC, these declarations can be queried the same way as any other
data. Type reflexivity is useful for browsing knowledge bases and,
potentially, for debugging logic programs.",
- paper = "Kife91.pdf"
+ paper = "Kife91.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ -3388,7 +3391,8 @@ paper = "Brea89.pdf"
title = {{Logic Programming over Polymorphically Order-Sorted Types}},
school = "Fachbereich Informatik, Universitat Kaiserslautern",
year = "1989",
- paper = "Smol89a.pdf"
+ paper = "Smol89a.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ -3917,7 +3921,7 @@ paper = "Brea89.pdf"
a variety of examples which will show some of the problems that remain
and that will require further research.",
paper = "Webe92b.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, printed"
}
\end{chunk}
@@ -9795,6 +9799,28 @@ when shown in factored form.
\end{chunk}
+\index{Avigad, Jeremy}
+\begin{chunk}{axiom.bib}
+@misc{Avig17b,
+ author = "Avigad, Jeremy",
+ title = {{Proof Theory}},
+ year = "2017",
+ abstract =
+ "Proof theory began in the 1920's as part of Hilbert's program,
+ which aimed to secrure the foundations of mathematics by modeling
+ infinitary mathematics with formal axiomatic systems and proving
+ those systems consistent using restricted, finitary means. The
+ program thus viewed mathematics as a system of reasoning with
+ precise linguistic norms, govenered by rules that can be described
+ and studied in concrete terms. Today such a viewpoint has
+ applications in mathematics, computer science, and the philosophy
+ of mathematics.",
+ paper = "Avig17b.pdf",
+ keywords = "private communication"
+}
+
+\end{chunk}
+
\index{Bates, Joseph L.}
\index{Constable, Robert L.}
\begin{chunk}{axiom.bib}
@@ -10257,6 +10283,27 @@ when shown in factored form.
\end{chunk}
+\index{Crocker, David}
+\begin{chunk}{axiom.bib}
+@inproceedings{Croc14,
+ author = "Crocker, David",
+ title = {{Can C++ Be Made as Safe as SPARK?}},
+ booktitle = "Proc 2014 HILT",
+ isbn = "978-1-4503-3217-0",
+ year = "2014",
+ abstract =
+ "SPARK offers a way to develop formally-verified software in a
+ language (Ada) that is designed with safety in mind and is further
+ restricted by the SPARK language subset. However, much critical
+ embedded software is developed in C or C++ We look at whether and how
+ benefits similar to those offered by the SPARK language subset and
+ associated tools can be brought to a C++ development environment.",
+ paper = "Croc14.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\begin{chunk}{axiom.bib}
@misc{Cyph17,
author = "Cypherpunks",
@@ -10352,6 +10399,37 @@ when shown in factored form.
\end{chunk}
+\index{Filliatre, Jean-Christophe}
+\begin{chunk}{axiom.bib}
+@article{Fill07,
+ author = "Filliatre, Jean-Christophe",
+ title = {{Formal Proof of a Program: FIND}},
+ journal = "Science of Computer Programming",
+ volume = "64",
+ pages = "332-340",
+ year = "2007",
+ abstract =
+ "In 1971, C.A.R. Hoare gave the proof of correctness and
+ termination of a rather complex algorithm, in a paper entitled
+ {\sl Proof of a program: Find}. It is a handmade proof, where the
+ program is given together with its formal specification and where
+ each step is fully justified by mathematical reasoning. We present
+ here a formal proof of the same program in the system Coq, using
+ the recent tactic of the system developed to establish the total
+ correctness of imperative programs. We follow Hoare's paper as
+ closely as possible, keeping the same program and the same
+ specification. We show that we get exactly the same proof
+ obligations, which are proved in a straightforward way, following
+ the original paper. We also explain how more informal aspects of
+ Hoare's proof are formalized in the system Coq. This demonstrates
+ the adequacy of the system Coq in the process of certifying
+ imperative programs.",
+ paper = "Fill07.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Font, Josep Marie}
\begin{chunk}{axiom.bib}
@book{Font16,
@@ -10364,6 +10442,17 @@ when shown in factored form.
\end{chunk}
+\index{Garret, Ron}
+\begin{chunk}{axiom.bib}
+@misc{Garr14,
+ author = "Garret, Ron",
+ title = {{The Awesome Power of Theory}},
+ link = "\url{http://www.flownet.com/ron/lambda-calculus.html}",
+ year = "2014"
+}
+
+\end{chunk}
+
\index{Glass, Robert L.}
\begin{chunk}{axiom.bib}
@article{Glas94,
@@ -10435,6 +10524,41 @@ when shown in factored form.
\end{chunk}
+\index{Hickey, Rich}
+\begin{chunk}{axiom.bib}
+@misc{Hick18,
+ author = "Hickey, Rich",
+ title = {{Effective Programs - 10 Years of Clojure}},
+ link = "\url{https://www.youtube.com/watch?v=2V1FtfBDsLU}",
+ year = "2018"
+}
+
+\end{chunk}
+
+\index{Hoare, Charles Antony Richard}
+\begin{chunk}{axiom.bib}
+@article{Hoar71,
+ author = "Hoare, Charles Antony Richard",
+ title = {{Proof of a Program: FIND}},
+ journal = "Communications of the ACM",
+ volume = "14",
+ number = "1",
+ year = "1971",
+ abstract =
+ "A proof is given of the correctness of the algorithm 'Find.'
+ First, an informal description is given of the purpose of the
+ program and the method used. A systematic technique is described
+ for constructing the program proof during the process of coding
+ it, in such a way as to prevent the intrusion of logical
+ errors. The prrof of termination is treated as a separate
+ exercie. Finally, some conclusions related to general programming
+ methodology are drawn.",
+ paper = "Hoar71.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Hoare, Charles Antony Richard}
\begin{chunk}{axiom.bib}
@article{Hoar87,
@@ -10477,6 +10601,43 @@ when shown in factored form.
\end{chunk}
+\index{Kovacs, Laura}
+\begin{chunk}{axiom.bib}
+@article{Kova16,
+ author = "Kovacs, Laura",
+ title = {{Symbolic Computation and Automated Reasoning for Program
+ Analysis}},
+ journal = "LNCS",
+ volume = "9681",
+ pages = "20-27",
+ year = "2016",
+ abstract =
+ "This talk describes how a combination of symbolic computation
+ techniques with first-order theorem proving can be used for solving
+ some challenges of automating program analysis, in particular for
+ generating and proving properties about the logically complex parts of
+ software. The talk will first present how computer algebra methods,
+ such as Gröbner basis computation, quantifier elimination and
+ algebraic recurrence solving, help us in inferring properties of
+ program loops with non-trivial arithmetic. Typical properties inferred
+ by our work are loop invariants and expressions bounding the number of
+ loop iterations. The talk will then describe our work to generate
+ first-order properties of programs with unbounded data structures,
+ such as arrays. For doing so, we use saturation-based first-order
+ theorem proving and extend first- order provers with support for
+ program analysis. Since program analysis requires reasoning in the
+ combination of first-order theories of data structures, the talk
+ also discusses new features in first-order theorem proving, such as
+ inductive reasoning and built-in boolean sort. These extensions allow
+ us to express program properties directly in first-order logic and
+ hence use further first-order theorem provers to reason about program
+ properties.",
+ paper = "Kova16.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Lakatos, Imre}
\begin{chunk}{axiom.bib}
@book{Laka76,
@@ -10830,6 +10991,27 @@ when shown in factored form.
\end{chunk}
+\index{Morris, F.L.}
+\index{Jones, C.B.}
+\begin{chunk}{axiom.bib}
+@article{Morr84,
+ author = "Morris, F.L. and Jones, C.B.",
+ title = {{An Early Program Proof by Alan Turing}},
+ journal = "Annals of the History of Computing",
+ volume = "6",
+ number = "2",
+ year = "1984",
+ pages = "139-143",
+ abstract =
+ "The paper reproduces, with typographical corrections and
+ comments, a 1949 paper by Alan Turing that foreshadoes much
+ subsequent work in program proving.",
+ paper = "Morr84.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Mulligan, Dominic P.}
\begin{chunk}{axiom.bib}
@misc{Mull13,
@@ -11023,6 +11205,55 @@ when shown in factored form.
\end{chunk}
+\index{Thiemann, Rene}
+\index{Yamada, Akihisa}
+\begin{chunk}{axiom.bib}
+@article{Thie17,
+ author = "Thiemann, Rene and Yamada, Akihisa",
+ title = {{Polynomial Factorization: Proof Outline}},
+ journal = "Archive of Formal Proofs",
+ year = "2017",
+ link = "\url{https://www.isa-afp.org/browser_info/current/AFP/Polynomial_Factorization/outline.pdf}",
+ abstract =
+ "Based on existing libraries for polynomial interpolation and
+ matrices, we formalized several factorization algorihms for
+ polynomials, including Kronecker's algorithm for intgeer polynomials,
+ Yun's square-free factorization algorithm for field polynomials, and a
+ factorization algorithm which delivers root-free polynomials.
+
+ As side products, we developed division algorithms for polynomials
+ over integral domains, as well as primality-testing and prime
+ factorization algorithms for integers.",
+ paper = "Thie17.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Thiemann, Rene}
+\index{Yamada, Akihisa}
+\begin{chunk}{axiom.bib}
+@article{Thie17a,
+ author = "Thiemann, Rene and Yamada, Akihisa",
+ title = {{Polynomial Factorization: Proof Document}},
+ journal = "Archive of Formal Proofs",
+ year = "2017",
+ link = "\url{https://www.isa-afp.org/browser_info/current/AFP/Polynomial_Factorization/document.pdf}",
+ abstract =
+ "Based on existing libraries for polynomial interpolation and
+ matrices, we formalized several factorization algorihms for
+ polynomials, including Kronecker's algorithm for intgeer polynomials,
+ Yun's square-free factorization algorithm for field polynomials, and a
+ factorization algorithm which delivers root-free polynomials.
+
+ As side products, we developed division algorithms for polynomials
+ over integral domains, as well as primality-testing and prime
+ factorization algorithms for integers.",
+ paper = "Thie17a.pdf"
+}
+
+\end{chunk}
+
\index{Trybulec, Zinaida}
\index{Swieczkowska, Halina}
\begin{chunk}{axiom.bib}
@@ -11162,7 +11393,8 @@ when shown in factored form.
and similarities in their approaches, highlight potentials of
combining their strengths, and discuss the challenges that come with
this task.",
- paper = "Abra15.pdf"
+ paper = "Abra15.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ -11430,7 +11662,7 @@ when shown in factored form.
discovering closed recursive forms. Thus, its proof is both more
straightforward to construct and easier to validate than a direct
proof of the inference algorithm would be.",
- paper = "Aker93.pdf"
+ paper = "Aker93.pdf, printed"
}
\end{chunk}
@@ -11579,7 +11811,7 @@ when shown in factored form.
link =
"\url{http://github.com/leanprover/lean2/blob/master/library/data/nat/gcd.lean}",
year = "2014",
- keywords = "CAS-Proof"
+ keywords = "CAS-Proof, printed"
}
\end{chunk}
@@ -14191,7 +14423,7 @@ when shown in factored form.
execution of the algorithms, equivalent to testing over infinite test
sets, aids in debugging, while strengthening beliefs that the correctness
of results is an algebraic truth rather than an accident.",
- paper = "Fate02a.pdf, CAS-Proof"
+ paper = "Fate02a.pdf, CAS-Proof, printed"
}
\end{chunk}
@@ -14277,7 +14509,8 @@ when shown in factored form.
title = {{Function and Concept}},
year = "1891",
link = "\url{http://fitelson.org/proseminar/frege_fac.pdf}",
- paper = "Frege.pdf"
+ paper = "Frege.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ -14996,7 +15229,8 @@ when shown in factored form.
summer school in 2011. The course consists of an introduction to
separation logic, with a slant towards its use in automatic program
verification and analysis.",
- paper = "Hear12.pdf"
+ paper = "Hear12.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ -15048,7 +15282,8 @@ when shown in factored form.
a formal proof of a simple theorem is displayed. Finally, it is argued
that important advantages, both theoretical and practical, may follow
from a pursuance of these topics",
- paper = "Hoar69.pdf"
+ paper = "Hoar69.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ -16199,7 +16434,8 @@ when shown in factored form.
automated theorem-proving program Otter was used extensively to
construct sets of candidate axioms and to search for and nd proofs
that given candidate axioms are in fact single axioms.",
- paper = "Mccu93.pdf"
+ paper = "Mccu93.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ -16259,7 +16495,8 @@ when shown in factored form.
a multi-radix and multi-precision implementation free from underflow
and overflow. It provides the basic arithmetic operators and a few
elementary functions.",
- paper = "Melq12.pdf"
+ paper = "Melq12.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ -16626,7 +16863,7 @@ when shown in factored form.
balance efficiency and usability. We describe the central design
goals, and the means by which they are achieved.",
paper = "Mour15.pdf",
- keywords = "coercion"
+ keywords = "coercion, printed"
}
\end{chunk}
@@ -17139,7 +17376,8 @@ when shown in factored form.
pages = "538-543",
year = "1991",
publisher = "Morgan Kaufmann",
- paper = "Pell91.pdf"
+ paper = "Pell91.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ -17533,7 +17771,8 @@ when shown in factored form.
including extensions that permit unrestricted address arithmetic,
dynamically allocated arrays, and recursive procedures. We will also
discuss promising future directions.",
- paper = "Reyn02.pdf"
+ paper = "Reyn02.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ -17554,6 +17793,7 @@ when shown in factored form.
imperative programs that use shared mutable data structures or
shared-memory concurrency",
paper = "Reyn05.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ -20180,7 +20420,8 @@ SIAM J. Computing Vol 18 pp 893-905 (1989)
formal literature, and where they have been, there is one recent
development indicating that the question is more delicate than had
been supposed.",
- paper = "Dave16.pdf"
+ paper = "Dave16.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ -25972,7 +26213,8 @@ Proc ISSAC 97 pp172-175 (1997)
prove them with computer algebra using the Cylindrical Algebraic
Decomposition algorithm. This is an example collection for standard
applications of this algorithm, intended as a guide for potential users.",
- paper = "Kaue11.pdf"
+ paper = "Kaue11.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ -28275,7 +28517,8 @@ Proc ISSAC 97 pp172-175 (1997)
title = {{Dependently Typed Programming in Agda}},
link = "\url{http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf}",
year = "2008",
- paper = "Nore08.pdf"
+ paper = "Nore08.pdf",
+ keywords = "printed"
}
\end{chunk}
@@ -31171,7 +31414,7 @@ American Mathematical Society (1994)
language facilities as well as the underlying manipulation routines
may be interactively extended by an experienced user.",
paper = "Blai70a.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, printed"
}
\end{chunk}
@@ -32739,7 +32982,7 @@ Universit{\"a}t Karsruhe, Karlsruhe, Germany 1994
pages = "1-18",
year = "1985",
paper = "Cavi85.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, printed"
}
\end{chunk}
@@ -33764,7 +34007,7 @@ April 8-9, 2013 Portland Oregon
number = "TR5/92",
year = "1992",
paper = "Dave92a.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, printed"
}
\end{chunk}
@@ -35371,7 +35614,7 @@ ISBN 1-58113-073-2 LCCN QA76.95.I57 1999
exists. Finally, we present a demonstration implementation of this
automated coerion algorithm in Axiom.",
paper = "Doye97.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, printed"
}
\end{chunk}
@@ -39532,7 +39775,7 @@ Watson Research Center, Yorktown Heights, NY, USA, 1969 RC2968 July 1970
functor of RUSSELL) and leads to a very powerful notion of abstract
algorithms missing from other work on data types known to the authors.",
paper = "Jenk81.pdf",
- keywords = "axiomref"
+ keywords = "axiomref, printed"
}
\end{chunk}
@@ -39626,7 +39869,7 @@ SIGPLAN Notices, New York: Association for Computing Machiner, Nov 1981
be covered in the SCRATCHPAD System Programming Manual [SCRA84] and an
expanded version of this paper will serve as a primer for SCRATCHPAD
users [JESU84].",
- keywords = "axiomref",
+ keywords = "axiomref, printed",
beebe = "Jenks:1984:PKN"
}
@@ -40631,7 +40874,7 @@ SIGSAM Communications in Computer Algebra, 157 2006
on stochastic differentials, of the Mardia-Dryden distribution from
statistical shape theory.",
paper = "Kend01.pdf",
- keywords = "axiomref, CAS-Proof",
+ keywords = "axiomref, CAS-Proof, printed",
beebe = "Kendall:2001:SIC"
}
@@ -46438,7 +46681,7 @@ Kognitive Systeme, Universit\"t Karlsruhe 1992
user friendly and relatively weakly typed front end for the strongly
typed programming language.",
paper = "Suto87.pdf",
- keywords = "axiomref",
+ keywords = "axiomref, printed",
beebe = "Sutor:1987:TICb"
}
@@ -46730,7 +46973,8 @@ IBM Manual, March 1988
author = "Unknown",
title = {{Hindley-Milner Type Inference}},
link = "\url{https://www7.in.tum.de/um/courses/seminar/sove/SS2013/final/hindley-milner.slides.pdf}",
- paper = "Unkn13.pdf"
+ paper = "Unkn13.pdf",
+ keywords = "printed"
}
@@ -48913,7 +49157,7 @@ National Physical Laboratory. (1982)
year = "2012",
comment = "slides",
paper = "Avig12.pdf",
- keywords ="CAS-Proof"
+ keywords ="CAS-Proof, printed"
}
\end{chunk}
@@ -51549,6 +51793,43 @@ A.E.R.E. Report R.8730. HMSO. (1977)
\end{chunk}
+\index{Filliatre, Jean-Christophe}
+\begin{chunk}{axiom.bib}
+@article{Fill03,
+ author = "Filliatre, Jean-Christophe",
+ title = {{Verification of Non-Functional Programs using Interpretations
+ in Type Theory}},
+ journal = "J. Functional Programming",
+ volume = "13",
+ number = "4",
+ pages = "709-745",
+ year = "2003",
+ abstract =
+ "We study the problem of certifying programs combining imperative
+ and functional features within the general framework of type
+ theory.
+
+ Type theory is a powerful specification language, which is
+ naturally suited for the proof of purely functional programs. To
+ deal with imperative programs, we propose a logical interpretation
+ of an annotated program as a partial proof of its
+ specification. The construction of the corresponding partial proof
+ term is based on a static analysis of the effects of the program
+ which excludes aliases. The missing subterms in the partial proof
+ term are seen as proof obligations, whose actual proofs are left
+ to the user. We show that the validity of those proof obligations
+ implies the total correctness of the program.
+
+ This work has been implemented in the Coq proof assistant. It
+ appears as a tactic taking an annotated program as argument and
+ generating a set of proof obligations. Several nontrivial
+ algorithms have been certified using this tactic.",
+ paper = "Fill03.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\index{Fitch, John P.}
\begin{chunk}{axiom.bib}
@misc{Fitc74,
diff --git a/changelog b/changelog
index 100f4c9..d5fd824 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20180209 tpd src/axiom-website/patches.html 20180209.01.tpd.patch
+20180209 tpd books/bookvolbib add references
20180125 tpd src/axiom-website/patches.html 20180125.01.tpd.patch
20180125 tpd src/axiom-website/index.html updated per request
20180121 tpd src/axiom-website/patches.html 20180121.02.tpd.patch
diff --git a/patch b/patch
index 7af2f2f..e26b50f 100644
--- a/patch
+++ b/patch
@@ -1,3 +1,267 @@
-src/axiom-website/index.html updated per request
+books/bookvolbib add references
-Goal: Axiom Maintenance
+Goal: Proving Axiom Correct
+
+\index{Hickey, Rich}
+\begin{chunk}{axiom.bib}
+@misc{Hick18,
+ author = "Hickey, Rich",
+ title = {{Effective Programs - 10 Years of Clojure}},
+ link = "\url{https://www.youtube.com/watch?v=2V1FtfBDsLU}",
+ year = "2018"
+}
+
+\end{chunk}
+
+\index{Thiemann, Rene}
+\index{Yamada, Akihisa}
+\begin{chunk}{axiom.bib}
+@article{Thie17,
+ author = "Thiemann, Rene and Yamada, Akihisa",
+ title = {{Polynomial Factorization: Proof Outline}},
+ journal = "Archive of Formal Proofs",
+ year = "2017",
+ link = "\url{https://www.isa-afp.org/browser_info/current/AFP/Polynomial_Factorization/outline.pdf}",
+ abstract =
+ "Based on existing libraries for polynomial interpolation and
+ matrices, we formalized several factorization algorihms for
+ polynomials, including Kronecker's algorithm for intgeer polynomials,
+ Yun's square-free factorization algorithm for field polynomials, and a
+ factorization algorithm which delivers root-free polynomials.
+
+ As side products, we developed division algorithms for polynomials
+ over integral domains, as well as primality-testing and prime
+ factorization algorithms for integers.",
+ paper = "Thie17.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Thiemann, Rene}
+\index{Yamada, Akihisa}
+\begin{chunk}{axiom.bib}
+@article{Thie17a,
+ author = "Thiemann, Rene and Yamada, Akihisa",
+ title = {{Polynomial Factorization: Proof Document}},
+ journal = "Archive of Formal Proofs",
+ year = "2017",
+ link = "\url{https://www.isa-afp.org/browser_info/current/AFP/Polynomial_Factorization/document.pdf}",
+ abstract =
+ "Based on existing libraries for polynomial interpolation and
+ matrices, we formalized several factorization algorihms for
+ polynomials, including Kronecker's algorithm for intgeer polynomials,
+ Yun's square-free factorization algorithm for field polynomials, and a
+ factorization algorithm which delivers root-free polynomials.
+
+ As side products, we developed division algorithms for polynomials
+ over integral domains, as well as primality-testing and prime
+ factorization algorithms for integers.",
+ paper = "Thie17a.pdf"
+}
+
+\end{chunk}
+
+\begin{Crocker, David}
+\begin{chunk}{axiom.bib}
+@inproceedings{Croc14,
+ author = "Crocker, David",
+ title = {{Can C++ Be Made as Safe as SPARK?}},
+ booktitle = "Proc 2014 HILT",
+ isbn = "978-1-4503-3217-0",
+ year = "2014",
+ abstract =
+ "SPARK offers a way to develop formally-verified software in a
+ language (Ada) that is designed with safety in mind and is further
+ restricted by the SPARK language subset. However, much critical
+ embedded software is developed in C or C++ We look at whether and how
+ benefits similar to those offered by the SPARK language subset and
+ associated tools can be brought to a C++ development environment.",
+ paper = "Croc14.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Filliatre, Jean-Christophe}
+\begin{chunk}{axiom.bib}
+@article{Fill03,
+ author = "Filliatre, Jean-Christophe",
+ title = {{Verification of Non-Functional Programs using Interpretations
+ in Type Theory}},
+ journal = "J. Functional Programming",
+ volume = "13",
+ number = "4",
+ pages = "709-745",
+ year = "2003",
+ abstract =
+ "We study the problem of certifying programs combining imperative
+ and functional features within the general framework of type
+ theory.
+
+ Type theory is a powerful specification language, which is
+ naturally suited for the proof of purely functional programs. To
+ deal with imperative programs, we propose a logical interpretation
+ of an annotated program as a partial proof of its
+ specification. The construction of the corresponding partial proof
+ term is based on a static analysis of the effects of the program
+ which excludes aliases. The missing subterms in the partial proof
+ term are seen as proof obligations, whose actual proofs are left
+ to the user. We show that the validity of those proof obligations
+ implies the total correctness of the program.
+
+ This work has been implemented in the Coq proof assistant. It
+ appears as a tactic taking an annotated program as argument and
+ generating a set of proof obligations. Several nontrivial
+ algorithms have been certified using this tactic.",
+ paper = "Fill03.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Garret, Ron}
+\begin{chunk}{axiom.bib}
+@misc{Garr14,
+ author = "Garret, Ron",
+ title = {{The Awesome Power of Theory}},
+ link = "\url{http://www.flownet.com/ron/lambda-calculus.html}",
+ year = "2014"
+}
+
+\end{chunk}
+
+\index{Hoare, Charles Antony Richard}
+\begin{chunk}{axiom.bib}
+@article{Hoar71,
+ author = "Hoare, Charles Antony Richard",
+ title = {{Proof of a Program: FIND}},
+ journal = "Communications of the ACM",
+ volume = "14",
+ number = "1",
+ year = "1971",
+ abstract =
+ "A proof is given of the correctness of the algorithm 'Find.'
+ First, an informal description is given of the purpose of the
+ program and the method used. A systematic technique is described
+ for constructing the program proof during the process of coding
+ it, in such a way as to prevent the intrusion of logical
+ errors. The prrof of termination is treated as a separate
+ exercie. Finally, some conclusions related to general programming
+ methodology are drawn.",
+ paper = "Hoar71.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Filliatre, Jean-Christophe}
+\begin{chunk}{axiom.bib}
+@article{Fill07,
+ author = "Filliatre, Jean-Christophe",
+ title = {{Formal Proof of a Program: FIND}},
+ journal = "Science of Computer Programming",
+ volume = "64",
+ pages = "332-340",
+ year = "2007",
+ abstract =
+ "In 1971, C.A.R. Hoare gave the proof of correctness and
+ termination of a rather complex algorithm, in a paper entitled
+ {\sl Proof of a program: Find}. It is a handmade proof, where the
+ program is given together with its formal specification and where
+ each step is fully justified by mathematical reasoning. We present
+ here a formal proof of the same program in the system Coq, using
+ the recent tactic of the system developed to establish the total
+ correctness of imperative programs. We follow Hoare's paper as
+ closely as possible, keeping the same program and the same
+ specification. We show that we get exactly the same proof
+ obligations, which are proved in a straightforward way, following
+ the original paper. We also explain how more informal aspects of
+ Hoare's proof are formalized in the system Coq. This demonstrates
+ the adequacy of the system Coq in the process of certifying
+ imperative programs.",
+ paper = "Fill07.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Morris, F.L.}
+\index{Jones, C.B.}
+\begin{chunk}{axiom.bib}
+@article{Morr84,
+ author = "Morris, F.L. and Jones, C.B.",
+ title = {{An Early Program Proof by Alan Turing}},
+ journal = "Annals of the History of Computing",
+ volume = "6",
+ number = "2",
+ year = "1984",
+ pages = "139-143",
+ abstract =
+ "The paper reproduces, with typographical corrections and
+ comments, a 1949 paper by Alan Turing that foreshadoes much
+ subsequent work in program proving.",
+ paper = "Morr84.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Kovacs, Laura}
+\begin{chunk}{axiom.bib}
+@article{Kova16,
+ author = "Kovacs, Laura",
+ title = {{Symbolic Computation and Automated Reasoning for Program
+ Analysis}},
+ journal = "LNCS",
+ volume = "9681",
+ pages = "20-27",
+ year = "2016",
+ abstract =
+ "This talk describes how a combination of symbolic computation
+ techniques with first-order theorem proving can be used for solving
+ some challenges of automating program analysis, in particular for
+ generating and proving properties about the logically complex parts of
+ software. The talk will first present how computer algebra methods,
+ such as Gröbner basis computation, quantifier elimination and
+ algebraic recurrence solving, help us in inferring properties of
+ program loops with non-trivial arithmetic. Typical properties inferred
+ by our work are loop invariants and expressions bounding the number of
+ loop iterations. The talk will then describe our work to generate
+ first-order properties of programs with unbounded data structures,
+ such as arrays. For doing so, we use saturation-based first-order
+ theorem proving and extend first- order provers with support for
+ program analysis. Since program analysis requires reasoning in the
+ combination of first-order theories of data structures, the talk
+ also discusses new features in first-order theorem proving, such as
+ inductive reasoning and built-in boolean sort. These extensions allow
+ us to express program properties directly in first-order logic and
+ hence use further first-order theorem provers to reason about program
+ properties.",
+ paper = "Kova16.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Avigad, Jeremy}
+\begin{chunk}{axiom.bib}
+@misc{Avig17a,
+ author = "Avigad, Jeremy",
+ title = {{Proof Theory}},
+ year = "2017",
+ abstract =
+ "Proof theory began in the 1920's as part of Hilbert's program,
+ which aimed to secrure the foundations of mathematics by modeling
+ infinitary mathematics with formal axiomatic systems and proving
+ those systems consistent using restricted, finitary means. The
+ program thus viewed mathematics as a system of reasoning with
+ precise linguistic norms, govenered by rules that can be described
+ and studied in concrete terms. Today such a viewpoint has
+ applications in mathematics, computer science, and the philosophy
+ of mathematics.",
+ paper = "Avig17a.pdf",
+ keywords = "private communication"
+}
+
+\end{chunk}
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 795ac07..8182969 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5906,6 +5906,8 @@ books/bookvolbib add references

books/bookvol10.1 add SPDE chapter

20180125.01.tpd.patch
src/axiom-website/index.html updated per request

+20180209.01.tpd.patch
+books/bookvolbib add references

--
1.9.1