In 1979 Bates [Bates 79] proposed the notion of refinement logic and an interactive style of doing proofs in such a logic (see also [Kay & Goldberg 77,Smullyan 68,Toledo 75]). At the same time our experience with the Cornell Program Synthesizer of R. Teitelbaum and T. Reps [Teitelbaum & Reps 81] directly influenced our thinking about proof editors. Some of these ideas were first tested by Krafft for the PL/CV logic in a system called AVID [Krafft 81]. Bates also proposed specific ways to extract executable code from constructive proofs that would be efficient enough for use in a programming system. In 1982 a specific system of this kind was designed and implemented by the Prl group at Cornell [Bates & Constable 85, Staff 83]; that system is .
The
system was designed to interact with the metalanguage ML from
the Edinburgh LCF project [Gordon, Milner, & Wadsworth 79].
The
system also incorporated decision procedures from the PL/CV project;
indeed
the early
style of automated reasoning is a synthesis of the ideas
from AUTOMATH, PL/CV and LCF.
Now a distinctive new style is emerging, a style
which will be reported in the work
of some of the authors of this monograph.
The logic itself was designed as an attempt to present the Cornell version of constructive type theory in the setting a of refinement--style logic. The result of this design is embodied in the system and in this document.