|
(1) |
Develop proof-checking and model checking for certifying proofs
of the standard body of computationally related mathematics.
|
|
The PhD thesis of A. Nogin deals with this topic.
Theory and Implementation of an Efficient Tactic-Based Logical Framework.
The paper by James Caldwell and John Cowles shows how to use one prover,
ACL2, to certify results in another, Nuprl.
Representing Nuprl Proof Objects in ACL2: Toward a Proof Checker for Nuprl.
MetaPRL ---
A Modular Logical Environment.
This multiple-author paper
describes one of the systems we use to generate content.
|
|
(2) | Catalog those principal mathematical
concepts, together with their formal definitions, which are used in
contemporary computing. |
|
At present we rely on collecting the content into books and displaying them on
the Web in the Nuprl Libraries and PVS Libraries. The inter-book hyperlinks provide navigation. The FDL content allows
full interobject linking and is described in The FDL Navigator: Browsing and
Manipulating Formal Content.
|
|
(3) | Investigate suitable base language and logic
within which competing logics can be expressed and evaluated. |
|
This paper by Robert Constable discusses the logical issues that
arise in trying to relate constructive and
classical theorem provers. It discusses Evan
Moran's extensions of Howe's results relating
Computational Type Theory (CTT) to classical
ZFC set theory. It also discusses the Logic
of Events.
Information-Intensive Proof Technology, by Robert Constable.
This paper by Robert Constable surveys the ideas of general type theory that underlie many theorem provers and proof development systems. The vast majority of these systems use type theory.
Naive Computational Type Theory.
This LICS 2003 paper by A. Kopylov introduces
the dependent intersection type and shows how to
use it to define dependent records and thus to
internalize formal theories. It illustrates these
ideas with abstract algebra examples. The results
apply to the structure of libraries, for example
showing how to internalize Automath-like contexts.
Dependent Intersection: A New Way of Defining Records in Type Theory.
This paper by Robert Constable shows how Kopylov's
results apply to Automath and it also discusses results
in A. Nogin's PhD thesis that improve the axiomatic
basis for quotient structures in type theories.
Recent Results in Type Theory and Their Relationship to Automath.
|
|
(4) | Provide automated assistance for routine
aspects of developing libraries of formal theorems, proofs, algorithms, and
their expressions as programs. |
|
This paper by J. Hickey, A. Nogin, A. Granicz, and
B. Aydemir shows how
to structure a compiler as a sequence of program
transformation algorithms that are formalized in
a logical framework and stored in a formal digital
library.
Formal Compiler Implementation in a Logical Framework, by Jason Hickey, et al.
The FDL Navigator: Browsing and
Manipulating Formal Content by Christoph Kreitz shows how to provide basic operations of creating definitions and theorems in the FDL.
|
|
|
(5) | Investigate forms of assured interoperation
for assembling, composing, specializing, and generalizing algorithmic
knowledge. |
|
The fundamental papers of Stuart Allen deal precisely with these issues.
Notes on the Design and Purpose of the FDL.
Abstract Identifiers and
Textual Reference.
|
|
(6) |
Investigate reflection for coordination, interoperation, and
dynamic adaptation.
|
|
Reflection is critical both to content and to relating theories. The paper of PhD student Eli Barzilay with Stuart Allen is one example.
Reflecting
Higher-Order Abstract Syntax in Nuprl.
The system description by Barzilay, Allen and Constable is another contribution.
Practical Reflection in Nuprl.
|
|
(7) | Study issues of consistency and maintenance among
libraries. |
|
This paper by Robert Constable gives an account
of Doug Howe's result that Classical CTT is
consistent (see Howe's Semantic Foundations
for Embedding HOL in Nuprl).
Information-Intensive Proof Technology, by Robert Constable.
The papers of Stuart Allen cited in (5) also deal with consistency.
|
|
(8) | Address the human-computing aspects of
syntaxes and concepts that are appropriate for both foundational developers and
end-users. |
|
We use two specialized editors, one for Nuprl and one for the FDL that also
applies to Nuprl. We have not written articles, but the work of Lori Lorigo on
the XML interface is relevant. See Latest News.
|
|
(9) | Explore innovative metaphors and protocols for
understanding, using, composing, searching, authenticating, and validating
constructive results. |
|
The Master's thesis of Xin Yu deals with connecting constructive
mathematics and classical.
Formalizing Abstract Algebra in Constructive Set Theory.
|
|
(10) | Examine
models of applicable assurance structures and their economics. |
|
|
|
