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

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

	January 1985,
	(Cornell TR 85-659)

	<li>
	<font color="#ee0000">Constable, Robert L.,</font>
	<i>Constructive Mathematics as a programming logic:  some principles of theory,</i>
	<b>Annals of Mathematics,</b>
	Vol. 24,
	Elsevier Science Publishers, B.V. (North-Holland),
	1985,
	(Reprinted from 
		<i>Topics in the Theory of Computation, </i>
		<b> Selected Papers of the Intnl. Conf. on "Foundations of Computation Theory," FCT '83</b>
	)

	<li>
	<font color="#ee0000">Constable, Robert L. and T. Knoblock and J.L. Bates,</font>
	<i>Writing programs that construct proofs,</i>
	<b>J. Automated Reasoning,</b>
	v. 1,
	n. 3,
	pp. 285-326,
	1984

	<li>
	<font color="#ee0000">Constable, Robert L. and Michael J. O'Donnell,</font>
        <b>A Programming Logic</b>,
        Winthrop, Mass,
        1978

	<li>	
        <font color="#ee0000">Constable, Robert L.,</font>
        <i>Constructive mathematics and automatic program writers,</i>
        <b>Proc. IFIP Congr.,</b>
        Ljubljana,
	pp. 229-233,
        1971

	<li>
	<font color="#ee0000">Giunchiglia, F. and A. Smaill,</font>
	<i>Reflection in constrcutive and non-constructive automated reasoning,</i>
	<b>Meta-Programming in Logic Programming,</b>
	MIT Press,
	1989,
	Abramson, H. and M.H. Rogers (Editors),
	pp. 123-140

	<li>
	<font color="#ee0000">Horn, C.,</font>
	<i>The Nuprl proof development system,</i>
	<b>Dept. of Artificial Intelligence, Edinburgh,</b>
	1988,
	Working paper 214

        <li>
	<font color="#ee0000">Howe, Douglas J.and Stoller, Scott D.,</font>
        <i>An operational approach to combining classical set theory and functional programming languages, </i>
        <b>International Symposium TACS '94,</b>
        (Lecture Notes in Computer Science),
        Springer-Verlag,
        1994,
	Goos, G. and Hartmanis, J. (Editors),
        pp. 36-55

	<li>
	<font color="#ee0000">Howe, Douglas J.,</font>
	<i>Reasoning About Functional Programs in Nuprl,</i>
	<b>Functional Programming, Concurrency, Simulation and Automated Reasoning,</b>
	(Lecture Notes in Computer Science),
	1993,
	(To appear)

	<li>
	<font color="#ee0000">Howe, Douglas J.,</font>
	<b>A Simple Type Theory for Reasoning about Functional Programs.</b>
	Computer Science Department, Cornell Univeristy,
	(Pre print),
	1992

	<li>
	<font color="#ee0000">Howe, Douglas J.,</font>
	<i>Equality in Lazy Computation Systems,</i>
	<b>Proc. of Fourth Symp. on Logic in Comp. Sci.,</b>
	1989,
	IEEE Computer Society,
	pp. 198-203

	<li>
	<font color="#ee0000">Howe, Douglas J.,</font>
	<i>Computational Metatheory in Nuprl,</i>
	<b>9th International Conference on Automated Deduction,</b>
	(Lecture Notes in Computer Science, Vol. 310),
	E. Lusk and R. Overbeek (Editors),
	pp. 238-257,
	Springer-Verlag, New York,
	1988

	<li>
	<font color="#ee0000">Howe, Douglas J.,</font>
	<b>Automating Reasoning in an Implementation of Constructive Type Theory</b>,
	Cornell University,
	1988

	<li>
	<font color="#ee0000">Howe, Douglas J.</font>
	<i>Implementing Number Theory: An Experiment with Nuprl,</i>
	<b>8th International Conference on Automated Deduction,</b>
	(Lecture Notes in Computer Science, Vol. 230),
	1987,
	pp. 404-415

	<li>
	<font color="#ee0000">Howe, Douglas J.</font>
	<i>The Computational Behaviour of Girard's Paradox</i>
	<b>Proc. of Second Symp. on Logic in Comp. Sci.</b>
	IEEE,
	1987,
	pp. 205--214

	<li>
	<font color="#ee0000">Jackson, Paul B. and Robert L. Constable,</font>
	<i>Type Theory for Computer Algebra,</i>
	(In preparation),
	1995

	<li>
	<font color="#ee0000">Paul B. Jackson,</font>
	<b>Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra,</b>
	Cornell University,
	1994,
	Ithaca, NY,

	<li>
	<font color="#ee0000">Paul B.~Jackson,</font>
	<b>The Nuprl Proof Development System, Version 4.1 Reference Manual and User's Guide,</b>
	Cornell University,
	Ithaca, NY,
	1994

	<li>
	<font color="#ee0000">Paul B. Jackson,</font>
	<i>Exploring Abstract Algebra in Constructive Type Theory</i>,
	<b>12th Conference on Automated Deduction</b>,
	1994,
	A. Bundy (Editor),
	Springer-Verlag,
	New York

	<li>
	<font color="#ee0000">Jackson, Paul B.,</font>
	<i>Developing a toolkit for floating-point hardware in the Nuprl proof development system, </i>
	<b>Advanced Research Workshop on Correct Hardware Design Methodologies,</b>
	pp. 401-419,
	Organized by ESPRIT, Turin, Italy,
	June 1991

	<li>
	<font color="#ee0000">Jackson, Paul B.,</font>
	<i>Nuprl and its Use in Circuit Design, </i>
	<b>Proceedings of the IFIP TC10/WG10.2 
	International Conference on Theorem Provers in Circuit Design: 
	Theory, Practice and Experience, </b> 
	V. Stavridou, T.F. Melham and R.T. Boute (Editors),
	pp. 311-336,
	North-Holland, The Netherlands,
	1992

	<li>
	<font color="#ee0000">Paul B. Jackson,</font>
	<b>Logic-Based Knowledge Representation,</b>
	MIT Press, Cambridge, MA,
	1989

	<li>
        <font color="#ee0000">Knoblock, Ted,</font>
        <b>Mathematical Extensibility in Type Theory</b>,
        Cornell University,
        1987

	<li>
	<font color="#ee0000">Knoblock, Ted B. and Robert L. Constable,</font>
	<i>Formalized Metareasoning in Type Theory,</i>
	<b>Proc. of the First Symp. on Logic in Comp. Sci.,</b>
        pp. 237-248,
	1986,
	IEEE

	<li>
	<font color="#ee0000">Kreitz, Charles,</font>
	<b>Constructive Automata Theory Implemented with the Nuprl Proof Development System,</b>
	Cornell University,
	1986,
	Ithaca, New York

	<li>
	<font color="#ee0000">Kreitz, Charles,</font>
	<b>Meta-Synthesis:  Deriving Programs that Develop Programs,</b>
	Technical University of Darmstadt,
	November, 1992

	<li>
	<font color="#ee0000">O'Leary, John; Miriam Leester; Jason Hickey; and Mark Aagaard,</font>
	<i>Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization,</i>
	<b>International Conference on Theorem Proving &amp;  Circuit Design,</b>
	1994

	<li>
	<font color="#ee0000">Leeser, Miriam,</font>
	<i>Using Nuprl for the verification and synthesis of hardware,</i>
	<b>Phil. Trans. R. Soc. Lond.</b>,
	1992,
	v. 339,
	pp. 49-68

	<li>
	<font color="#ee0000">Madden, P.,</font>
	<i>Automatic program optimization via the transformation of Nuprl synthesis proofs, </i>
	<b>Proc. of the 1988 Alvey Technical Conf.,</b>
	1988,
	Clarke, L. (Editor),
	(Also available from Edinburgh as DAI Research Paper No. 392)

	<li>
	<font color="#ee0000">Mendler, P.F.</font>
	<i>Recursive Types and Type Constraints in Second-Order Lambda Calculus</i>
	<b>Proc. of Second Symp. on Logic in Comp. Sci.</b>
	IEEE,
	1987,
	pp. 30-36

	<li>
	<font color="#ee0000">Mendler, P.F.,</font>
	<b>Inductive Definition in Type Theory,</b>
	Cornell University,
	Ithaca, NY,
	1988

	<li>
	<font color="#ee0000">Mendler, N.; Robert L.~Constable; and P. Panangaden</font>
	<i>Infinite Objects in Type Theory</i>
	<b>Proc. of First Symp. on Logic in Comp. Sci.</b>
	IEEE,
	1986,
	pp. 249-257
	(Cornell TR 86-743)

	<li>
	<font color="#ee0000">Murthy, Chetan,</font>
	<i>A computational analysis of Girard's translation and LC,</i>
	<b>Proc. of Seventh Symp. on Logic in Comp. Sci.,</b>
	1992

	<li>
	<font color="#ee0000">Murthy, Chetan,</font>
	<i>An Evaluation Semantics for Classical Proofs,</i>
	<b>Proc. of Sixth Symp. on Logic in Comp. Sci.,</b>
	1991,
	pp. 96-109,
	IEEE, Amsterdam, The Netherlands

	<li>
	<font color="#ee0000">Russell, J. and Chetan Murthy,</font>
	<i>A Direct Constructive Proof of Higman's Lemma,</i>
	pp. 257-269,
	<b>Proc. of Fifth Symp. on Logic in Comp. Sci.,</b>
	IEEE,
	1990

	<li>
	<font color="#ee0000">Murthy, Chetan,</font>
	<b>Extracting Constructive Content for Classical Proofs</b>,
	Cornell University, Dept. of Computer Science,
	1990,
	(TR 89-1151)

	<li>
        <font color="#ee0000">Sasaki, James T.,</font>
        <b>The Extraction and Optimization of Programs from Constructive Proofs,</b>
        Cornell University,
        1985

	<li>
        <font color="#ee0000">Smith, Scott F. and Robert L. Constable,</font>
        <i>Partial objects in constructive type theory, </i>
	<b>Proc. of Second Symp. on Logic in Comp. Sci.,</b>
	IEEE, Washington, D.C.,
	pp. 183-93,
        1987
	
	<li>
	<font color="#ee0000">Smith, Scott F.,</font>
	<b>Partial Objects in Type Theory,</b>
	Cornell University,
	Ithaca, NY,
	1989

	<li>
	<font color="#ee0000">J.L. Underwood,</font>
	<b>Aspects of the Computational Content of Proofs,</b>
	Cornell University,
	1994,
	Ithaca, NY
	(Cornell TR94-1460)
	
	<li>
	<font color="#ee0000">Underwood, Judith,</font>
	<i>The Tableau Algorithm for Intuitionistic Propositional 
  	Calculus as a Constructive Completeness Proof</i>,
	<b>Proceedings of the Workshop on Theorem Proving with Analytic Tableaux,</b>
  	Marseille, France,
        pp. 245-248,
	1993,
	(Available as Technical Report MPI-I-93-213
  	Max-Planck-Institut fur Informatik, Saarbrucken, Germany)

	<li>
	<font color="#ee0000">Underwood, Judith,</font>
	<b>A Constructive Completeness Proof for the Intuitionistic Propositional Calculus</b>,
	Cornell University,
	(Cornell TR90-1179),
	1990
    </ol>
    <p>
  <li> <b>Research Papers</b>
    <p>
	<ul>
		<li> <font color="#eeee00">Coming soon
		<li> at your browser!</font>
	</ul>
    <p>
  <li> <b>Research Notes</b>
    <p>
	<ul>
		<li> <font color="#eeee00">Coming soon
		<li> at your browser!</font>
	</ul>
</ul>

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

<!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><A HREF="http://www.cs.cornell.edu/Info/Projects/NuPrl/index.html"> <!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><IMG SRC="http://www.cs.cornell.edu/Info/Projects/NuPrl/icons/index.gif">
 Return to Main Index </A> <P>

<ADDRESS> Nuprl Project / [e-mail] </ADDRESS>