http:^^www.cs.cornell.edu^info^faculty^rc^rc.html

This data set contains WWW-pages collected from computer science departments of various universities

MIME-Version: 1.0
Server: CERN/3.0
Date: Sunday, 01-Dec-96 20:31:43 GMT
Content-Type: text/html
Content-Length: 5937
Last-Modified: Wednesday, 25-May-94 14:05:15 GMT

<title>Robert L. Constable</title>

<h1>
<img src="rc-photo.gif">
Robert L. Constable<br>
Department Chair/Professor<br>
[e-mail]</h1>

Ph.D. University of Wisconsin, Madison, 1968<p>

<h2>Research</h2>

We are engaged in the study of computer systems that provide
mechanical assistance in problem solving, especially in programming
and mathematics.  This involves a long term study of ways to make the
formalization of mathematics feasible and useful.  We have implemented
three such systems in the past tne years: PL/CV, PRL, and Nuprl.<p>

Our major experimentation is with <a
href="/Info/Projects/Nuprl/nuprl.html">Nuprl</a>, a 60,000-line Lisp
program that implements a constructive theory of types.  Systems such
as Nuprl are useful formalizations of mathematics because they can
express a wide variety of proof and program-building methods as
metalevel programs of the system.  These provide considerable theorem
proving power.  Moreover, Nuprl is especially useful because it can
evaluate the computational content of theorems.  In principle, Nuprl
is both a fomal system of mathematics and a programming language.<p>

We continue to improve Nuprl; the current version used at Cornell is
called Nuprl 4.  It differs from its predecessors in having a new term
editor designed by Stuart Allen and implemented by Richard Eaton.  Its
internal structure is more modular, making the system suitable for he
definition of a wide variety of logics beyond the built-in
constructive type theory.  Also, the entire theorem-proving mechanism
has been rebuilt and stream-lined by Paul Jackson, building on the
work of Douglas Howe.  This contributes to the generic nature of Nuprl
4.  Finally, this version of the system can refer to itself.  There is
an internal description of the language and its logic built
principally by William Aitken using the theory developed by Allen,
Howe, and myself.  Richard Eaton designed a link between the internal
description of the logic and the logic itself, which makes it possible
to prove theorems about the process of proving theorems.<p>

We are also engaged in three exciting joint ventures.  One is with
Miriam Leeser of Electrical ENgineering and the other two are in
Computer Science; with <a href="/Info/Faculty/gries/gries.html">David
Gries</a> on Polya and with <a href="/Info/People/rz/rz.html"> Richard
Zippel</a> on <a href="/Info/Projects/Weyl/weyl.html">Weyl</a>.  With
Lesser, we are involved in hardware synthesis and verification.
Leeser and her student Mark Aagard have used Nuprl to prove the
correctness of a 1000-line boolean circuit minimization package, Pbs,
used by circuit designers.  This is a component of Leeser's Bedroc
system (it implements the weak division algorithm, which is widely
used in circuit design systems).  This major theorem proving effort
taught us a great deal about the effectiveness of our technology in
the hands of expert users from an application domain.<p>

The second joint venture involves building a model of the <a
href="/Info/Projects/Polya/polya.html">Polya</a> programming language and a
program refinement mechanism for it, both designed by David Gries,
which will enable him to write his handbook of algorithms in the
manner that he devised through years of study of the programming
process.  Stuart Allen has givne a formal type-theoretic definition of
Polya.  We expect to be experimenting soon with transforms and trying
to capture the programming style that Gries wants.<p>

We have recently begun a collaboration that we hope to relate to the
Polya effort.  Conal Mannion has been exploring the possibility of
using Nuprl in computational science.  We have been discussing
problems with Richard Zippel and are hoping to connect Zippel's
symbolic algebra system, Weyl, with Nuprl in the near future.  This
will be used to explore the development of scientific computing
software using Weyl and Nuprl together with other tools that Zippel is
building.<p>

<h2>Professional Activities</h2>

<dl>
<dt>Editor, <var>Journal of Symbolic Computation</var>
<dt>Editor, Academic Press
<dt>Editor, <I>Journal of Logic and Computation</i>
<dt>Editor, Oxford University Press
<dt>General Chair, LICS
<dt>Program Committee, North American Jumelage
<dt>Program Committee, Theoretical Aspects of Computer Software
<dt>Referee/Reviewer: NSERC (Canada), NSF, <cite>Theoretical Computer Science</cite>
</dl>

<h2>University Activities</h2>

<dl>
<dt>Chair, Computer Science Recruiting Committee
<dt>Computer Science Computing Facilities Committee
<dt>Provost's Study Committee on Mathematics
</dl>

<h2>Lectures</h2>

<dl>
<dt>Formal theories and software systems: fundamental connections between
<dd>computer science and logic.  INRIA's 25th Anniversary Celebration, Paris, 
France, December 1992.
<dt>The Nuprl software development system.  Computer Science Colloquium, Ben
<dd>Gurion University, Ber Sheva, Israel, January 1993.
<dt>Formal theories and software systems.  State of Israel Symposium, Tel Aviv,
<dd>Israel, January 1993.
<dt>___. Association for Symbolic Logic, Annual Meeting, Notre Dame University,
<dd>Notre Dame, Indiana, March 1993.
<dt>Metaprogramming in type theory.  State University of New York, Buffalo,
<dd>New York, March 1993.
<dt>Formal explanations of software.  Formal Methods and Software Engineering
<dd>Workshop, University of Pennsylvania, Philadelphia, Pennsylvania, May 1993.
</dl>

<h2>Publications</h2>

<dl>
<dt>Formal theories and software systems: fundamental connections between
<dd>computer science and logic.  In <i>Future Tendencies in Computer Science,
Control and Applied Mathematics</i> (ed. A Bensoussan and J.-P. Verjus)
<i>Lecture Notes in Computer Science 653</i>, Springer-Verlag (December 1992),
105-127.
<dt>Metalevel programming in constructive type theory. In <i>Programming and
<dd>Mathematical Method</i> (ed. Manfred Broy), NATO ASI Series F88,
Springer-Verlag (1992), 45-93.
</dl>