Our project has always been closely associated with advances in programming languages and programming environments. The PRL project is a successor to the PL/CV project (1975-79) which was part of a departmental interest in a dialect of PLI called PL/C. The parent project, PL/C, built and supported a compiler for the PL/C subset of PLI. The compiler was used at over 200 universities to teach programming.
In the mid-seventies we provided a denotational semantics for a subset of PL/C and then built a programmer verifier for that subset based on the mathematical semantics. The compiler enforced the restrictions needed to support the programming logic. This project also spawned the Cornell Program Synthesizer which provided a structure editor and debugging environment for these languages.
While we were making the transition to PRL by enriching the type system of our verifier, the language group at Cornell was designing and implementing Russell, a polymorphic higher type language. At Edinburgh in Scotland the programming language ML was being designed as part of the LCF theorem proving project. We were strongly influenced by both efforts. ML has become a major programming language of the 80s and 90s, and we have remained closely involved. Nuprl uses ML as its tactic language and a variant as its term language. We continue to modify the early compiler and are involved in both SML through the work of Rod Moten and OCaml through the work of Mark Hayden and Jason Hickey.
Since we use ML extensively, we have been interested in improvements to it. In one direction we have looked at object-oriented extensions such as Karl Crary's KML effort which is now being used in the TAL project of Morrisett and his students.
We are also interested in extending the type checking capabilities of ML by incorporating algorithms used in Nuprl. We call this effort Extended Static Checking (ESC). Ozan Hafizogullari and Christoph Kreitz have provided an extension to ML checking that includes array bounds checking.