From 8df7e3471504435f81c0e716858439d8a2027e9a Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Fri, 9 Mar 2018 18:40:53 0500
Subject: [PATCH] books/bookvolbib add references
MIMEVersion: 1.0
ContentType: text/plain; charset=UTF8
ContentTransferEncoding: 8bit
Goal: Proving Axiom Correct
\index{Harper, Robert}
\begin{chunk}{axiom.bib}
@phdthesis{Harp85,
author = "Harper, Robert",
title = {{Aspects of the Implementation of Type Theory}},
school = "Cornell University",
year = "1985",
comment = "TR 85675",
abstract =
"This thesis is about building an automated programming logic. For our
purposes an automated programming logic consists of
\begin{itemize}
\item A formal system for reasoning about programs
\item A proof development environment which includes, at least, an
editor for the construction of proofs in the logic
\item Mechanized decision methods to assist in the proof development
process
\item A library mechanism for managing collections of theorems
\end{itemize}",
paper = "Harp85.pdf"
}
\end{chunk}
\index{Blanqui, Frederic}
\index{jouannaud, JeanPierre}
\index{Okada, Mitsuhiro}
\begin{chunk}{axiom.bib}
@inproceedings{Blan99,
author = "Blanqui, Frederic and jouannaud, JeanPierre and Okada, Mitsuhiro",
title = {{The Calculus of Algebraic Constructions}},
booktitle = "Rewriting Techniques and Applications RTA99",
year = "1999",
publisher = "LNCS 1631",
link = "\url{https://hal.inria.fr/inria00105545v1/document}",
abstract =
"This paper is concerned with the foundations of the Calculus of
Algebraic Constructions (CAC), an extension of the Calculus of
Constructions by inductive data types. CAC generalizes inductive
types equipped with higherorder primitive recursion, by providing
definition s of functions by patternmatching which capture recursor
definitions for arbitrary nondependent and nonpolymorphic inductive
types satisfying a strictly positivity condition. CAC also
generalizes the firstorder framework of abstract data types by
providing dependent types and higherorder rewrite rules.",
paper = "Blan99.pdf",
keywords = "printed"
}
\end{chunk}
\index{Blanqui, Frederic}
\begin{chunk}{axiom.bib}
@article{Blan05,
author = "Blanqui, Frederic",
title = {{Inductivev Types in the Calculus of Algebraic Constructions}},
journal = "Fundamenta Informaticae",
volume = "65",
number = "12",
pages = "6186",
year = "2005",
abstract =
"In a previous work, we proved that an important part of the Calculus
of Inductive Constructions (CIC), the basis of the Coq proof
assistant, can be seen as a Calculus of Algebraic Constructions
(CAC), an extension of the Calculus of Constructions with functions
and predicates defined by higherorder rewrite rules. In this
paper, we prove that almost all CIC can be seen as a CAC, and that it
can be further extended with nonstrictly positive types and
inductiverecursive types together with nonfree constructors and
patternmatching on defined symbols.",
paper = "Blan05.pdf"
}
\end{chunk}
\index{Floyd, Robert W.}
\begin{chunk}{axiom.bib}
@inproceedings{Floy67,
author = "Floyd, Robert W.",
title = {{Assigning Meanings to Programs}},
booktitle = "Proc. Symp. in Applied Mathematics",
year = "1967",
pages = "1932",
publisher = "American Mathematical Society",
paper = "Floy67.pdf",
keywords = "printed"
}
\end{chunk}
\index{Back, R.J.R}
\begin{chunk}{axiom.bib}
@article{Back81,
author = "Back, R.J.R",
title = {{On Correct Refinement of Programs}},
journal = "J. Computer and System Sciences",
volume = "23",
number = "1",
pages = "4968",
year = "1981",
abstract =
"The stepwise refinement technique is studied from a mathematical
point of view. A relation of correct refinement between programs is
defined, based on the principle that refinement steps should be
correctness preserving. Refinement between programs will therefore
depend on the criterion of program correctness used. The application
of the refinement relation in showing the soundness of different
techniques for refining programs is discussed. Special attention is
given to the use of abstraction in program construction. Refinement
with respect to partial and total correctness will be studied in more
detail, both for deterministic and nondeterministic programs. The
relationship between these refinement relations and the approximation
relation of fixpoint semantics will be studied, as well as the
connection with the predicate transformers used in program
verification.",
paper = "Back81.pdf",
keywords = "printed"
}
\end{chunk}
\index{Morgan, Carroll}
\begin{chunk}{axiom.bib}
@book{Morg98,
author = "Morgan, Carroll",
title = {{Programming from Specifcations, 2nd Ed.}},
publisher = "Prentice Hall",
year = "1998",
link =
"\url{http://www.cse.unsw.edu.au/~carrollm/ProgrammingFromSpecifications.pdf}",
paper = "Morg98.pdf"
}
\end{chunk}
\index{Filliatre, JeanChristophe}
\begin{chunk}{axiom.bib}
@phdthesis{Fill99,
author = "Filliatre, JeanChristophe",
title = {{Preuve de programmes imp\'eratifs en th\'eorie des types}},
school = {{Universit\'e ParisSud}},
year = "1999",
link = "\url{}",
paper = "Fill99.pdf"
}
\end{chunk}
\index{Caldwell, James L.}
\begin{chunk}{axiom.bib}
@inproceedings{Cald97,
author = "Caldwell, James L.",
title = {{Moving proofsasprograms into practice}},
booktitle = "Automated Software Engineering",
publisher = "IEEE",
year = "1997",
abstract =
"Proofs in the Nuprl system, an implementation of a constructive
type theory, yield “correctbyconstruction” pro grams. In this
paper a new methodology is presented for extracting efficient and
readable programs from inductive proofs. The resulting extracted
programs are in a form suitable for use in hierarchical
verifications in that they are amenable to clean partial evaluation
via extensions to the Nuprl rewrite system. The method is based on two
elements: specifications written with careful use of the Nuprl
settype to restrict the extracts to strictly computational content;
and on proofs that use induction tactics that generate extracts
using familiar fixedpoint combinators of the untyped lambda
calculus. In this paper the methodology is described and its
application is illustrated by example.",
paper = "Cald97.pdf",
keywords = "printed"
}
\end{chunk}
\index{Talpin, JeanPierre}
\index{Jouvelot, Pierre}
\begin{chunk}{axiom.bib}
@inproceedings{Talp92,
author = "Talpin, JeanPierre and Jouvelot, Pierre",
title = {{The Type and Effect Discipline}},
booktitle = "Conf. on Logic in Computer Science",
publisher = "Computer Science Press",
year = "1992",
abstract =
"The {\sl type and effect discipline} is a new framework for
reconstructing the principal type and the minimal effect of
expressions in implicitly typed polymorphic functional languages that
support imperative constructs. The type and effect discipline
outperforms other polymorphic type systems. Just as types abstract
collections of concrete values, {\sl effects} denote imperative
operations on regions. {\sl Regions} abstract sets of possibly aliased
memory locations.
Effects are used to control type generalization in the presence of
imperative constructs while regions delimit observable
sideeffects. The observable effects of an expression range over the
regions that are free in its type environment and its type; effects
related to local data structures can be discarded during type
reconstruction. The type of an expression can be generalized with
respect to the variables that are not free in the type environment or
in the observable effect.",
paper = "Talp92.pdf",
keywords = "printed"
}
\end{chunk}
\index{Davis, Jared Curran}
\begin{chunk}{axiom.bib}
@phdthesis{Davi09,
author = "Davis, Jared Curran",
title = {{A SelfVerifying Theorem Prover}},
school = "University of Texas at Austin",
year = "2009",
abstract =
"Programs have precise semantics, so we can use mathematical proof to
establish their properties. These proofs are often too large to
validate with the usual “social process” of mathematics, so instead we
create and check them with theoremproving software. This software
must be advanced enough to make the proof process tractable, but this
very sophistication casts doubt upon the whole enterprise: who
verifies the verifier?
We begin with a simple proof checker, Level 1, that only accepts
proofs composed of the most primitive steps, like Instantiation and
Cut. This program is so straightforward the ordinary, social process
can establish its soundness and the consistency of the logical
theory it implements (so we know theorems are “always true”).
Next, we develop a series of increasingly capable proof checkers,
Level 2, Level 3, etc. Each new proof checker accepts new kinds of
proof steps which were not accepted in the previous levels. By taking
advantage of these new proof steps, higherlevel proofs can be
written more concisely than lowerlevel proofs, and can take less time
to construct and check. Our highestlevel proof checker, Level 11, can
be thought of as a simplified version of the ACL2 or NQTHM theorem
provers. One contribution of this work is to show how such systems can
be verified.
To establish that the Level 11 proof checker can be trusted, we first
use it, without trusting it, to prove the fidelity of every Level n to
Level 1: whenever Level n accepts a proof of some $\phi$, there exists a
Level 1 proof of $\phi$. We then mechanically translate the Level 11 proof
for each Level n into a Level n − 1 proof—that is, we create a Level 1
proof of Level 2’s fidelity, a Level 2 proof of Level 3’s fidelity,
and so on. This layering shows that each level can be trusted, and
allows us to manage the sizes of these proofs.
In this way, our system proves its own fidelity, and trusting Level 11
only requires us to trust Level 1.",
paper = "Davi09.pdf"
}
\end{chunk}
\index{Myreen, Magnus O.}
\index{Davis, Jared}
\begin{chunk}{axiom.bib}
@article{Myre14,
author = "Myreen, Magnus O. and Davis, Jared",
title = {{The Reflective Milawa Theorem Prover is Sound}},
journal = "LNAI",
pages = "421436",
year = "2014",
abstract =
"Milawa is a theorem prover styled after ACL2 but with a small kernel
and a powerful reflection mechanism. We have used the HOL4 theorem
prover to formalize the logic of Milawa, prove the logic sound, and
prove that the source code for the Milawa kernel (2,000 lines of Lisp)
is faithful to the logic. Going further, we have combined these
results with our previous verification of an x86 machinecode
implementation of a Lisp runtime. Our toplevel HOL4 theorem states
that when Milawa is run on top of our verified Lisp, it will only
print theorem statements that are semantically true. We believe that
this toplevel theorem is the most comprehensive formal evidence of a
theorem prover’s soundness to date.".
paper = "Myre14.pdf",
keywords = "printed"
}
\end{chunk}
\index{Davis, Jared}
\index{Myreen, Magnus O.}
\begin{chunk}{axiom.bib}
@article{Davi15,
author = "Davis, Jared and Myreen, Magnus O.",
title = {{The Reflective Milawa Theorem Prover is Sound}},
journal = "J. Automated Reasoning",
volume = "55",
number = "2",
pages = "117183",
year = "2015",
abstract =
"This paper presents, we believe, the most comprehensive evidence of a
theorem prover’s soundness to date. Our subject is the Milawa theorem
prover. We present evidence of its soundness down to the machine
code. Milawa is a theorem prover styled after NQTHM and ACL2. It is
based on an idealised version of ACL2’s computational logic and
provides the user with highlevel tactics similar to ACL2’s. In
contrast to NQTHM and ACL2, Milawa has a small kernel that is somewhat
like an LCFstyle system. We explain how the Milawa theorem prover is
constructed as a sequence of reflective extensions from its
kernel. The kernel establishes the soundness of these extensions
during Milawa’s bootstrapping process. Going deeper, we explain how
we have shown that the Milawa kernel is sound using the HOL4 theorem
prover. In HOL4, we have formalized its logic, proved the logic sound,
and proved that the source code for the Milawa kernel (1,700 lines of
Lisp) faithfully implements this logic. Going even further, we have
combined these results with the x86 machinecode level verification of
the Lisp runtime Jitawa. Our toplevel theorem states that Milawa can
never claim to prove anything that is false when it is run on this
Lisp runtime.",
paper = "Davi15.pdf",
keywords = "printed"
}
\end{chunk}
\index{Myreen, Magnus O.}
\begin{chunk}{axiom.bib}
@article{Myre12,
author = "Myreen, Magnus O.",
title = {{Functional Programs: Conversions between Deep and Shallow
Embeddings}},
journal = "LNCS",
volume = "7406",
pages = "412417",
year = "2012",
abstract =
"This paper presents a method which simplifies verification of deeply
embedded functional programs. We present a technique by which
proofcertified equations describing the effect of functional
programs (shallow embeddings) can be automatically extracted from their
operational semantics. Our method can be used in reverse, i.e. from
shallow to deep embeddings, and thus for implementing certifying code
synthesis: we have implemented a tool which maps HOL functions to
equivalent Lisp functions, for which we have a verified Lisp runtime.
A key benefit, in both directions, is that the verifier does not need
to understand the operational semantics that gives meanings to the
deep embeddings.",
paper = "Myre12.pdf",
keywords = "printed"
}
\end{chunk}
\index{Myreen, Magnus O.}
\index{Davis, Jared}
\begin{chunk}{axiom.bib}
@article{Myre11,
author = "Myreen, Magnus O. and Davis, Jared",
title = {{A Verified Runtime for a Verified Theorem Prover}},
journal = "NCS",
volume = "6898",
pages = "265280",
year = "2011",
abstract =
"Theorem provers, such as ACL2, HOL, Isabelle and Coq, rely on the
correctness of runtime systems for programming languages like ML,
OCaml or Common Lisp. These runtime systems are complex and critical
to the integrity of the theorem provers.
In this paper, we present a new Lisp runtime which has been formally
verified and can run the Milawa theorem prover. Our runtime consists
of 7,500 lines of machine code and is able to complete a 4 gigabyte
Milawa proof effort. When our runtime is used to carry out Milawa
proofs, less unverified code must be trusted than with any other
theorem prover.
Our runtime includes a justintime compiler, a copying garbage collector,
a parser and a printer, all of which are HOL4verified down to
the concrete x86 code. We make heavy use of our previously developed
tools for machinecode verification. This work demonstrates that our
approach to machinecode verification scales to nontrivial
applications.",
paper = "Myre11.pdf",
keywords = "printed"
}
\end{chunk}

books/axiom.bib  415 +++++++++++++++++++++++++++++++
books/bookvolbib.pamphlet  495 +++++++++++++++++++++++++++++++++++++
changelog  2 +
patch  320 +++++++++++++++++++++++++
src/axiomwebsite/patches.html  2 +
5 files changed, 1152 insertions(+), 82 deletions()
diff git a/books/axiom.bib b/books/axiom.bib
index 2ab9298..7daa0a6 100644
 a/books/axiom.bib
+++ b/books/axiom.bib
@@ 7403,6 +7403,48 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@inproceedings{Blan99,
+ author = "Blanqui, Frederic and jouannaud, JeanPierre and Okada, Mitsuhiro",
+ title = {{The Calculus of Algebraic Constructions}},
+ booktitle = "Rewriting Techniques and Applications RTA99",
+ year = "1999",
+ publisher = "LNCS 1631",
+ link = "\url{https://hal.inria.fr/inria00105545v1/document}",
+ abstract =
+ "This paper is concerned with the foundations of the Calculus of
+ Algebraic Constructions (CAC), an extension of the Calculus of
+ Constructions by inductive data types. CAC generalizes inductive
+ types equipped with higherorder primitive recursion, by providing
+ definition s of functions by patternmatching which capture recursor
+ definitions for arbitrary nondependent and nonpolymorphic inductive
+ types satisfying a strictly positivity condition. CAC also
+ generalizes the firstorder framework of abstract data types by
+ providing dependent types and higherorder rewrite rules.",
+ paper = "Blan99.pdf",
+ keywords = "printed"
+}
+
+@article{Blan05,
+ author = "Blanqui, Frederic",
+ title = {{Inductivev Types in the Calculus of Algebraic Constructions}},
+ journal = "Fundamenta Informaticae",
+ volume = "65",
+ number = "12",
+ pages = "6186",
+ year = "2005",
+ abstract =
+ "In a previous work, we proved that an important part of the Calculus
+ of Inductive Constructions (CIC), the basis of the Coq proof
+ assistant, can be seen as a Calculus of Algebraic Constructions
+ (CAC), an extension of the Calculus of Constructions with functions
+ and predicates defined by higherorder rewrite rules. In this
+ paper, we prove that almost all CIC can be seen as a CAC, and that it
+ can be further extended with nonstrictly positive types and
+ inductiverecursive types together with nonfree constructors and
+ patternmatching on defined symbols.",
+ paper = "Blan05.pdf"
+}
+
@article{Bowe95,
author = "Bowen, Jonathan P. and Hinchey, Michael G.",
title = {{Seven More Myths of Formal Methods}},
@@ 7892,6 +7934,14 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@phdthesis{Fill99,
+ author = "Filliatre, JeanChristophe",
+ title = {{Preuve de programmes imp\'eratifs en th\'eorie des types}},
+ school = {{Universit\'e Paris Sud}},
+ year = "1999",
+ paper = "Fill99.pdf"
+}
+
@article{Fill07,
author = "Filliatre, JeanChristophe",
title = {{Formal Proof of a Program: FIND}},
@@ 7996,6 +8046,26 @@ paper = "Brea89.pdf"
keywords = "printed"
}
+@phdthesis{Harp85,
+ author = "Harper, Robert",
+ title = {{Aspects of the Implementation of Type Theory}},
+ school = "Cornell University",
+ year = "1985",
+ comment = "TR 85675",
+ abstract =
+ "This thesis is about building an automated programming logic. For our
+ purposes an automated programming logic consists of
+ \begin{itemize}
+ \item A formal system for reasoning about programs
+ \item A proof development environment which includes, at least, an
+ editor for the construction of proofs in the logic
+ \item Mechanized decision methods to assist in the proof development
+ process
+ \item A library mechanism for managing collections of theorems
+ \end{itemize}",
+ paper = "Harp85.pdf"
+}
+
@inproceedings{Harp94,
author = "Harper, Robert and Lillibridge, Mark",
title = {{A TypeTheoretic Approach to HigherOrder Modules with Sharing}},
@@ 8697,6 +8767,7 @@ paper = "Brea89.pdf"
title = {{Mosquito: An Aimplementation for HigherOrder Logic}},
school = "University of Cambridge",
year = "2013",
+ link = "\url{https://bitbucket.org/MosquitoProofAssistant/mosquito}",
abstract =
"We present Mosquito: an experimental stateless, pure, largely total
LCFstyle implementation of higherorder logic using Haskell as a
@@ 9045,6 +9116,317 @@ paper = "Brea89.pdf"
link = "\url{http://www.wolfram.com}"
}
+@article{Back81,
+ author = "Back, R.J.R",
+ title = {{On Correct Refinement of Programs}},
+ journal = "J. Computer and System Sciences",
+ volume = "23",
+ number = "1",
+ pages = "4968",
+ year = "1981",
+ abstract =
+ "The stepwise refinement technique is studied from a mathematical
+ point of view. A relation of correct refinement between programs is
+ defined, based on the principle that refinement steps should be
+ correctness preserving. Refinement between programs will therefore
+ depend on the criterion of program correctness used. The application
+ of the refinement relation in showing the soundness of different
+ techniques for refining programs is discussed. Special attention is
+ given to the use of abstraction in program construction. Refinement
+ with respect to partial and total correctness will be studied in more
+ detail, both for deterministic and nondeterministic programs. The
+ relationship between these refinement relations and the approximation
+ relation of fixpoint semantics will be studied, as well as the
+ connection with the predicate transformers used in program
+ verification.",
+ paper = "Back81.pdf",
+ keywords = "printed"
+}
+
+@inproceedings{Cald97,
+ author = "Caldwell, James L.",
+ title = {{Moving proofsasprograms into practice}},
+ booktitle = "Automated Software Engineering",
+ publisher = "IEEE",
+ year = "1997",
+ abstract =
+ "Proofs in the Nuprl system, an implementation of a constructive
+ type theory, yield “correctbyconstruction” pro grams. In this
+ paper a new methodology is presented for extracting efficient and
+ readable programs from inductive proofs. The resulting extracted
+ programs are in a form suitable for use in hierarchical
+ verifications in that they are amenable to clean partial evaluation
+ via extensions to the Nuprl rewrite system. The method is based on two
+ elements: specifications written with careful use of the Nuprl
+ settype to restrict the extracts to strictly computational content;
+ and on proofs that use induction tactics that generate extracts
+ using familiar fixedpoint combinators of the untyped lambda
+ calculus. In this paper the methodology is described and its
+ application is illustrated by example.",
+ paper = "Cald97.pdf",
+ keywords = "printed"
+}
+
+@phdthesis{Davi09,
+ author = "Davis, Jared Curran",
+ title = {{A SelfVerifying Theorem Prover}},
+ school = "University of Texas at Austin",
+ year = "2009",
+ abstract =
+ "Programs have precise semantics, so we can use mathematical proof to
+ establish their properties. These proofs are often too large to
+ validate with the usual “social process” of mathematics, so instead we
+ create and check them with theoremproving software. This software
+ must be advanced enough to make the proof process tractable, but this
+ very sophistication casts doubt upon the whole enterprise: who
+ verifies the verifier?
+
+ We begin with a simple proof checker, Level 1, that only accepts
+ proofs composed of the most primitive steps, like Instantiation and
+ Cut. This program is so straightforward the ordinary, social process
+ can establish its soundness and the consistency of the logical
+ theory it implements (so we know theorems are “always true”).
+
+ Next, we develop a series of increasingly capable proof checkers,
+ Level 2, Level 3, etc. Each new proof checker accepts new kinds of
+ proof steps which were not accepted in the previous levels. By taking
+ advantage of these new proof steps, higherlevel proofs can be
+ written more concisely than lowerlevel proofs, and can take less time
+ to construct and check. Our highestlevel proof checker, Level 11, can
+ be thought of as a simplified version of the ACL2 or NQTHM theorem
+ provers. One contribution of this work is to show how such systems can
+ be verified.
+
+ To establish that the Level 11 proof checker can be trusted, we first
+ use it, without trusting it, to prove the fidelity of every Level n to
+ Level 1: whenever Level n accepts a proof of some $\phi$, there exists a
+ Level 1 proof of $\phi$. We then mechanically translate the Level 11 proof
+ for each Level n into a Level n − 1 proof—that is, we create a Level 1
+ proof of Level 2’s fidelity, a Level 2 proof of Level 3’s fidelity,
+ and so on. This layering shows that each level can be trusted, and
+ allows us to manage the sizes of these proofs.
+
+ In this way, our system proves its own fidelity, and trusting Level 11
+ only requires us to trust Level 1.",
+ paper = "Davi09.pdf"
+}
+
+@article{Davi15,
+ author = "Davis, Jared and Myreen, Magnus O.",
+ title = {{The Reflective Milawa Theorem Prover is Sound}},
+ journal = "J. Automated Reasoning",
+ volume = "55",
+ number = "2",
+ pages = "117183",
+ year = "2015",
+ abstract =
+ "This paper presents, we believe, the most comprehensive evidence of a
+ theorem prover’s soundness to date. Our subject is the Milawa theorem
+ prover. We present evidence of its soundness down to the machine
+ code. Milawa is a theorem prover styled after NQTHM and ACL2. It is
+ based on an idealised version of ACL2’s computational logic and
+ provides the user with highlevel tactics similar to ACL2’s. In
+ contrast to NQTHM and ACL2, Milawa has a small kernel that is somewhat
+ like an LCFstyle system. We explain how the Milawa theorem prover is
+ constructed as a sequence of reflective extensions from its
+ kernel. The kernel establishes the soundness of these extensions
+ during Milawa’s bootstrapping process. Going deeper, we explain how
+ we have shown that the Milawa kernel is sound using the HOL4 theorem
+ prover. In HOL4, we have formalized its logic, proved the logic sound,
+ and proved that the source code for the Milawa kernel (1,700 lines of
+ Lisp) faithfully implements this logic. Going even further, we have
+ combined these results with the x86 machinecode level verification of
+ the Lisp runtime Jitawa. Our toplevel theorem states that Milawa can
+ never claim to prove anything that is false when it is run on this
+ Lisp runtime.",
+ paper = "Davi15.pdf",
+ keywords = "printed"
+}
+
+@article{Fill03,
+ author = "Filliatre, JeanChristophe",
+ title = {{Verification of NonFunctional Programs using Interpretations
+ in Type Theory}},
+ journal = "J. Functional Programming",
+ volume = "13",
+ number = "4",
+ pages = "709745",
+ 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"
+}
+
+@article{Fill13,
+ author = "Filliatre, JeanChristophe and Paskevich, Andrei",
+ title = {{Why3  Where Programs Meet Provers}},
+ journal = "LNCS",
+ volume = "7792",
+ year = "2013",
+ link = "\url{https://hal.inria.fr/hal00789533/document}",
+ abstract =
+ "We present Why3, a tool for deductive program verification, and
+ WhyML, its programming and specification language. WhyML is a
+ firstorder language with polymorphic types, pattern matching, and
+ inductive predicates. Programs can make use of record types with
+ mutable fields, type invariants, and ghost code. Verification
+ conditions are discharged by Why3 with the help of various existing
+ automated and interactive theorem provers. To keep verification
+ conditions tractable and comprehensible, WhyML imposes a static
+ control of aliases that obviates the use of a memory model. A user
+ can write WhyML programs directly and get correctbyconstruction
+ OCaml programs via an automated extraction mechanism. WhyML is also
+ used as an intermediate language for the verification of C, Java, or
+ Ada programs. We demonstrate the benefits of Why3 and WhyML on
+ nontrivial examples of program verification.",
+ paper = "Fill13.pdf",
+ keywords = "printed"
+}
+
+@inproceedings{Floy67,
+ author = "Floyd, Robert W.",
+ title = {{Assigning Meanings to Programs}},
+ booktitle = "Proc. Symp. in Applied Mathematics",
+ year = "1967",
+ pages = "1932",
+ publisher = "American Mathematical Society",
+ paper = "Floy67.pdf",
+ keywords = "printed"
+}
+
+@article{Myre12,
+ author = "Myreen, Magnus O.",
+ title = {{Functional Programs: Conversions between Deep and Shallow
+ Embeddings}},
+ journal = "LNCS",
+ volume = "7406",
+ pages = "412417",
+ year = "2012",
+ abstract =
+ "This paper presents a method which simplifies verification of deeply
+ embedded functional programs. We present a technique by which
+ proofcertified equations describing the effect of functional
+ programs (shallow embeddings) can be automatically extracted from their
+ operational semantics. Our method can be used in reverse, i.e. from
+ shallow to deep embeddings, and thus for implementing certifying code
+ synthesis: we have implemented a tool which maps HOL functions to
+ equivalent Lisp functions, for which we have a verified Lisp runtime.
+ A key benefit, in both directions, is that the verifier does not need
+ to understand the operational semantics that gives meanings to the
+ deep embeddings.",
+ paper = "Myre12.pdf",
+ keywords = "printed"
+}
+
+@article{Myre11,
+ author = "Myreen, Magnus O. and Davis, Jared",
+ title = {{A Verified Runtime for a Verified Theorem Prover}},
+ journal = "NCS",
+ volume = "6898",
+ pages = "265280",
+ year = "2011",
+ abstract =
+ "Theorem provers, such as ACL2, HOL, Isabelle and Coq, rely on the
+ correctness of runtime systems for programming languages like ML,
+ OCaml or Common Lisp. These runtime systems are complex and critical
+ to the integrity of the theorem provers.
+
+ In this paper, we present a new Lisp runtime which has been formally
+ verified and can run the Milawa theorem prover. Our runtime consists
+ of 7,500 lines of machine code and is able to complete a 4 gigabyte
+ Milawa proof effort. When our runtime is used to carry out Milawa
+ proofs, less unverified code must be trusted than with any other
+ theorem prover.
+
+ Our runtime includes a justintime compiler, a copying garbage collector,
+ a parser and a printer, all of which are HOL4verified down to
+ the concrete x86 code. We make heavy use of our previously developed
+ tools for machinecode verification. This work demonstrates that our
+ approach to machinecode verification scales to nontrivial
+ applications.",
+ paper = "Myre11.pdf",
+ keywords = "printed"
+}
+
+@article{Myre14,
+ author = "Myreen, Magnus O. and Davis, Jared",
+ title = {{The Reflective Milawa Theorem Prover is Sound}},
+ journal = "LNAI",
+ pages = "421436",
+ year = "2014",
+ abstract =
+ "Milawa is a theorem prover styled after ACL2 but with a small kernel
+ and a powerful reflection mechanism. We have used the HOL4 theorem
+ prover to formalize the logic of Milawa, prove the logic sound, and
+ prove that the source code for the Milawa kernel (2,000 lines of Lisp)
+ is faithful to the logic. Going further, we have combined these
+ results with our previous verification of an x86 machinecode
+ implementation of a Lisp runtime. Our toplevel HOL4 theorem states
+ that when Milawa is run on top of our verified Lisp, it will only
+ print theorem statements that are semantically true. We believe that
+ this toplevel theorem is the most comprehensive formal evidence of a
+ theorem prover’s soundness to date.",
+ paper = "Myre14.pdf",
+ keywords = "printed"
+}
+
+@book{Morg98,
+ author = "Morgan, Carroll",
+ title = {{Programming from Specifcations, 2nd Ed.}},
+ publisher = "Prentice Hall",
+ year = "1998",
+ link =
+"\url{http://www.cse.unsw.edu.au/~carrollm/ProgrammingFromSpecifications.pdf}",
+ paper = "Morg98.pdf"
+}
+
+@inproceedings{Talp92,
+ author = "Talpin, JeanPierre and Jouvelot, Pierre",
+ title = {{The Type and Effect Discipline}},
+ booktitle = "Conf. on Logic in Computer Science",
+ publisher = "Computer Science Press",
+ year = "1992",
+ abstract =
+ "The {\sl type and effect discipline} is a new framework for
+ reconstructing the principal type and the minimal effect of
+ expressions in implicitly typed polymorphic functional languages that
+ support imperative constructs. The type and effect discipline
+ outperforms other polymorphic type systems. Just as types abstract
+ collections of concrete values, {\sl effects} denote imperative
+ operations on regions. {\sl Regions} abstract sets of possibly aliased
+ memory locations.
+
+ Effects are used to control type generalization in the presence of
+ imperative constructs while regions delimit observable
+ sideeffects. The observable effects of an expression range over the
+ regions that are free in its type environment and its type; effects
+ related to local data structures can be discarded during type
+ reconstruction. The type of an expression can be generalized with
+ respect to the variables that are not free in the type environment or
+ in the observable effect.",
+ paper = "Talp92.pdf",
+ keywords = "printed"
+}
+
@incollection{Soze06,
author = "Sozeau, Matthieu",
title = {{Subset Coercions in Coq}},
@@ 35985,39 +36367,6 @@ paper = "Brea89.pdf"
keywords = "printed"
}
@article{Fill03,
 author = "Filliatre, JeanChristophe",
 title = {{Verification of NonFunctional Programs using Interpretations
 in Type Theory}},
 journal = "J. Functional Programming",
 volume = "13",
 number = "4",
 pages = "709745",
 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 2785180..683d337 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 10024,6 +10024,58 @@ when shown in factored form.
\end{chunk}
+\index{Blanqui, Frederic}
+\index{jouannaud, JeanPierre}
+\index{Okada, Mitsuhiro}
+\begin{chunk}{axiom.bib}
+@inproceedings{Blan99,
+ author = "Blanqui, Frederic and jouannaud, JeanPierre and Okada, Mitsuhiro",
+ title = {{The Calculus of Algebraic Constructions}},
+ booktitle = "Rewriting Techniques and Applications RTA99",
+ year = "1999",
+ publisher = "LNCS 1631",
+ link = "\url{https://hal.inria.fr/inria00105545v1/document}",
+ abstract =
+ "This paper is concerned with the foundations of the Calculus of
+ Algebraic Constructions (CAC), an extension of the Calculus of
+ Constructions by inductive data types. CAC generalizes inductive
+ types equipped with higherorder primitive recursion, by providing
+ definition s of functions by patternmatching which capture recursor
+ definitions for arbitrary nondependent and nonpolymorphic inductive
+ types satisfying a strictly positivity condition. CAC also
+ generalizes the firstorder framework of abstract data types by
+ providing dependent types and higherorder rewrite rules.",
+ paper = "Blan99.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Blanqui, Frederic}
+\begin{chunk}{axiom.bib}
+@article{Blan05,
+ author = "Blanqui, Frederic",
+ title = {{Inductivev Types in the Calculus of Algebraic Constructions}},
+ journal = "Fundamenta Informaticae",
+ volume = "65",
+ number = "12",
+ pages = "6186",
+ year = "2005",
+ abstract =
+ "In a previous work, we proved that an important part of the Calculus
+ of Inductive Constructions (CIC), the basis of the Coq proof
+ assistant, can be seen as a Calculus of Algebraic Constructions
+ (CAC), an extension of the Calculus of Constructions with functions
+ and predicates defined by higherorder rewrite rules. In this
+ paper, we prove that almost all CIC can be seen as a CAC, and that it
+ can be further extended with nonstrictly positive types and
+ inductiverecursive types together with nonfree constructors and
+ patternmatching on defined symbols.",
+ paper = "Blan05.pdf"
+}
+
+\end{chunk}
+
\index{Bowen, Jonathan P.}
\index{Hinchey, Michael G.}
\begin{chunk}{axiom.bib}
@@ 10607,6 +10659,18 @@ when shown in factored form.
\index{Filliatre, JeanChristophe}
\begin{chunk}{axiom.bib}
+@phdthesis{Fill99,
+ author = "Filliatre, JeanChristophe",
+ title = {{Preuve de programmes imp\'eratifs en th\'eorie des types}},
+ school = {{Universit\'e Paris Sud}},
+ year = "1999",
+ paper = "Fill99.pdf"
+}
+
+\end{chunk}
+
+\index{Filliatre, JeanChristophe}
+\begin{chunk}{axiom.bib}
@article{Fill07,
author = "Filliatre, JeanChristophe",
title = {{Formal Proof of a Program: FIND}},
@@ 10742,6 +10806,30 @@ when shown in factored form.
\end{chunk}
\index{Harper, Robert}
+\begin{chunk}{axiom.bib}
+@phdthesis{Harp85,
+ author = "Harper, Robert",
+ title = {{Aspects of the Implementation of Type Theory}},
+ school = "Cornell University",
+ year = "1985",
+ comment = "TR 85675",
+ abstract =
+ "This thesis is about building an automated programming logic. For our
+ purposes an automated programming logic consists of
+ \begin{itemize}
+ \item A formal system for reasoning about programs
+ \item A proof development environment which includes, at least, an
+ editor for the construction of proofs in the logic
+ \item Mechanized decision methods to assist in the proof development
+ process
+ \item A library mechanism for managing collections of theorems
+ \end{itemize}",
+ paper = "Harp85.pdf"
+}
+
+\end{chunk}
+
+\index{Harper, Robert}
\index{Lillibridge, Mark}
\begin{chunk}{axiom.bib}
@inproceedings{Harp94,
@@ 11592,6 +11680,7 @@ when shown in factored form.
title = {{Mosquito: An Aimplementation for HigherOrder Logic}},
school = "University of Cambridge",
year = "2013",
+ link = "\url{https://bitbucket.org/MosquitoProofAssistant/mosquito}",
abstract =
"We present Mosquito: an experimental stateless, pure, largely total
LCFstyle implementation of higherorder logic using Haskell as a
@@ 12031,6 +12120,373 @@ when shown in factored form.
\end{chunk}
+\section{Proving Axiom Correct  Spring 2018}
+
+\index{Back, R.J.R}
+\begin{chunk}{axiom.bib}
+@article{Back81,
+ author = "Back, R.J.R",
+ title = {{On Correct Refinement of Programs}},
+ journal = "J. Computer and System Sciences",
+ volume = "23",
+ number = "1",
+ pages = "4968",
+ year = "1981",
+ abstract =
+ "The stepwise refinement technique is studied from a mathematical
+ point of view. A relation of correct refinement between programs is
+ defined, based on the principle that refinement steps should be
+ correctness preserving. Refinement between programs will therefore
+ depend on the criterion of program correctness used. The application
+ of the refinement relation in showing the soundness of different
+ techniques for refining programs is discussed. Special attention is
+ given to the use of abstraction in program construction. Refinement
+ with respect to partial and total correctness will be studied in more
+ detail, both for deterministic and nondeterministic programs. The
+ relationship between these refinement relations and the approximation
+ relation of fixpoint semantics will be studied, as well as the
+ connection with the predicate transformers used in program
+ verification.",
+ paper = "Back81.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Caldwell, James L.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Cald97,
+ author = "Caldwell, James L.",
+ title = {{Moving proofsasprograms into practice}},
+ booktitle = "Automated Software Engineering",
+ publisher = "IEEE",
+ year = "1997",
+ abstract =
+ "Proofs in the Nuprl system, an implementation of a constructive
+ type theory, yield “correctbyconstruction” pro grams. In this
+ paper a new methodology is presented for extracting efficient and
+ readable programs from inductive proofs. The resulting extracted
+ programs are in a form suitable for use in hierarchical
+ verifications in that they are amenable to clean partial evaluation
+ via extensions to the Nuprl rewrite system. The method is based on two
+ elements: specifications written with careful use of the Nuprl
+ settype to restrict the extracts to strictly computational content;
+ and on proofs that use induction tactics that generate extracts
+ using familiar fixedpoint combinators of the untyped lambda
+ calculus. In this paper the methodology is described and its
+ application is illustrated by example.",
+ paper = "Cald97.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Davis, Jared Curran}
+\begin{chunk}{axiom.bib}
+@phdthesis{Davi09,
+ author = "Davis, Jared Curran",
+ title = {{A SelfVerifying Theorem Prover}},
+ school = "University of Texas at Austin",
+ year = "2009",
+ abstract =
+ "Programs have precise semantics, so we can use mathematical proof to
+ establish their properties. These proofs are often too large to
+ validate with the usual “social process” of mathematics, so instead we
+ create and check them with theoremproving software. This software
+ must be advanced enough to make the proof process tractable, but this
+ very sophistication casts doubt upon the whole enterprise: who
+ verifies the verifier?
+
+ We begin with a simple proof checker, Level 1, that only accepts
+ proofs composed of the most primitive steps, like Instantiation and
+ Cut. This program is so straightforward the ordinary, social process
+ can establish its soundness and the consistency of the logical
+ theory it implements (so we know theorems are “always true”).
+
+ Next, we develop a series of increasingly capable proof checkers,
+ Level 2, Level 3, etc. Each new proof checker accepts new kinds of
+ proof steps which were not accepted in the previous levels. By taking
+ advantage of these new proof steps, higherlevel proofs can be
+ written more concisely than lowerlevel proofs, and can take less time
+ to construct and check. Our highestlevel proof checker, Level 11, can
+ be thought of as a simplified version of the ACL2 or NQTHM theorem
+ provers. One contribution of this work is to show how such systems can
+ be verified.
+
+ To establish that the Level 11 proof checker can be trusted, we first
+ use it, without trusting it, to prove the fidelity of every Level n to
+ Level 1: whenever Level n accepts a proof of some $\phi$, there exists a
+ Level 1 proof of $\phi$. We then mechanically translate the Level 11 proof
+ for each Level n into a Level n − 1 proof—that is, we create a Level 1
+ proof of Level 2’s fidelity, a Level 2 proof of Level 3’s fidelity,
+ and so on. This layering shows that each level can be trusted, and
+ allows us to manage the sizes of these proofs.
+
+ In this way, our system proves its own fidelity, and trusting Level 11
+ only requires us to trust Level 1.",
+ paper = "Davi09.pdf"
+}
+
+\end{chunk}
+
+\index{Davis, Jared}
+\index{Myreen, Magnus O.}
+\begin{chunk}{axiom.bib}
+@article{Davi15,
+ author = "Davis, Jared and Myreen, Magnus O.",
+ title = {{The Reflective Milawa Theorem Prover is Sound}},
+ journal = "J. Automated Reasoning",
+ volume = "55",
+ number = "2",
+ pages = "117183",
+ year = "2015",
+ abstract =
+ "This paper presents, we believe, the most comprehensive evidence of a
+ theorem prover’s soundness to date. Our subject is the Milawa theorem
+ prover. We present evidence of its soundness down to the machine
+ code. Milawa is a theorem prover styled after NQTHM and ACL2. It is
+ based on an idealised version of ACL2’s computational logic and
+ provides the user with highlevel tactics similar to ACL2’s. In
+ contrast to NQTHM and ACL2, Milawa has a small kernel that is somewhat
+ like an LCFstyle system. We explain how the Milawa theorem prover is
+ constructed as a sequence of reflective extensions from its
+ kernel. The kernel establishes the soundness of these extensions
+ during Milawa’s bootstrapping process. Going deeper, we explain how
+ we have shown that the Milawa kernel is sound using the HOL4 theorem
+ prover. In HOL4, we have formalized its logic, proved the logic sound,
+ and proved that the source code for the Milawa kernel (1,700 lines of
+ Lisp) faithfully implements this logic. Going even further, we have
+ combined these results with the x86 machinecode level verification of
+ the Lisp runtime Jitawa. Our toplevel theorem states that Milawa can
+ never claim to prove anything that is false when it is run on this
+ Lisp runtime.",
+ paper = "Davi15.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Filliatre, JeanChristophe}
+\begin{chunk}{axiom.bib}
+@article{Fill03,
+ author = "Filliatre, JeanChristophe",
+ title = {{Verification of NonFunctional Programs using Interpretations
+ in Type Theory}},
+ journal = "J. Functional Programming",
+ volume = "13",
+ number = "4",
+ pages = "709745",
+ 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{Filliatre, JeanChristophe}
+\index{Paskevich, Andrei}
+\begin{chunk}{axiom.bib}
+@article{Fill13,
+ author = "Filliatre, JeanChristophe and Paskevich, Andrei",
+ title = {{Why3  Where Programs Meet Provers}},
+ journal = "LNCS",
+ volume = "7792",
+ year = "2013",
+ link = "\url{https://hal.inria.fr/hal00789533/document}",
+ abstract =
+ "We present Why3, a tool for deductive program verification, and
+ WhyML, its programming and specification language. WhyML is a
+ firstorder language with polymorphic types, pattern matching, and
+ inductive predicates. Programs can make use of record types with
+ mutable fields, type invariants, and ghost code. Verification
+ conditions are discharged by Why3 with the help of various existing
+ automated and interactive theorem provers. To keep verification
+ conditions tractable and comprehensible, WhyML imposes a static
+ control of aliases that obviates the use of a memory model. A user
+ can write WhyML programs directly and get correctbyconstruction
+ OCaml programs via an automated extraction mechanism. WhyML is also
+ used as an intermediate language for the verification of C, Java, or
+ Ada programs. We demonstrate the benefits of Why3 and WhyML on
+ nontrivial examples of program verification.",
+ paper = "Fill13.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Floyd, Robert W.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Floy67,
+ author = "Floyd, Robert W.",
+ title = {{Assigning Meanings to Programs}},
+ booktitle = "Proc. Symp. in Applied Mathematics",
+ year = "1967",
+ pages = "1932",
+ publisher = "American Mathematical Society",
+ paper = "Floy67.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Myreen, Magnus O.}
+\begin{chunk}{axiom.bib}
+@article{Myre12,
+ author = "Myreen, Magnus O.",
+ title = {{Functional Programs: Conversions between Deep and Shallow
+ Embeddings}},
+ journal = "LNCS",
+ volume = "7406",
+ pages = "412417",
+ year = "2012",
+ abstract =
+ "This paper presents a method which simplifies verification of deeply
+ embedded functional programs. We present a technique by which
+ proofcertified equations describing the effect of functional
+ programs (shallow embeddings) can be automatically extracted from their
+ operational semantics. Our method can be used in reverse, i.e. from
+ shallow to deep embeddings, and thus for implementing certifying code
+ synthesis: we have implemented a tool which maps HOL functions to
+ equivalent Lisp functions, for which we have a verified Lisp runtime.
+ A key benefit, in both directions, is that the verifier does not need
+ to understand the operational semantics that gives meanings to the
+ deep embeddings.",
+ paper = "Myre12.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Myreen, Magnus O.}
+\index{Davis, Jared}
+\begin{chunk}{axiom.bib}
+@article{Myre11,
+ author = "Myreen, Magnus O. and Davis, Jared",
+ title = {{A Verified Runtime for a Verified Theorem Prover}},
+ journal = "NCS",
+ volume = "6898",
+ pages = "265280",
+ year = "2011",
+ abstract =
+ "Theorem provers, such as ACL2, HOL, Isabelle and Coq, rely on the
+ correctness of runtime systems for programming languages like ML,
+ OCaml or Common Lisp. These runtime systems are complex and critical
+ to the integrity of the theorem provers.
+
+ In this paper, we present a new Lisp runtime which has been formally
+ verified and can run the Milawa theorem prover. Our runtime consists
+ of 7,500 lines of machine code and is able to complete a 4 gigabyte
+ Milawa proof effort. When our runtime is used to carry out Milawa
+ proofs, less unverified code must be trusted than with any other
+ theorem prover.
+
+ Our runtime includes a justintime compiler, a copying garbage collector,
+ a parser and a printer, all of which are HOL4verified down to
+ the concrete x86 code. We make heavy use of our previously developed
+ tools for machinecode verification. This work demonstrates that our
+ approach to machinecode verification scales to nontrivial
+ applications.",
+ paper = "Myre11.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+
+\index{Myreen, Magnus O.}
+\index{Davis, Jared}
+\begin{chunk}{axiom.bib}
+@article{Myre14,
+ author = "Myreen, Magnus O. and Davis, Jared",
+ title = {{The Reflective Milawa Theorem Prover is Sound}},
+ journal = "LNAI",
+ pages = "421436",
+ year = "2014",
+ abstract =
+ "Milawa is a theorem prover styled after ACL2 but with a small kernel
+ and a powerful reflection mechanism. We have used the HOL4 theorem
+ prover to formalize the logic of Milawa, prove the logic sound, and
+ prove that the source code for the Milawa kernel (2,000 lines of Lisp)
+ is faithful to the logic. Going further, we have combined these
+ results with our previous verification of an x86 machinecode
+ implementation of a Lisp runtime. Our toplevel HOL4 theorem states
+ that when Milawa is run on top of our verified Lisp, it will only
+ print theorem statements that are semantically true. We believe that
+ this toplevel theorem is the most comprehensive formal evidence of a
+ theorem prover’s soundness to date.",
+ paper = "Myre14.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Morgan, Carroll}
+\begin{chunk}{axiom.bib}
+@book{Morg98,
+ author = "Morgan, Carroll",
+ title = {{Programming from Specifcations, 2nd Ed.}},
+ publisher = "Prentice Hall",
+ year = "1998",
+ link =
+"\url{http://www.cse.unsw.edu.au/~carrollm/ProgrammingFromSpecifications.pdf}",
+ paper = "Morg98.pdf"
+}
+
+\end{chunk}
+
+\index{Talpin, JeanPierre}
+\index{Jouvelot, Pierre}
+\begin{chunk}{axiom.bib}
+@inproceedings{Talp92,
+ author = "Talpin, JeanPierre and Jouvelot, Pierre",
+ title = {{The Type and Effect Discipline}},
+ booktitle = "Conf. on Logic in Computer Science",
+ publisher = "Computer Science Press",
+ year = "1992",
+ abstract =
+ "The {\sl type and effect discipline} is a new framework for
+ reconstructing the principal type and the minimal effect of
+ expressions in implicitly typed polymorphic functional languages that
+ support imperative constructs. The type and effect discipline
+ outperforms other polymorphic type systems. Just as types abstract
+ collections of concrete values, {\sl effects} denote imperative
+ operations on regions. {\sl Regions} abstract sets of possibly aliased
+ memory locations.
+
+ Effects are used to control type generalization in the presence of
+ imperative constructs while regions delimit observable
+ sideeffects. The observable effects of an expression range over the
+ regions that are free in its type environment and its type; effects
+ related to local data structures can be discarded during type
+ reconstruction. The type of an expression can be generalized with
+ respect to the variables that are not free in the type environment or
+ in the observable effect.",
+ paper = "Talp92.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
\section{Proving Axiom Correct  Coercion in CASProof Systesms} %
\index{Sozeau, Matthieu}
@@ 12069,7 +12525,7 @@ when shown in factored form.
\end{chunk}
\section{Proving SAxiom Correct  CASProof System Survey} %%%%%%%%
+\section{Proving Axiom Correct  CASProof System Survey} %%%%%%%%
\subsection{A} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ 52570,43 +53026,6 @@ A.E.R.E. Report R.8730. HMSO. (1977)
\end{chunk}
\index{Filliatre, JeanChristophe}
\begin{chunk}{axiom.bib}
@article{Fill03,
 author = "Filliatre, JeanChristophe",
 title = {{Verification of NonFunctional Programs using Interpretations
 in Type Theory}},
 journal = "J. Functional Programming",
 volume = "13",
 number = "4",
 pages = "709745",
 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 439a0c1..0414540 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20180309 tpd src/axiomwebsite/patches.html 20180309.01.tpd.patch
+20180309 tpd books/bookvolbib add references
20180304 tpd src/axiomwebsite/patches.html 20180304.01.tpd.patch
20180304 tpd proposal
20180227 tpd src/axiomwebsite/patches.html 20180227.03.tpd.patch
diff git a/patch b/patch
index d413c96..7e31a35 100644
 a/patch
+++ b/patch
@@ 26,17 +26,6 @@ Goal: Proving Axiom Correct
\end{chunk}
\index{Filliatre, JeanChristophe}
\begin{chunk}{axiom.bib}
@phdthesis{Fill99,
 author = "Filliatre, JeanChristophe",
 title = {{Preuve de programmes imp\'eratifs en th\'eorie des types}},
 school = {{Universit\'e Paris Sud}},
 year = "1999"
}

\end{chunk}

\index{Blanqui, Frederic}
\index{jouannaud, JeanPierre}
\index{Okada, Mitsuhiro}
@@ 88,3 +77,312 @@ Goal: Proving Axiom Correct
}
\end{chunk}
+
+\index{Floyd, Robert W.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Floy67,
+ author = "Floyd, Robert W.",
+ title = {{Assigning Meanings to Programs}},
+ booktitle = "Proc. Symp. in Applied Mathematics",
+ year = "1967",
+ pages = "1932",
+ publisher = "American Mathematical Society",
+ paper = "Floy67.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Back, R.J.R}
+\begin{chunk}{axiom.bib}
+@article{Back81,
+ author = "Back, R.J.R",
+ title = {{On Correct Refinement of Programs}},
+ journal = "J. Computer and System Sciences",
+ volume = "23",
+ number = "1",
+ pages = "4968",
+ year = "1981",
+ abstract =
+ "The stepwise refinement technique is studied from a mathematical
+ point of view. A relation of correct refinement between programs is
+ defined, based on the principle that refinement steps should be
+ correctness preserving. Refinement between programs will therefore
+ depend on the criterion of program correctness used. The application
+ of the refinement relation in showing the soundness of different
+ techniques for refining programs is discussed. Special attention is
+ given to the use of abstraction in program construction. Refinement
+ with respect to partial and total correctness will be studied in more
+ detail, both for deterministic and nondeterministic programs. The
+ relationship between these refinement relations and the approximation
+ relation of fixpoint semantics will be studied, as well as the
+ connection with the predicate transformers used in program
+ verification.",
+ paper = "Back81.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Morgan, Carroll}
+\begin{chunk}{axiom.bib}
+@book{Morg98,
+ author = "Morgan, Carroll",
+ title = {{Programming from Specifcations, 2nd Ed.}},
+ publisher = "Prentice Hall",
+ year = "1998",
+ link =
+"\url{http://www.cse.unsw.edu.au/~carrollm/ProgrammingFromSpecifications.pdf}",
+ paper = "Morg98.pdf"
+}
+
+\end{chunk}
+
+\index{Filliatre, JeanChristophe}
+\begin{chunk}{axiom.bib}
+@phdthesis{Fill99,
+ author = "Filliatre, JeanChristophe",
+ title = {{Preuve de programmes imp\'eratifs en th\'eorie des types}},
+ school = {{Universit\'e ParisSud}},
+ year = "1999",
+ link = "\url{}",
+ paper = "Fill99.pdf"
+}
+
+\end{chunk}
+
+\index{Caldwell, James L.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Cald97,
+ author = "Caldwell, James L.",
+ title = {{Moving proofsasprograms into practice}},
+ booktitle = "Automated Software Engineering",
+ publisher = "IEEE",
+ year = "1997",
+ abstract =
+ "Proofs in the Nuprl system, an implementation of a constructive
+ type theory, yield “correctbyconstruction” pro grams. In this
+ paper a new methodology is presented for extracting efficient and
+ readable programs from inductive proofs. The resulting extracted
+ programs are in a form suitable for use in hierarchical
+ verifications in that they are amenable to clean partial evaluation
+ via extensions to the Nuprl rewrite system. The method is based on two
+ elements: specifications written with careful use of the Nuprl
+ settype to restrict the extracts to strictly computational content;
+ and on proofs that use induction tactics that generate extracts
+ using familiar fixedpoint combinators of the untyped lambda
+ calculus. In this paper the methodology is described and its
+ application is illustrated by example.",
+ paper = "Cald97.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Talpin, JeanPierre}
+\index{Jouvelot, Pierre}
+\begin{chunk}{axiom.bib}
+@inproceedings{Talp92,
+ author = "Talpin, JeanPierre and Jouvelot, Pierre",
+ title = {{The Type and Effect Discipline}},
+ booktitle = "Conf. on Logic in Computer Science",
+ publisher = "Computer Science Press",
+ year = "1992",
+ abstract =
+ "The {\sl type and effect discipline} is a new framework for
+ reconstructing the principal type and the minimal effect of
+ expressions in implicitly typed polymorphic functional languages that
+ support imperative constructs. The type and effect discipline
+ outperforms other polymorphic type systems. Just as types abstract
+ collections of concrete values, {\sl effects} denote imperative
+ operations on regions. {\sl Regions} abstract sets of possibly aliased
+ memory locations.
+
+ Effects are used to control type generalization in the presence of
+ imperative constructs while regions delimit observable
+ sideeffects. The observable effects of an expression range over the
+ regions that are free in its type environment and its type; effects
+ related to local data structures can be discarded during type
+ reconstruction. The type of an expression can be generalized with
+ respect to the variables that are not free in the type environment or
+ in the observable effect.",
+ paper = "Talp92.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Davis, Jared Curran}
+\begin{chunk}{axiom.bib}
+@phdthesis{Davi09,
+ author = "Davis, Jared Curran",
+ title = {{A SelfVerifying Theorem Prover}},
+ school = "University of Texas at Austin",
+ year = "2009",
+ abstract =
+ "Programs have precise semantics, so we can use mathematical proof to
+ establish their properties. These proofs are often too large to
+ validate with the usual “social process” of mathematics, so instead we
+ create and check them with theoremproving software. This software
+ must be advanced enough to make the proof process tractable, but this
+ very sophistication casts doubt upon the whole enterprise: who
+ verifies the verifier?
+
+ We begin with a simple proof checker, Level 1, that only accepts
+ proofs composed of the most primitive steps, like Instantiation and
+ Cut. This program is so straightforward the ordinary, social process
+ can establish its soundness and the consistency of the logical
+ theory it implements (so we know theorems are “always true”).
+
+ Next, we develop a series of increasingly capable proof checkers,
+ Level 2, Level 3, etc. Each new proof checker accepts new kinds of
+ proof steps which were not accepted in the previous levels. By taking
+ advantage of these new proof steps, higherlevel proofs can be
+ written more concisely than lowerlevel proofs, and can take less time
+ to construct and check. Our highestlevel proof checker, Level 11, can
+ be thought of as a simplified version of the ACL2 or NQTHM theorem
+ provers. One contribution of this work is to show how such systems can
+ be verified.
+
+ To establish that the Level 11 proof checker can be trusted, we first
+ use it, without trusting it, to prove the fidelity of every Level n to
+ Level 1: whenever Level n accepts a proof of some $\phi$, there exists a
+ Level 1 proof of $\phi$. We then mechanically translate the Level 11 proof
+ for each Level n into a Level n − 1 proof—that is, we create a Level 1
+ proof of Level 2’s fidelity, a Level 2 proof of Level 3’s fidelity,
+ and so on. This layering shows that each level can be trusted, and
+ allows us to manage the sizes of these proofs.
+
+ In this way, our system proves its own fidelity, and trusting Level 11
+ only requires us to trust Level 1.",
+ paper = "Davi09.pdf"
+}
+
+\end{chunk}
+
+\index{Myreen, Magnus O.}
+\index{Davis, Jared}
+\begin{chunk}{axiom.bib}
+@article{Myre14,
+ author = "Myreen, Magnus O. and Davis, Jared",
+ title = {{The Reflective Milawa Theorem Prover is Sound}},
+ journal = "LNAI",
+ pages = "421436",
+ year = "2014",
+ abstract =
+ "Milawa is a theorem prover styled after ACL2 but with a small kernel
+ and a powerful reflection mechanism. We have used the HOL4 theorem
+ prover to formalize the logic of Milawa, prove the logic sound, and
+ prove that the source code for the Milawa kernel (2,000 lines of Lisp)
+ is faithful to the logic. Going further, we have combined these
+ results with our previous verification of an x86 machinecode
+ implementation of a Lisp runtime. Our toplevel HOL4 theorem states
+ that when Milawa is run on top of our verified Lisp, it will only
+ print theorem statements that are semantically true. We believe that
+ this toplevel theorem is the most comprehensive formal evidence of a
+ theorem prover’s soundness to date.".
+ paper = "Myre14.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Davis, Jared}
+\index{Myreen, Magnus O.}
+\begin{chunk}{axiom.bib}
+@article{Davi15,
+ author = "Davis, Jared and Myreen, Magnus O.",
+ title = {{The Reflective Milawa Theorem Prover is Sound}},
+ journal = "J. Automated Reasoning",
+ volume = "55",
+ number = "2",
+ pages = "117183",
+ year = "2015",
+ abstract =
+ "This paper presents, we believe, the most comprehensive evidence of a
+ theorem prover’s soundness to date. Our subject is the Milawa theorem
+ prover. We present evidence of its soundness down to the machine
+ code. Milawa is a theorem prover styled after NQTHM and ACL2. It is
+ based on an idealised version of ACL2’s computational logic and
+ provides the user with highlevel tactics similar to ACL2’s. In
+ contrast to NQTHM and ACL2, Milawa has a small kernel that is somewhat
+ like an LCFstyle system. We explain how the Milawa theorem prover is
+ constructed as a sequence of reflective extensions from its
+ kernel. The kernel establishes the soundness of these extensions
+ during Milawa’s bootstrapping process. Going deeper, we explain how
+ we have shown that the Milawa kernel is sound using the HOL4 theorem
+ prover. In HOL4, we have formalized its logic, proved the logic sound,
+ and proved that the source code for the Milawa kernel (1,700 lines of
+ Lisp) faithfully implements this logic. Going even further, we have
+ combined these results with the x86 machinecode level verification of
+ the Lisp runtime Jitawa. Our toplevel theorem states that Milawa can
+ never claim to prove anything that is false when it is run on this
+ Lisp runtime.",
+ paper = "Davi15.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Myreen, Magnus O.}
+\begin{chunk}{axiom.bib}
+@article{Myre12,
+ author = "Myreen, Magnus O.",
+ title = {{Functional Programs: Conversions between Deep and Shallow
+ Embeddings}},
+ journal = "LNCS",
+ volume = "7406",
+ pages = "412417",
+ year = "2012",
+ abstract =
+ "This paper presents a method which simplifies verification of deeply
+ embedded functional programs. We present a technique by which
+ proofcertified equations describing the effect of functional
+ programs (shallow embeddings) can be automatically extracted from their
+ operational semantics. Our method can be used in reverse, i.e. from
+ shallow to deep embeddings, and thus for implementing certifying code
+ synthesis: we have implemented a tool which maps HOL functions to
+ equivalent Lisp functions, for which we have a verified Lisp runtime.
+ A key benefit, in both directions, is that the verifier does not need
+ to understand the operational semantics that gives meanings to the
+ deep embeddings.",
+ paper = "Myre12.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
+
+\index{Myreen, Magnus O.}
+\index{Davis, Jared}
+\begin{chunk}{axiom.bib}
+@article{Myre11,
+ author = "Myreen, Magnus O. and Davis, Jared",
+ title = {{A Verified Runtime for a Verified Theorem Prover}},
+ journal = "NCS",
+ volume = "6898",
+ pages = "265280",
+ year = "2011",
+ abstract =
+ "Theorem provers, such as ACL2, HOL, Isabelle and Coq, rely on the
+ correctness of runtime systems for programming languages like ML,
+ OCaml or Common Lisp. These runtime systems are complex and critical
+ to the integrity of the theorem provers.
+
+ In this paper, we present a new Lisp runtime which has been formally
+ verified and can run the Milawa theorem prover. Our runtime consists
+ of 7,500 lines of machine code and is able to complete a 4 gigabyte
+ Milawa proof effort. When our runtime is used to carry out Milawa
+ proofs, less unverified code must be trusted than with any other
+ theorem prover.
+
+ Our runtime includes a justintime compiler, a copying garbage collector,
+ a parser and a printer, all of which are HOL4verified down to
+ the concrete x86 code. We make heavy use of our previously developed
+ tools for machinecode verification. This work demonstrates that our
+ approach to machinecode verification scales to nontrivial
+ applications.",
+ paper = "Myre11.pdf",
+ keywords = "printed"
+}
+
+\end{chunk}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index a9183bf..20f6c5a 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5916,6 +5916,8 @@ books/bookvolbug bug 7335: type resolution failure
books/bookvol10.1 add new chapter
20180304.01.tpd.patch
proposal
+20180309.01.tpd.patch
+books/bookvolbib add references

1.9.1