http:^^www.cs.cornell.edu^info^projects^nuprl^html^publication.html

来自「This data set contains WWW-pages collect」· HTML 代码 · 共 694 行 · 第 1/2 页

MIME-Version: 1.0
Server: CERN/3.0
Date: Monday, 25-Nov-96 00:40:53 GMT
Content-Type: text/html
Content-Length: 20145
Last-Modified: Sunday, 29-Sep-96 20:50:30 GMT

<TITLE>Nuprl Project Related Publications</TITLE>
<!body bgcolor="#ffffff">
<!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><img src="http://www.cs.cornell.edu/Info/Projects/NuPrl/icons/line.red.right.gif">

<H1>Nuprl Project Related Web Sites</H1>

<UL>
	<li><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><a href=http://www.altavista.digital.com/cgi-bin/query?pg=q&what=web&fmt=.&q=Nuprl> AltaVista(tm) Search</a>
	<LI> <!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><A HREF="http://www.cs.cornell.edu/Info/People/jackson/nuprl/index.html">	Paul Jackson's Nuprl Page</A>
</UL>

<!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><img src="http://www.cs.cornell.edu/Info/Projects/NuPrl/icons/line.red.right.gif">


<H1>Nuprl Project Online Papers</H1>

There are several formats used to present the papers accessible here.
<OL>
<LI> HTML : A hypertext version created using <!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><A HREF="http://cbl.leeds.ac.uk/nikos/tex2html/doc/latex2html/latex2html.html"> latex2html. </A>
<LI> PostScript : A downloadable PostScript version created using dvips.
<LI> NCSTRL : A pointer into the <!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><A HREF="http://cs-tr.cs.cornell.edu/"> Networked Computer Science Technical Reports Library. </A>
</OL>

<HR>

<UL>
<LI> Collaborative Mathematics Environments.
	[<!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><A HREF="http://www.cs.cornell.edu/Info/Projects/NuPrl/documents/colmath/it.html"> HTML </A>, 
         <!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><A HREF="http://www.cs.cornell.edu/Info/Projects/NuPrl/documents/colmath.ps"> PostScript </A>]
<LI> Constable, R.
<UL> <LI> Experience Using Type Theory as a Foundation for Computer Science, circa 1985-1995.
        [<!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><A HREF="http://www.cs.cornell.edu/Info/Projects/NuPrl/documents/make/make.html">HTML </A>]
</UL>

<LI> Constable, R.
<UL> <LI> Semantics of Evidence.
	[<!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><A HREF="http://www.cs.cornell.edu/Info/Projects/NuPrl/documents/semantics/it.html"> HTML </A>,
	 <!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><A HREF="http://cs-tr.cs.cornell.edu:80/Dienst/UI/2.0/Describe/ncstrl.cornell%2fTR85-684"> NCSTRL </A>]
</UL>
<LI> Constable, R.
<UL> <LI> The Value of Automated Deductions.
        [<!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><A HREF="http://www.cs.cornell.edu/Info/Projects/NuPrl/documents/deduction/deduction.html">HTML </A>]
</UL>    
<LI> Forester, M.
<UL> <LI> Formalizing Constructive Real Analysis.
	[<!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><A HREF="http://www.cs.cornell.edu/Info/Projects/NuPrl/documents/real-analysis/it.html"> HTML </A>,
	 <!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><A HREF="http://cs-tr.cs.cornell.edu:80/Dienst/UI/2.0/Describe/ncstrl.cornell%2fTR93-1382"> NCSTRL </A>,
         <!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><A HREF="http://www.cs.cornell.edu/Info/Projects/NuPrl/documents/real-analysis.ps"> PostScript </A>]
</UL>
</UL> 

<!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><img src="http://www.cs.cornell.edu/Info/Projects/NuPrl/icons/line.red.right.gif">

<H1>Nuprl Project Related Publications</H1>

<ul>
   <li> <b>Published Papers and Chapters of Books</b>
     <p>
     <ol>
	<li>
	<font color="#ee0000">Aagaard, Mark and Leeser, Miriam,</font>
	<i>Verifying a Logic Synthesis Tool in Nuprl.</i>
	<b>Proceedings of Workshop on Computer-Aided Verification.</b>
	1992.
	Editor: Gregor Bochmann and David Probst,
	Publisher: Springer-Verlag,
	pp. 72-83.
	(To appear by Springer-Verlag, 1993)

	<li>
 	<font color="#ee0000">Allen, Stuart F. and Robert L. Constable and Douglas J. Howe and Willaim Aitken.</font>
	<i>The Semantics of Reflected Proof.</i>
	<b>Proc. of Fifth Symp. on Logic in Comp. Sci.</b>
	IEEE, 
	1990,
	pp. 95-197

	<li>
	<font color="#ee0000">Allen, Stuart F.</font>
	<i>A Non-Type-Theoretic Definition of Martin-Lof's Types.</i>
	<b>Proc. of Second Symp. on Logic in Comp. Sci.</b>
	IEEE,
	June 1987,
	pp. 215-224
       
	<li>
        <font color="#ee0000">Allen, Stuart F.</font>
        <i>A non-type-theoretic semantics for type-theoretic language.</i>
        <b>Cornell University.</b>
        1987

	<li>
	<font color="#ee0000">Basin, David A.</font>
	<i>Extracting circuits from constructive proofs.</i>
	<b>Dept. of Artificial Intelligence, Edinburgh.</b>
	1991,
	Research Paper 533,
	(Also appeared in Proc. of the IFIP-IEEE Int'l. Workshop on Form
	al Methods in VLSI Design, Miami USA, 1991.)


	<li>
	<font color="#ee0000">Basin, David A. and Douglas J.Howe,</font>
	<i>Some Normalization Properties of Martin-Lof's Type Theory, and Applications,</i>
	<b>Theoretical Aspects of Computer Software, Int. Conf. TACS '91,</b>
	(Lecture Notes in Computer Science, Vol. 526})
	Springer-Verlag,
	pp. 475-494,
	1991

	<li>
	<font color="#ee0000">Basin, D. and G. Brown and M. Leeser,</font>
	<i>Formally Verified Synthesis of Combinational Circuits,</i>
	<b>Integration: The International Journal of  VLSI Design,</b>
	1991,
	v. 11,
	pp. 235-250

       	<li>
	<font color="#ee0000">Basin, D. and R. Constable,</font>
	<i>Metalogical Frameworks,</i>
	<b>Proc. of the Second Annual Workshop on Logical Frameworks,</b>
	Edinburgh, UK,
	June 1991
	
	<li>
	<font color="#ee0000">Basin, David A.,</font>
	<i>Building Problem Solving Environments in Constructive Type Theory,</i>
	<b>Cornell University,</b>
	1990"

	<li>
	<font color="#ee0000">Basin, D. and P. Del Vecchio</font>
	<i>Hardware Specification, Verification and Synthesis,</i>
	<b>Hardware Specification, Verification and Synthesis:  Mathematical Aspects,</b>
	(Lecture Notes in Computer Science, Vol. 408)
	1989,
	pp. 333-357,
	Springer-Verlag

	<li>
	<font color="#ee0000">Basin, David A.,</font>
	<i>Building Theories in Nuprl,</i>
	<b>Proc. of Logic at Botik '89,</b>
	(Lecture Notes in Computer Science, Vol. 363),
	pp. 12-25,
	Springer-Verlag, Pereslavl-Zalesky, USSR,
	1989,
	(Cornell TR 88-932)

	<li>
	<font color="#ee0000">Basin, David A.,</font>
	<i>An environment for automated reasoning about partial functions</i>,
	<b>9th International Conference on Automated Deduction,</b>
	(Lecture Notes in Computer Science, Vol. 310),
	pp. 101-110,
	Springer-Verlag, NY,
	1988

	<li>
        <font color="#ee0000">Bates, J. L. and Robert L. Constable,</font>
        <i>Proofs as programs,</i>
        <b>ACM Trans. Program. Lang. and Syst.,</b>
	v. 7,
	n. 1,
	pp. 53-71,
	1985

	<li>
	<font color="#ee0000">Bundy, A. and F. van Harmelen and C. Horn and A. Smaill,</font>
	<i>The Oyster-Clam system,</i>
	<b>10th International Conference on Automated Design,</b>
	(Lecture Notes in Artificial Intelligence, Vol. 449),
	Springer-Verlag,
	1990,
	Stickel, M.E. (Editor),
	pp. 647-648

	<li>
	<font color="#ee0000">Chen, W.Z.,</font>
	<i>Tactic-based Theorem Proving and Knowledge-based Forward Chaining,</i>
	<b>Eleventh International Conference on Automated Deduction,</b>
	(Lecture Notes in A.I., Vol. 607),
	1992,
	D. Kapur (Editor),
	pp. 552-566,
	Springer-Verlag
	
	<li>
	<font color="#ee0000">Chirimar, J. and Douglas J.~Howe,</font>
	<i>Implementing Constructive Real Analysis: a Preliminary Report,</i>
	<b>Symposium on Constructivity in Computer Science,</b>
	Springer-Verlag,
	1991

	<li>
	<font color="#ee0000">Robert L. Constable,</font>
	<i>Exporting and reflecting abstract constructive meta-mathematics,</i>
	<b>Lecture Notes in Artificial Intelligence,</b>
	1994,
	Alan Bundy (Editor),
	p. 529,
	(12th International Conference on Automated Deduction),
	Springer-Verlag

        <li>
	<font color="#ee0000">Robert L. Constable,</font>
	<i>Expressing computational complexity in constructive type theory,</i>
        <b>LNCS/LNAI Proceedings, </b>
        (Lecture Notes in Computer Science),
        1994,
	pp. 131-144,
        Springer-Verlag

	<li>
	<font color="#ee0000">Robert L. Constable,</font>
	<i>Using Reflection to Explain and Enhance Type Theory</i>,
	<b>Proof and Computation</b>,
	1994,
	NATO ASI Series,
	Springer-Verlag

	<li>
	<font color="#ee0000">Constable, Robert L. and Paul B. Jackson,</font>
	<i>Towards Integrated Systems for Symbolic Algebra and Formal Constructive Mathematics,</i>
	To appear.,
	1994

	<li>
	<font color="#ee0000">Constable, Robert L. and Scott F. Smith,</font>
	<i>Computational Foundations of Basic Recursive Function Theory,</i>
	<b>Theoretical Computer Science B: Logic, semantics, and theory of programming,</b>
	1993,
	v. 121,
	pp. 89-112

	<li>
	<font color="#ee0000">Constable, Robert L.,</font>
	<i>Formal Theories and Software Systems:  
	Fundamental Connections between Computer Science and Logic,</i>
	<b>Future Tendencies in Computer Science, Control and Applied Mathematics,</b>
	(Lecture Notes in Computer Science, Vol. 653),
	Springer-Verlag,
	December, 1992,
	Bensoussan, A. and J.-P. Verjus (Editors),
	pp. 105-127

	<li>
	<font color="#ee0000">Constable, Robert L.,</font>
	<i>Metalevel Programming in Constructive Type Theory,</i>
	<b>Programming and Mathematical Method,</b>
	(NATO ASI Series, Vol. F88),
	Springer-Verlag,
	1992,
	Broy, Manfred (Editor),
	pp. 45-93

	<li>
	<font color="#ee0000">Constable, Robert L.,</font>
	<i>Lectures on: Classical Proofs as Programs,</i>
	<b>Constructive Methods of Computing Science,</b>
	(NATO ASI Series),
	M. Broy (Editor),
	1992

	<li>
	<font color="#ee0000">Constable, Robert L. and Chetan Murthy,</font>
	<i>Finding  Computational Content from Classical Proofs,</i>
	<b>Logical Frameworks,</b>
	Cambridge University Press,
	1991,
	Gerard Huet and Gordon Plotkin (Editors),
	pp. 341-362

	<li>
	<font color="#ee0000">Constable, Robert L.,</font>
	<i>Type Theory as a Foundation for Computer Science,</i>
	<b>Theoretical Aspects of Computer Software, Int. Conf. TACS '91,</b>
	(Lecture Notes in Computer Science, Vol. 526),
	1991,
	pp. 226-243

	<li>
	<font color="#ee0000">Constable, Robert L. and  Stuart F. Allen and Douglas J. Howe,</font>
	<i>Reflecting the Open-Ended Computation System of Constructive Type  Theory,</i>
	<b>Logic, Algebra and Computation,</b>
	(NATO ASI Series, Vol. F79),
	H. Schwichtenberg (Editor),
	1990

	<li>
        <font color="#ee0000">Robert L. Constable and Douglas J. Howe,</font>
        <i>Implementing Metamathematics as an Approach to Automatic Theorem Proving,</i>
        <b>Formal Techniques in Artificial Intelligence: A Source Book,</b>
        Elsevier Science Publishers (North-Holland),
        1990,
        R.B. Banerji (Editor),
        pp. 45-76

	<li>
	<font color="#ee0000">Constable, Robert L. and Douglas J. Howe,</font>
	<i>Nuprl as a General Logic,</i>
	<b>Logic in Computer Science,</b>
	Academic Press,
	1990,
	P. Odifreddi (Editor),
	pp. 77-90,
	(Cornell TR 89-1021)

	<li>
	<font color="#ee0000">Constable, Robert L.,</font>
	<i>Assigning Meaning to Proofs: a semantic basis for problem solving environments,</i>
	<b>Constructive Methods of Computing Science,</b>
	(NATO ASI Series, Vol. F55),
	M. Broy (Editor),
	pp. 63-91,
	1989 

	<li>
	<font color="#ee0000">Constable, Robert L. and Scott F. Smith,</font>
	<i>Computational Foundations of Basic Recursive Function Theory,</i>
	<b>Third Symp. on Logic in Comp. Sci.,</b>
	IEEE, Edinburgh, UK,
	pp. 360-371,
	1988,
	(Cornell TR 88-904)

	<li>
	<font color="#ee0000">Constable, Robert L. and Stuart F. Allen and H.M. Bromley and W.R. Cleaveland 
	and J.F. Cremer and R.W. Harper and Douglas J. Howe and T.B. Knoblock and 
	N.P. Mendler and P. Panangaden and James T. Sasaki and Scott F. Smith,</font>
	<b>Implementing Mathematics with the Nuprl Development System,</b>
	Prentice-Hall, NJ,
	1986

	<li>
	<font color="#ee0000">Constable, Robert L. and N.P. Mendler,</font>
	<i>Recursive Definitions in Type Theory,</i>
	<b>Proc. of Logics of Prog. Conf.,</b>
	pp. 61-78,