Cornell University Department of Computer Science 1995 M.S. Computer Science (Awarded on Completion of A-Exam)
At Cornell I work in the Nuprl
group. My thesis advisor is Robert
Constable.
My Ph.D. research is in the application of constructive logic to the
development of correct and safe decision procedures. Among the
various approaches to formally justifying correctness for executable
requirements and programs perhaps the most interesting, but least well
understood, is the approach based on the so-called proofs-as-programs
paradigm. By a beautiful theoretical result know as the Curry-Howard
Isomorphism, constructive type theory can be used to encode
higher-order constructive logic. Unlike other approaches which
separate the concerns of programming from correctness proofs, those
based on constructive type theories (like that implemented in the
Nuprl system) provide a means of extracting programs directly from the
proofs. Under the encoding, type expressions in the type theory
correspond to propositions in the logic, and proofs of a proposition
in the logic correspond to programs inhabiting the corresponding type.
In practice, this means a constructive proof of a theorem is an
encoding for a program. Since the program is explicitly extracted
from the correctness proof itself, it is "correct by construction."
For my dissertation I am using the Nuprl system to extract
programs from proofs of decidability for sequent formulations of both
classical propositional logic and intuitionistic propositional logic.
In both cases the programs extracted from the proofs turn out to be
implementations of the tableau method.
State University of New York at Albany Department of Computer Science 1988 M.S. Computer Science 1984 B.S. Computer Science
For my M.S. project I worked with Dan Rosenkrantz on matching algorithms in hypergraphs.
