Paul Jackson
Research Interests
Theorem proving environments, formal methods for software and
hardware development, computer algebra, synthesis of scientific programs,
linkage of software tools for engineering design.
Thesis Information
Paul's PhD thesis is entitled Enhancing the Nuprl Proof Development
System and Applying it to Computational Abstract Algebra.
The
abstract (3K)
is available, as is the full text in
dvi(216K)
and
postscript(311K)
formats.
Papers

Paul B. Jackson. Exploring Abstract Algebra in Constructive Type Theory. In A.
Bundy, editor, 12th International Conference on Automated
Deduction, Lecture Notes in Artifical Intelligence. SpringerVerlag,
June 1994.
The
abstract
is available, as is the full text in
dvi(25K)
and
postscript(59K) formats.

Paul B. Jackson. Nuprl and its use in circuit Design. In R.T. Boute,
V. Stavridou, T.F.Melham,editors, Proceedings of the 1992 Interational
Conference on Theorem Provers in Circuit Design , IFIP Transactions
A10. NorthHolland, 1992.
The
abstract
is available, as is the full text in
dvi(39K)
and
postscript(76K) formats.

Paul B. Jackson. Developing a Toolkit for floatingpoint hardware in the
Nuprl proof development system. In Proceedings of the
Advanced Research Workshop on correct Hardware Design Methodologies.
Elsevier, 1991.
Nuprl
Hypertext listings for some of the theories Paul developed for his thesis
are available on the
Nuprl Math Library page.
The listings for each theory include introductions,
summaries of definitions and theorems, and formatted proofs.