http:^^www.cs.cornell.edu^info^people^jackson^jackson.html

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

MIME-Version: 1.0
Server: CERN/3.0
Date: Wednesday, 20-Nov-96 19:31:37 GMT
Content-Type: text/html
Content-Length: 3315
Last-Modified: Monday, 27-Feb-95 02:12:50 GMT

<title>Paul Jackson's Home Page</title>

<h1>Paul Jackson</h1><br>

<!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><img src="http://www.cs.cornell.edu/Info/People/jackson/jackson2.gif"> <br>

<h2> Post-Doctoral Associate<br>
Cornell University </h2>
<p>
<dl>
<dt>e-mail: 
<dd><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><a href="mailto:[e-mail]">[e-mail]</a><br>
<dt>www: 
<dd>http://www.cs.cornell.edu/Info/People/jackson/jackson.html
<p>
<dt>address: <br>
<dd>  Department of Computer Science <br>
  4158 Upson Hall<br>
  Cornell University<br>
  Ithaca NY 14853<br>
  USA
<p>
<dt>phone #: 
<dd>[phone]<br>
<dt>department fax #: 
<dd>[phone]

<hr>

<h2>Research Interests</h2>
Theorem proving environments, formal methods for software and
hardware development, computer algebra, synthesis of scientific programs,
linkage of software tools for engineering design.

<h2>Thesis Information</h2>
My PhD thesis is entitled <cite> Enhancing the Nuprl Proof Development
System and Applying it to Computational Abstract Algebra</cite>.
The 
<!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><a href = "http://www.cs.cornell.edu/Info/People/jackson/thesis/abstract.html"> abstract </a>(3K)
is available, as is the full text in 
<!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><a href="http://www.cs.cornell.edu/Info/People/jackson/thesis/thesis.dvi.gz">dvi</a>(216K)
and 
<!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><a href="http://www.cs.cornell.edu/Info/People/jackson/thesis/thesis.ps.gz">postscript</a>(311K)
formats. 


<h2>Papers</h2>
<ul>
<li> 
Paul B. Jackson. Exploring Abstract Algebra in Constructive Type Theory.  In A.
Bundy, editor, <cite>12th International Conference on Automated
Deduction,</cite> Lecture Notes in Artifical Intelligence. Springer-Verlag, 
June 1994.  
<p>
The 
<!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><a href = "http://www.cs.cornell.edu/Info/People/jackson/papers/ab-alg-abstract.html"> abstract </a>
is available, as is the full text in 
<!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><a href="http://www.cs.cornell.edu/Info/People/jackson/papers/abalg.dvi.gz">dvi</a>(25K)
and 
<!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><a href="http://www.cs.cornell.edu/Info/People/jackson/papers/abalg.ps.gz">postscript</a>(59K) formats.
<p>
<li>
Paul B. Jackson. Nuprl and its use in circuit Design. In R.T. Boute, 
V. Stavridou, T.F.Melham,editors, <cite>Proceedings of the 1992 Interational 
Conference on Theorem Provers in Circuit Design </cite>, IFIP Transactions
A-10. North-Holland, 1992.
<p>
The 
<!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><a href = "http://www.cs.cornell.edu/Info/People/jackson/papers/tp-in-cd-abstract.html"> abstract </a>
is available, as is the full text in 
<!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><a href="http://www.cs.cornell.edu/Info/People/jackson/papers/tp-in-cd-92.dvi.gz">dvi</a>(39K)
and 
<!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><a href="http://www.cs.cornell.edu/Info/People/jackson/papers/tp-in-cd-92.ps.gz">postscript</a>(76K) formats.
<p>
<li> 
Paul B. Jackson. Developing a Toolkit for floating-point hardware in the
Nuprl proof development system. In <cite> Proceedings of the
Advanced Research Workshop on correct Hardware Design Methodologies</cite>.
Elsevier, 1991.
</ul>
<p>

<h2>Nuprl</h2>
The Nuprl project has its own 
<!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><a href="http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html">
World-Wide Web home page </a>. From here, you can access documentation on 
Nuprl and communicate with a live Nuprl session that has some basic 
theories loaded. This collection of Nuprl pages still needs further work
on it to make it more accessible. I or someone else will get
round to paying some attention to this, sometime in the next month or two.
<p>
<!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><a href="http://www.cs.cornell.edu/Info/People/jackson/nuprl/index.html"> Hypertext listings </a> for most of the
theories I developed for my thesis are available.  The listings for
each theory include introductions, summaries of definitions and
theorems, and formatted proofs. The listings for the
polynomial-related theories are not included at the moment, but should
be in the next couple of days.


<hr>
Last Modified Feb 25th, 1995<p>

<address> Paul Jackson / <!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><a href="mailto:[e-mail]">[e-mail]</a> </address>