|
|||
|
|||
Overall Workplan
- Year 1 (May 2001 - April 2002):
- We will improve and implement those
library services that allow us to cooperate in building theories among
ourselves at Cornell (office to office and system to system -- Nuprl
and MetaPRL). This will involve detailed work on sentinels, stable
tactic code, archival operations and local web editing. We will also
bring MetaPRL to a more advanced stage and expand our ability to
interact with it from the Nuprl logical library. We will continue to
develop the basic library of functions and data types and illustrate the
inter-linking of text, hyper-text, and formal content; and we will
continue to apply our LPE to the Ensemble protocol design and
verification.
- Year 2 (May 2002 - April 2003):
- We will extend our cooperation to the
three teams working remotely. One goal is to be able to merge libraries
developed independently at the three participating institutions. We will
use both the logical library and multiple refiners remotely. We aim to
extend web based editing among the group. At this stage we will call the
library a Common Logical Library. We will collectively demonstrate an
impact of the Library on one of our major applications, such as Ensemble
verification as well as on the basic library of functions and data
types.
- Year 3 (May 2003 - April 2004):
- We will begin to import theories from
other remote sites and export theory building and editing operations. We
will bring all of the capability to bear on the library of functions and
data types and applications. We will also organize a wider experiment
with the Common Logical Library by arranging to support other external
efforts as in HOL, PVS, or ACL2.
- Year 4 (May 2004 - April 2005):
- We will test the tools on a wider group
of remote users and bring more capability on-line to support the
emerging needs. We will also automate the process of creating links to
text and start planning to connect the Common Logical Library to an
active digital library effort at Cornell such as NCSTRL.
- Year 5 (May 2005 - April 2006):
- We will link our tools and results to
one of the digital libraries such as NCSTRL, supported at Cornell. The
Library will also support the code base for the subset of ML used in our
verification work along with components of application software such as
Ensemble.
February 2002