Thursday, 22 October 1998
Professor of Computer Science and
Chair, Computer Science Department
Cornell University
Listening to Theorem Provers Who Talk
4:00 pm, Wean Hall 7500
3:45 pm - Refreshments Outside Wean Hall 7500
to Each Other about Computer Systems
The amount of formalized mathematics is dramatically increasing. It is being generated by theorem provers as a by-product of mechanized reasoning about computer systems. This distributed collection is now a significant formal digital library.
Nowadays when reasoning about a system, it is compelling to reuse basic results regardless of the formal theory in which they are proved.
This talk explains a method for sharing mathematical facts among theorem provers based on very different logics such as HOL, a classical type theory, and Nuprl, a constructive theory. The method comes from Douglas Howe's work and is based on his new semantics for classical Nuprl. It allows us to relate PVS and Nuprl as well. The talk will stress how these ideas allow agents with different world views to communicate.
The talk will also mention our work on translating formal proofs into English as a means of documenting system components. In principle these proofs can be spoken.
SPEAKER BIO
Robert Constable has been a professor at Cornell University since 1968.
Currently he is serving as department chair.
In 1979, he and Joseph L. Bates stated the PRL project - an effort to use formal methods to develop programs that are "correct by construction." Now the project is concerned with building large systems this way. This project is nearly twenty years old with over twenty PhD graduates.
One of its experimental tools is the Nuprl family of theorem provers; another is the new MetaPRL logical framework initiated with Jason Hickey. The project URL is http://www.cs.cornell.edu, under Research Projects, Nuprl Project.
With his students and colleagues, Professor Constable has introduced a number of ideas and methods being actively investigated and used in various research communities, such as: the proofs-as-programs principle; the use of a rich computational type theory as a foundation for computer science; the study of control operators as computational content for assertions; the use of partial types to model domains and provide a semantics of programming languages; the use of tactic-trees to organize interactive theorem proving; and the integration of reflected decision procedures and tactic-provers.
Currently the PRL group is supported by DARPA to verify properties of the Ensemble group communication system built by Mark Hayden and others in Ken Birman's group at Cornell. Also Amanda Holland-Minkley of Cornell and Regina Barzilay of Columbia are integrating Nuprl with the FUF natural langauge generator to translate Nuprl proofs into English.