Next:
Background and problems to
Up:
An Open Logical Programming
Previous:
Abstract
Technical Plans
Background and problems to be solved
Background
Problems
Cornell and Bell Labs work
Outline of document
Proposed solutions
Verified code problem -- linking code to models and specifications.
Sound tools problem - a semantic basis for modeling interface.
Shared tools and models problem - sharing basic theories
Scalable environments problem - verifications in the large
Integration of tools problem - industrial environments
Design Issues
Details of relating type theories
Libraries for mathematics
Modular Construction
Implementation
Relating Large Libraries of Mathematics
Mathematics of logical library structure
Formal module systems
Relations between mathematical domains
Inheritance of results
Reflection with the implementation language
New capabilities
Bell Labs verifications
I/O automata and verification of group communications software
Program Extraction
Extraction of non-local control operators from Nuprl proofs.
Joan Lockwood
7/10/1998
