An Open Logical Programming Environment:
A Practical Framework for Sharing Formal Models and Tools
Background and problems to be solved
Cornell and Bell Labs work
Outline of proposal
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
Details of relating type theories
Libraries for mathematics
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
Bell Labs verifications
I/O automata and verification of group communications software
Extraction of non-local control operators from Nuprl proofs.
About this document ...