next up previous contents index
Next: Introduction to Type Up: Related Work Previous: Theoretical Background

Systems Background

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]. gif 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.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995