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:jackson@cs.cornell.edu">jackson@cs.cornell.edu</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>+1 (607) 255-6046<br><dt>department fax #: <dd>+1 (607) 255-4428<hr><h2>Research Interests</h2>Theorem proving environments, formal methods for software andhardware 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 DevelopmentSystem 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 AutomatedDeduction,</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 TransactionsA-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 theNuprl proof development system. In <cite> Proceedings of theAdvanced 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 workon it to make it more accessible. I or someone else will getround 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 thetheories I developed for my thesis are available.  The listings foreach theory include introductions, summaries of definitions andtheorems, and formatted proofs. The listings for thepolynomial-related theories are not included at the moment, but shouldbe 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:jackson@cs.cornell.edu">jackson@cs.cornell.edu</a> </address>