Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization  by O'Leary, John, Miriam Leeser, Jason Hickey, and Mark Aagaard, Theorem Provers in Circuit Design, Theory Practice and Experience (TPCD '94), Springer-Verlag, 1994.

           Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification  by Aagaard, Mark, and Miriam Leeser, Proceedings of Computer Aided Verification: Proceedings of the Fourth International Workshop (CAV'92), G. von Bochmann and D. Probst (eds.), pp. 69-81, Springer-Verlag, 1993.

           The Semantics of Reflected Proof  by Allen, Stuart F., Robert L. Constable, Douglas J. Howe, and William Aitken, Proceedings of Fifth IEEE Symposium on Logic in Computer Science, pp. 95-197, 1990.

            An Abstract Semantics for Atoms in Nuprl  by Allen, Stuart F., Cornell Tech Report TR2006-2032, 2006.

           Abstract Identifiers and Textual Reference  by Allen, Stuart F., Cornell University Technical Report 2002-1885, 2002.

           Abstract Identifiers, Intertextual Reference and a Computational Basis for Recordkeeping  by Allen, Stuart F., First Monday, vol. 9, no. 2, 2004.

           Enabling Large Scale Coherency Among Mathematical Texts  by Allen, Stuart F., and Robert L. Constable, Cornell University Technical Report, 2006-2014, 2006.

           Expressing and Implementing the Computational Content Implicit in Smullyan's Account of Boolean Valuations  by Allen, Stuart F., Robert L. Constable, and Matthew Fluet, Cornell University Technical Report 2004-1933, 2004.

           FDL: A Prototype Formal Digital Library  by Allen, Stuart F., Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, and Lori Lorigo, Cornell University Technical Report 2004-1941, 2002.

           From dy/dx to []P: A Matter of Notation  by Allen, Stuart F., Proceedings of Conference on User Interfaces for Theorem Provers, 1998.

           Implementing Mathematics with the Nuprl Development System  by Constable, Robert L., Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith, Prentice-Hall:NJ, 1986.

           Innovations in Computational Type Theory using Nuprl  by Allen, Stuart F., Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, and Evan Moran, Journal of Applied Logic, Volume 4, Issue 4, December 2006, Pages 428-469, 2006.

       Logical Aspects of Digital Mathematics Libraries (extended abstract)  by Allen, Stuart F., James L. Caldwell, and Robert L. Constable, Proceedings of First International Workshop on Mathematical Knowledge Management (MKM'01), RISC, A-4232 Schloss Hagenberg, Austria, 2001.

       A Non-Type-Theoretic Definition of Martin-Lof's Types  by Allen, Stuart F., Proceedings of Second IEEE Symposium on Logic in Computer Science, pp. 215-224, (also Cornell TR 87-832), 1987.

       A Non-Type-Theoretic Semantics for Type-Theoretic Language  by Allen, Stuart F., Cornell University Ph.D. Thesis, 1987.

       The Nuprl Open Logical Environment  by Allen, Stuart F., Robert L. Constable, Richard Eaton, Christoph Kreitz, and Lori Lorigo, Proceedings of 17th International Conference on Automated Deduction, LNAI 1831, pp. 170-176, Springer-Verlag, 2000.

       Practical Reflection in Nuprl  by Barzilay, Eli, Stuart F. Allen, and Robert L. Constable, Proceedings of 18th IEEE Symposium on Logic in Computer Science, P. Kolaitis (ed.), 2003.

       Reflecting Higher-Order Abstract Syntax in Nuprl  by Barzilay, Eli, and Stuart F. Allen, Track B Proceedings of 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs '02), pp. 23-32, 2002.

       Reflecting the Open-Ended Computation System of Constructive Type Theory  by Constable, Robert L., Stuart F. Allen, and Douglas J. Howe, Logic Algebra and Computation (NATO ASI Series), H. Schwichtenberg (ed.), vol. F79, 1990.

       The Semantics of Reflected Proof  by Allen, Stuart F., Robert L. Constable, Douglas J. Howe, and William Aitken, Proceedings of Fifth IEEE Symposium on Logic in Computer Science, pp. 95-197, 1990.

       Using Formal Reference to Enhance Authority and Integrity in Online Mathematical Texts  by Allen, Stuart F., Robert L. Constable, and Lori Lorigo, To appear in Journal of Electronic Publishing, February, 2006.

           MetaPRL -- A Modular Logical Environment  by Hickey, Jason, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, and Lori Lorigo, Proceedings of 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'03), D. Basin and B. Wolff (eds.), LNCS 2758, pp. 287-303, Springer-Verlag, 2003.

            Implementing Reflection in Nuprl  by Barzilay, Eli, Cornell University Ph.D. Thesis, 2006.

           MetaPRL -- A Modular Logical Environment  by Hickey, Jason, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, and Lori Lorigo, Proceedings of 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'03), D. Basin and B. Wolff (eds.), LNCS 2758, pp. 287-303, Springer-Verlag, 2003.

           Practical Reflection in Nuprl  by Barzilay, Eli, Stuart F. Allen, and Robert L. Constable, Proceedings of 18th IEEE Symposium on Logic in Computer Science, P. Kolaitis (ed.), 2003.

           Quotation and Reflection in Nuprl and Scheme  by Barzilay, Eli, Cornell University Technical Report 2001-1832, 2001.

           Reflecting Higher-Order Abstract Syntax in Nuprl  by Barzilay, Eli, and Stuart F. Allen, Track B Proceedings of 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs '02), pp. 23-32, 2002.

           Verbalization of High-Level Formal Proofs  by Holland-Minkley, Amanda, Regina Barzilay, and Robert L. Constable, Proceedings of Sixteenth National Conference on Artificial Intelligence, pp. 277-284, 1999.

           Building Problem Solving Environments in Constructive Type Theory  by Basin, David A., Cornell University Ph.D. Thesis, 1990.

           Building Theories in Nuprl  by Basin, David A., Proceedings of Logic at Botik '89, LNCS 363, pp. 12-25, Springer-Verlag:Pereslavl-Zalessky, USSR, (also Cornell Technical Report 88-932), 1989.

           An Environment for Automated Reasoning About Partial Functions  by Basin, David A., Proceedings of Ninth International Conference on Automated Deduction, LNCS 310, pp. 101-110, Springer-Verlag:NY, (also Cornell TR 87-884), 1988.

           Extracting Circuits from Constructive Proofs  by Basin, David A., Department of Artificial Intelligence, Edinburgh, Research Paper 533, (also appeared in Proceedings of the IFIP-IEEE International Workshop on Formal Methods in VLSI Design), 1991.

           Formally Verified Synthesis of Combinational Circuits  by Basin, David A., Geoffrey Brown, and Miriam Leeser, Integration: The International Journal of VLSI Design, vol. 11, pp. 235-250, 1991.

           Metalogical Frameworks  by Basin, David A., and Robert L. Constable, Proceedings of Second Annual Workshop on Logical Frameworks, (also Cornell Technical Report 91-1235), 1991.

           Some Normalization Properties of Martin-Lof's Type Theory and Applications  by Basin, David A., and Douglas J. Howe, International Conference on Theoretical Aspects of Computer Software (TACS '91), LNCS 526, pp. 475-494, Springer-Verlag, 1991.

           Verification of Combinational Logic in Nuprl  by Basin, David A., and Peter Del Vecchio, Hardware Specification Verification and Synthesis: Mathematical Aspects, LNCS 408, pp. 333-357, Springer-Verlag, (also Cornell TR 89-1018), 1989.

           A Logic for Correct Program Development  by Bates, Joseph L., Revision of Cornell University Ph.D. Thesis submitted August 1979, 1981.

           Proofs as Programs  by Bates, Joseph L., and Robert L. Constable, ACM Transactions on Programming Languages and Systems, vol. 7, no. 1, pp. 53-71, (also Cornell University Technical Report 82-530), 1985.

           Writing Programs That Construct Proofs  by Constable, Robert L., Todd B. Knoblock, and Joseph L. Bates, Journal of Automated Reasoning, vol. 1, no. 3, pp. 285-326, 1984.

           Automated Complexity Analysis of Nuprl Extracted Programs  by Benzinger, Ralph, Journal of Functional Programming, vol. 11, no.1, pp. 3-31, 2001.

           Automated Computational Complexity Analysis  by Benzinger, Ralph, Cornell University Ph.D. Thesis, 2001.

           A Causal Logic of Events in Formalized Computational Type Theory  by Bickford, Mark, and Robert L. Constable, Cornell University Technical Report, 2005.

           Component Specification Using Event Classes  by Bickford, Mark, Lecture Notes in Computer Science, Vol. 5582, pp. 140-155., 2009.

           An Experiment in Formal Design Using Meta-Properties  by Bickford, Mark, Christoph Kreitz, Robbert van Renesse, and Robert L. Constable, Proceedings of DARPA Information Survivability Conference and Exposition II (DISCEX II), pp. 100-107, 2001.

           FDL: A Prototype Formal Digital Library  by Allen, Stuart F., Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, and Lori Lorigo, Cornell University Technical Report 2004-1941, 2002.

           Formal Foundations of Computer Security  by Constable, Robert L., and Mark Bickford, NATO Science for Peace and Security Series, D: Information and Communication Security, Vol. 14, pages 29 - 52, 2008., 2008.

           Formalizing chain replication  by Guaspari, David, and Mark Bickford, , 2006.

           Formally Verifying Hybrid Protocols with the Nuprl Logical Programming Environment  by Bickford, Mark, Christoph Kreitz, and Robbert van Renesse, Cornell University Technical Report 2001-1839, 2001.

           Innovations in Computational Type Theory using Nuprl  by Allen, Stuart F., Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, and Evan Moran, Journal of Applied Logic, Volume 4, Issue 4, December 2006, Pages 428-469, 2006.

           Knowledge-Based Synthesis of Distributed Systems Using Event Structures  by Bickford, Mark, Robert L. Constable, Joseph Y. Halpern, and Sabina Petride, Cornell University Technical Report 2004-1927, 2004.

       Knowledge-based synthesis of distributed systems using event structures.  by Bickford, Mark, Robert L. Constable, Joseph Y. Halpern, and Sabina Petride, In Franz Baader and Andreo Voronsky, editors, Logic for Programming, Artificial Intelligence, and Reasoning, volume 3452 of Lecture Notes in Computer Science, pages 449-465, 2005.

       A Logic of Events  by Bickford, Mark, and Robert L. Constable, Cornell University Technical Report 2003-1893, 2003.

       A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics  by Kleinberg, Jon, Mark Bickford, Robert L. Constable, Richard Eaton, and Christoph Kreitz, Cornell University Technical Report 2003-1889, 2003.

       An Object-Oriented Approach to Verifying Group Communication Systems  by Bickford, Mark, and Jason Hickey, Proceedings of CADE-16, 1999.

       A Programming Logic for Distributed Systems  by Bickford, Mark, and David Guaspari, ATC-NY Technical Report, 2005.

       Protocol Switching: Exploiting Meta-Properties  by Liu, Xiaoming, Robbert van Renesse, Mark Bickford, Christoph Kreitz, and Robert L. Constable, ProceedingsInternational Workshop on Applied Reliable Group Communication (WARGC'01), IEEE Computer Society Press, 2001.

       Proving Hybrid Protocols Correct  by Bickford, Mark, Christoph Kreitz, Robbert van Renesse, and Xiaoming Liu, Proceedings of 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'01), R. Boulton and P. Jackson (eds.), LNCS 2152, pp. 105-120, Springer-Verlag, 2001.

       Unguessable Atoms: A Logical Foundation for Security  by Bickford, Mark, , 2006.

       Unguessable Atoms: A Logical Foundation for Security  by Bickford, Mark, Verified Software: Theories, Tools, Experiments, Second International Conference, VSTTE 2008 Toronto, Canada, pp 30 - 53, 2008.

           Building Reliable, High-Performance Communication Systems from Components  by Liu, Xiaoming, Christoph Kreitz, Robbert van Renesse, Jason Hickey, Mark Hayden, Kenneth Birman, and Robert L. Constable, Proceedings of 17th ACM Symposium on Operating System Principles (SOSP'99), Operating Systems Review, vol. 34, no. 5, pp. 80-92, 1999.

           The Horus and Ensemble Projects: Accomplishments and Limitations  by Birman, Kenneth, Robert L. Constable, Mark Hayden, Jason Hickey, Christoph Kreitz, Robbert van Renesse, Ohad Rodeh, and Werner Vogels, Proceedings of DARPA Information Survivability Conference and Exhibition (DISCEX '00), 2000.

           Implementing Mathematics with the Nuprl Development System  by Constable, Robert L., Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith, Prentice-Hall:NJ, 1986.

           Formally Verified Synthesis of Combinational Circuits  by Basin, David A., Geoffrey Brown, and Miriam Leeser, Integration: The International Journal of VLSI Design, vol. 11, pp. 235-250, 1991.

           The Oyster-Clam System  by Bundy, Alan, Frank Van Harmelen, Christian Horn, and Alan Smaill, Proceedings of 10th International Conference on Automated Design, LNAI 449, M. E. Stickel (ed.), pp. 647-648, Springer-Verlag, 1990.

           Classical Propositional Decidability via Nuprl Proof Extraction  by Caldwell, James L., Proceedings of 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs '98), J. Grundy and M. Newey (eds.), LNCS 1479, pp. 105-122, Springer-Verlag, 1998.

           Classical Tools for Constructive Proof Search  by Caldwell, James L., and Judith Underwood, Proceedings of CADE-13 Workshop on Proof Search in Type-Theoretic Languages, D. Galmiche (ed.), Rutgers:NJ, 1996.

           Decidability Extracted: Synthesizing "Correct-by-Construction" Decision Procedures from Constructive Proofs  by Caldwell, James L., Cornell University Ph.D Thesis, 1998.

           Extracting Propositional Decidability: A Proof of Propositional Decidability in Constructive Type Theory and its Extracted Program  by Caldwell, James L., Unpublished manuscript, 1997.

           Intuitionistic Tableau Extracted  by Caldwell, James L., Proceedings of International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX '99), LNAI 1617, pp. 82-96, Springer-Verlag, 1999.

           Logical Aspects of Digital Mathematics Libraries (extended abstract)  by Allen, Stuart F., James L. Caldwell, and Robert L. Constable, Proceedings of First International Workshop on Mathematical Knowledge Management (MKM'01), RISC, A-4232 Schloss Hagenberg, Austria, 2001.

           Moving Proofs-as-Programs into Practice  by Caldwell, James L., Proceedings of 12th IEEE International Conference Automated Software Engineering (ASE'97), 1997.

           Search Algorithms in Type Theory  by Caldwell, James L., Ian Gent, and Judith Underwood, Theoretical Computer Science, vol. 232, nos. 1-2, pp. 55-90, 2000.

           Reversal-Bounded Computations  by Chan, Tat-hung, Cornell University Ph.D. Thesis, 1980.

           Tactic-Based Theorem Proving and Knowledge-Based Forward Chaining: An Experiment with Nuprl and Ontic  by Chen, Wilfred Z., Proceedings of 11th International Conference on Automated Deduction, D. Kapur (ed.), LNCS 607, pp. 552-566, Springer-Verlag, (also Cornell Technical Report 92-1276), 1992.

           Collaborative Mathematics Environments  by Constable, Robert L., Paul Chew, Keshav Pingali, Steve Vavasis, and Richard Zippel, Unpublished manuscript, Cornell University, 1996.

           Implementing Mathematics with the Nuprl Development System  by Constable, Robert L., Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith, Prentice-Hall:NJ, 1986.

           Type-Theoretic Models of Concurrency  by Cleaveland, Walter Rance, Cornell University Ph.D. Thesis, 1987.

           Assigning Meaning to Proofs: A Semantic Basis for Problem Solving Environments  by Constable, Robert L., Constructive Methods of Computing Science (NATO ASI Series), M. Broy (ed.), vol. F55, pp. 63-91, 1989.

           Building Reliable, High-Performance Communication Systems from Components  by Liu, Xiaoming, Christoph Kreitz, Robbert van Renesse, Jason Hickey, Mark Hayden, Kenneth Birman, and Robert L. Constable, Proceedings of 17th ACM Symposium on Operating System Principles (SOSP'99), Operating Systems Review, vol. 34, no. 5, pp. 80-92, 1999.

           A Causal Logic of Events in Formalized Computational Type Theory  by Bickford, Mark, and Robert L. Constable, Cornell University Technical Report, 2005.

           Collaborative Mathematics Environments  by Constable, Robert L., Paul Chew, Keshav Pingali, Steve Vavasis, and Richard Zippel, Unpublished manuscript, Cornell University, 1996.

           Computational Complexity and Induction for Partial Computable Functions in Type Theory  by Constable, Robert L., and Karl Crary, Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, W. Sieg, R. Sommer, and C. Talcott (eds.), pp. 166-183, Association for Symbolic Logic, 2002.

           Computational Foundations of Basic Recursive Function Theory  by Constable, Robert L., and Scott F. Smith, Proceedings of Third IEEE Symposium on Logic in Computer Science, pp. 360-371, (also Cornell Technical Report 88-904), 1988.

           Computational Type Theory -- Extended Version  by Constable, Robert L., Cornell University Tech Report Ref Number 11513, 2008.

           Constructive Mathematics and Automatic Program Writers  by Constable, Robert L., Proceedings of IFIP Congress, pp. 229-233, 1971.

           Constructive Mathematics as a Programming Logic I: Some Principles of Theory  by Constable, Robert L., Annals of Mathematics, vol. 24, Elsevier Science Publishers BV: North-Holland, (also Cornell Technical Report 83-554), 1985.

       Creating and Evaluating Interactive Formal Courseware for Mathematics and Computing  by Constable, Robert L., Unpublished manuscript, Cornell University, 1996.

       Effectively Nonblocking Concensus Procedures Can Execute Forever - a Constructive Version of FLP  by Constable, Robert L., Cornell University Tech Report Ref Number 11512, 2008.

       Enabling Large Scale Coherency Among Mathematical Texts  by Allen, Stuart F., and Robert L. Constable, Cornell University Technical Report, 2006-2014, 2006.

       Experience Using Type Theory as a Foundation for Computer Science Circa 1985-1995  by Constable, Robert L., Unpublished manuscript, Cornell University, 1996.

       An Experiment in Formal Design Using Meta-Properties  by Bickford, Mark, Christoph Kreitz, Robbert van Renesse, and Robert L. Constable, Proceedings of DARPA Information Survivability Conference and Exposition II (DISCEX II), pp. 100-107, 2001.

       Exporting and Reflecting Abstract Meta-mathematics  by Constable, Robert L., Proceedings of 12th International Conference on Automated Deduction, A. Bundy (ed.), LNAI 814, p 529, Springer-Verlag, 1994.

       Expressing and Implementing the Computational Content Implicit in Smullyan's Account of Boolean Valuations  by Allen, Stuart F., Robert L. Constable, and Matthew Fluet, Cornell University Technical Report 2004-1933, 2004.

       Expressing Computational Complexity in Constructive Type Theory  by Constable, Robert L., Proceedings of International Workshop on Logic and Computational Complexity (LCC'94), D. Leivant (ed.), LNCS 960, pp. 131-144, Springer-Verlag, 1995.

       Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics  by Constable, Robert L., and Wojciech Moczydlowski, , 2006.

       Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus  by Moczydlowski, Wojciech, and Robert L. Constable, Cornell University Technical Report 2006-2061. To appear in Proceedings of Symposium on Logical Foundations of Computer Science 2007, 2007.

       FDL: A Prototype Formal Digital Library  by Allen, Stuart F., Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, and Lori Lorigo, Cornell University Technical Report 2004-1941, 2002.

       Finding Computational Content from Classical Proofs  by Constable, Robert L., and Chetan Murthy, Logical Frameworks, G. Huet and G. Plotkin (eds.), pp. 341-362, Cambridge University Press, 1991.

       Formal Foundations of Computer Security  by Constable, Robert L., and Mark Bickford, NATO Science for Peace and Security Series, D: Information and Communication Security, Vol. 14, pages 29 - 52, 2008., 2008.

       Formal Theories and Software Systems: Fundamental Connections Between Computer Science and Logic  by Constable, Robert L., Future Tendencies in Computer Science: Control and Applied Mathematics, A. Bensoussan and J.-P. Verjus (eds.), LNCS 653, pp. 105-127, Springer-Verlag, 1992.

       Formalized Metareasoning in Type Theory  by Knoblock, Todd B., and Robert L. Constable, Proceedings of First IEEE Symposium on Logic in Computer Science, pp. 237-248, 1986.

       Formalizing Automata II: Decidable Properties  by Constable, Robert L., and Pavel Naumov, Unpublished manuscript, Cornell University, 1996.

       Formalizing Automata Theory I: Finite Automata  by Constable, Robert L., Paul B. Jackson, Pavel Naumov, and Juan Uribe, Unpublished manuscript, Cornell University, 1996.

       A Graph-Based Approach towards Discerning Inherent Structures in a Digital Library of Formal Mathematics.  by Lorigo, Lori, Jon Kleinberg, Richard Eaton, and Robert L. Constable, International Conference on Mathematical Knowledge Management, Lecture Notes in Computer Science, Springer-Verlag, 2004.

       The Horus and Ensemble Projects: Accomplishments and Limitations  by Birman, Kenneth, Robert L. Constable, Mark Hayden, Jason Hickey, Christoph Kreitz, Robbert van Renesse, Ohad Rodeh, and Werner Vogels, Proceedings of DARPA Information Survivability Conference and Exhibition (DISCEX '00), 2000.

       Implementing Mathematics with the Nuprl Development System  by Constable, Robert L., Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith, Prentice-Hall:NJ, 1986.

       Implementing Metamathematics as an Approach to Automatic Theorem Proving  by Constable, Robert L., and Douglas J. Howe, Formal Techniques in Artificial Intelligence: A Source Book, R.B. Banerji (ed.), pp. 45-76, Elsevier Science Publishers:North-Holland, (also Cornell TR 89-982), 1990.

       Infinite Objects in Type Theory  by Mendler, Nax P., Robert L. Constable, and Prakash Panangaden, Proceedings of First IEEE Symposium on Logic in Computer Science, pp. 249-255, (also Cornell Technical Report 86-743), 1986.

       Information-Intensive Proof Technology  by Constable, Robert L., Lecture Notes for the Marktoberdorf NATO Summer School, 2003.

       Innovations in Computational Type Theory using Nuprl  by Allen, Stuart F., Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, and Evan Moran, Journal of Applied Logic, Volume 4, Issue 4, December 2006, Pages 428-469, 2006.

       Knowledge-Based Synthesis of Distributed Systems Using Event Structures  by Bickford, Mark, Robert L. Constable, Joseph Y. Halpern, and Sabina Petride, Cornell University Technical Report 2004-1927, 2004.

       Knowledge-based synthesis of distributed systems using event structures.  by Bickford, Mark, Robert L. Constable, Joseph Y. Halpern, and Sabina Petride, In Franz Baader and Andreo Voronsky, editors, Logic for Programming, Artificial Intelligence, and Reasoning, volume 3452 of Lecture Notes in Computer Science, pages 449-465, 2005.

       Lectures on: Classical Proofs as Programs  by Constable, Robert L., Constructive Methods of Computing Science (NATO ASI Series), M. Broy (ed.), 1992.

       A Logic of Events  by Bickford, Mark, and Robert L. Constable, Cornell University Technical Report 2003-1893, 2003.

       Logical Aspects of Digital Mathematics Libraries (extended abstract)  by Allen, Stuart F., James L. Caldwell, and Robert L. Constable, Proceedings of First International Workshop on Mathematical Knowledge Management (MKM'01), RISC, A-4232 Schloss Hagenberg, Austria, 2001.

       Metalevel Programming in Constructive Type Theory  by Constable, Robert L., Programming and Mathematical Method (NATO ASI Series F: Computer and Systems Sciences), M. Broy (ed.), vol. 88, pp. 45-93, Springer-Verlag, 1992.

       Metalogical Frameworks  by Basin, David A., and Robert L. Constable, Proceedings of Second Annual Workshop on Logical Frameworks, (also Cornell Technical Report 91-1235), 1991.

       Metalogical Frameworks II: Developing a Reflected Decision Procedure  by Constable, Robert L., Journal of Automated Reasoning, Volume 22, Issue 2, pp. 171-221., 1999.

       MetaPRL -- A Modular Logical Environment  by Hickey, Jason, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, and Lori Lorigo, Proceedings of 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'03), D. Basin and B. Wolff (eds.), LNCS 2758, pp. 287-303, Springer-Verlag, 2003.

       Naive Computational Type Theory  by Constable, Robert L., Proof and System-Reliability, H. Schwichtenberg and R. Steinbruggen (eds.), pp. 213-259, 2002.

       Nuprl as a General Logic  by Constable, Robert L., and Douglas J. Howe, Logic in Computer Science Academic Press, P. Odifreddi (ed.), pp. 77-90, (also Cornell Technical Report 89-1021), 1990.

       The Nuprl Open Logical Environment  by Allen, Stuart F., Robert L. Constable, Richard Eaton, Christoph Kreitz, and Lori Lorigo, Proceedings of 17th International Conference on Automated Deduction, LNAI 1831, pp. 170-176, Springer-Verlag, 2000.

       A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics  by Kleinberg, Jon, Mark Bickford, Robert L. Constable, Richard Eaton, and Christoph Kreitz, Cornell University Technical Report 2003-1889, 2003.

       Nuprl's Class Theory and Its Applications  by Constable, Robert L., and Jason Hickey, Foundations of Secure Computation, F. L. Bauer and R. Steinbruggen (eds.), pp. 91-115, IOS Press:Amsterdam, 2000.

       Partial Objects in Constructive Type Theory  by Smith, Scott F., and Robert L. Constable, Proceedings of Second IEEE Symposium on Logic in Computer Science, pp. 183-193, (also Cornell TR 87-822), 1987.

       Practical Reflection in Nuprl  by Barzilay, Eli, Stuart F. Allen, and Robert L. Constable, Proceedings of 18th IEEE Symposium on Logic in Computer Science, P. Kolaitis (ed.), 2003.

       A Programming Logic  by Constable, Robert L., and Michael J. O'Donnell, Winthrop, MA, 1978.

       Proofs as Programs  by Bates, Joseph L., and Robert L. Constable, ACM Transactions on Programming Languages and Systems, vol. 7, no. 1, pp. 53-71, (also Cornell University Technical Report 82-530), 1985.

       Protocol Switching: Exploiting Meta-Properties  by Liu, Xiaoming, Robbert van Renesse, Mark Bickford, Christoph Kreitz, and Robert L. Constable, ProceedingsInternational Workshop on Applied Reliable Group Communication (WARGC'01), IEEE Computer Society Press, 2001.

       Recent Results in Type Theory and Their Relationship to Automath  by Constable, Robert L., Thirty Five Years of Automating Mathematics, F. Kamareddine (ed.), pp. 1-11, Kluwer Academic Press, 2003.

       Recursive Definitions in Type Theory  by Constable, Robert L., and Nax P. Mendler, Proceedings of Logics of Progams Conference, pp. 61-78, (also Cornell Technical Report 85-659), 1985.

       Reflecting the Open-Ended Computation System of Constructive Type Theory  by Constable, Robert L., Stuart F. Allen, and Douglas J. Howe, Logic Algebra and Computation (NATO ASI Series), H. Schwichtenberg (ed.), vol. F79, 1990.

       Semantics of Evidence  by Constable, Robert L., Cornell University Technical Report 84-684, 1985.

       The Semantics of Reflected Proof  by Allen, Stuart F., Robert L. Constable, Douglas J. Howe, and William Aitken, Proceedings of Fifth IEEE Symposium on Logic in Computer Science, pp. 95-197, 1990.

       The Structure of Nuprl's Type Theory  by Constable, Robert L., Logic of Computation, M. Broy and H. Schwichtenberg (eds.), pp. 123-156, Springer-Verlag, 1997.

       Towards Integrated Systems for Symbolic Algebra and Formal Constructive Mathematics  by Constable, Robert L., and Paul B. Jackson, Cornell University Technical Report 2003-1893, 1994.

       Type Theory as a Foundation for Computer Science  by Constable, Robert L., Proceedings of Theoretical Aspects of Computer Software International Conference (TACS '91), LNCS 526, pp. 226-243, 1991.

       Using Formal Reference to Enhance Authority and Integrity in Online Mathematical Texts  by Allen, Stuart F., Robert L. Constable, and Lori Lorigo, To appear in Journal of Electronic Publishing, February, 2006.

       Using Reflection to Explain and Enhance Type Theory  by Constable, Robert L., Proof and Computation (NATO ASI Series F), H. Schwichtenberg (ed.), vol. 139, pp. 65-100, Springer-Verlag:Berlin, 1994.

       The Value of Automated Deduction  by Constable, Robert L., Unpublished manuscript, Cornell University, 1996.

       Verbalization of High-Level Formal Proofs  by Holland-Minkley, Amanda, Regina Barzilay, and Robert L. Constable, Proceedings of Sixteenth National Conference on Artificial Intelligence, pp. 277-284, 1999.

       Writing Programs That Construct Proofs  by Constable, Robert L., Todd B. Knoblock, and Joseph L. Bates, Journal of Automated Reasoning, vol. 1, no. 3, pp. 285-326, 1984.

           Computational Complexity and Induction for Partial Computable Functions in Type Theory  by Constable, Robert L., and Karl Crary, Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, W. Sieg, R. Sommer, and C. Talcott (eds.), pp. 166-183, Association for Symbolic Logic, 2002.

           Foundations for the Implementation of Higher-Order Subtyping  by Crary, Karl, Proceedings of 1997 ACM SIGPLAN International Conference on Functional Programming (ICFP '97), SIGPLAN Notices vol. 32, no. 8, pp. 125-135, ACM Press, 1997.

           Type-Theoretic Methodology for Practical Programming Languages  by Crary, Karl, Cornell University Ph.D. Thesis, 1998.

           Implementing Mathematics with the Nuprl Development System  by Constable, Robert L., Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith, Prentice-Hall:NJ, 1986.

           Verification of Combinational Logic in Nuprl  by Basin, David A., and Peter Del Vecchio, Hardware Specification Verification and Synthesis: Mathematical Aspects, LNCS 408, pp. 333-357, Springer-Verlag, (also Cornell TR 89-1018), 1989.

           FDL: A Prototype Formal Digital Library  by Allen, Stuart F., Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, and Lori Lorigo, Cornell University Technical Report 2004-1941, 2002.

           A Graph-Based Approach towards Discerning Inherent Structures in a Digital Library of Formal Mathematics.  by Lorigo, Lori, Jon Kleinberg, Richard Eaton, and Robert L. Constable, International Conference on Mathematical Knowledge Management, Lecture Notes in Computer Science, Springer-Verlag, 2004.

           Innovations in Computational Type Theory using Nuprl  by Allen, Stuart F., Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, and Evan Moran, Journal of Applied Logic, Volume 4, Issue 4, December 2006, Pages 428-469, 2006.

           The Nuprl Open Logical Environment  by Allen, Stuart F., Robert L. Constable, Richard Eaton, Christoph Kreitz, and Lori Lorigo, Proceedings of 17th International Conference on Automated Deduction, LNAI 1831, pp. 170-176, Springer-Verlag, 2000.

           A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics  by Kleinberg, Jon, Mark Bickford, Robert L. Constable, Richard Eaton, and Christoph Kreitz, Cornell University Technical Report 2003-1889, 2003.

           Expressing and Implementing the Computational Content Implicit in Smullyan's Account of Boolean Valuations  by Allen, Stuart F., Robert L. Constable, and Matthew Fluet, Cornell University Technical Report 2004-1933, 2004.

           Formalizing Constructive Real Analysis  by Forester, Max B., Unpublished manuscript, Cornell University, 1993.

           Search Algorithms in Type Theory  by Caldwell, James L., Ian Gent, and Judith Underwood, Theoretical Computer Science, vol. 232, nos. 1-2, pp. 55-90, 2000.

           Termination of Single-Threaded One-rule Semi-Thue Systems  by Moczydlowski, Wojciech, and Alfons Geser, Proceedings of 16th International Conference on Rewriting Techniques and Applications (RTA 2005), LNCS 3467, 338-352, Springer., 2005.

           Reflection in Constructive and Non-Constructive Automated Reasoning  by Giunchiglia, Fausto, and Alan Smaill, Meta-Programming in Logic Programming, H. Abramson and M.H. Rogers (eds.), pp. 123-140, MIT Press, 1989.

           Notational Definition and Top-down Refinement for Interactive Proof Development Systems  by Griffin, Timothy G., Cornell University Ph.D. Thesis, 1988.

           Formalizing chain replication  by Guaspari, David, and Mark Bickford, , 2006.

           A Programming Logic for Distributed Systems  by Bickford, Mark, and David Guaspari, ATC-NY Technical Report, 2005.

           Dependence Analysis Through Type Inference  by Hafizogullari, Ozan, and Christoph Kreitz, Proceedings of Sixth Workshop on Logic, Language, Information and Computation (WoLLIC'99), R. de Queiroz and W. A. Carnielli (eds.), pp. 127-138, 1999.

           Knowledge-Based Synthesis of Distributed Systems Using Event Structures  by Bickford, Mark, Robert L. Constable, Joseph Y. Halpern, and Sabina Petride, Cornell University Technical Report 2004-1927, 2004.

           Knowledge-based synthesis of distributed systems using event structures.  by Bickford, Mark, Robert L. Constable, Joseph Y. Halpern, and Sabina Petride, In Franz Baader and Andreo Voronsky, editors, Logic for Programming, Artificial Intelligence, and Reasoning, volume 3452 of Lecture Notes in Computer Science, pages 449-465, 2005.

           The Oyster-Clam System  by Bundy, Alan, Frank Van Harmelen, Christian Horn, and Alan Smaill, Proceedings of 10th International Conference on Automated Design, LNAI 449, M. E. Stickel (ed.), pp. 647-648, Springer-Verlag, 1990.

           Aspects of the Implementation of Type Theory  by Harper, Robert W., Cornell University Ph.D. Thesis, 1985.

           Implementing Mathematics with the Nuprl Development System  by Constable, Robert L., Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith, Prentice-Hall:NJ, 1986.

           Building Reliable, High-Performance Communication Systems from Components  by Liu, Xiaoming, Christoph Kreitz, Robbert van Renesse, Jason Hickey, Mark Hayden, Kenneth Birman, and Robert L. Constable, Proceedings of 17th ACM Symposium on Operating System Principles (SOSP'99), Operating Systems Review, vol. 34, no. 5, pp. 80-92, 1999.

           The Ensemble System  by Hayden, Mark, Cornell University Ph.D. Thesis, 1998.

           The Horus and Ensemble Projects: Accomplishments and Limitations  by Birman, Kenneth, Robert L. Constable, Mark Hayden, Jason Hickey, Christoph Kreitz, Robbert van Renesse, Ohad Rodeh, and Werner Vogels, Proceedings of DARPA Information Survivability Conference and Exhibition (DISCEX '00), 2000.

           A Proof Environment for the Development of Group Communication Systems  by Kreitz, Christoph, Mark Hayden, and Jason Hickey, Proceedings of 15th International Conference on Automated Deduction (CADE-15), C. and H. Kirchner (eds.), LNAI 1421, pp. 317-331, Springer-Verlag, 1998.

           Building Reliable, High-Performance Communication Systems from Components  by Liu, Xiaoming, Christoph Kreitz, Robbert van Renesse, Jason Hickey, Mark Hayden, Kenneth Birman, and Robert L. Constable, Proceedings of 17th ACM Symposium on Operating System Principles (SOSP'99), Operating Systems Review, vol. 34, no. 5, pp. 80-92, 1999.

           Fast Tactic-Based Theorem Proving  by Hickey, Jason, and Aleksey Nogin, Proceedings of 13th International Conference (TPHOLs 2000), LNCS 1869, pp. 252-266, Springer-Verlag, 2000.

           Fault-Tolerant Distributed Theorem Proving  by Hickey, Jason, Proceedings of 16th International Conference on Automated Deduction, H. Ganzinger (ed.), LNAI 1632, pp. 227-231, 1999.

           Formal Compiler Implementation in a Logical Framework  by Hickey, Jason, and Aleksey Nogin, Proceedings of MERLIN 2003, Second ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding, 2003.

           Formal Objects in Type Theory Using Very Dependent Types  by Hickey, Jason, Foundations of Object-Oriented Languages 3, 1996.

           The Horus and Ensemble Projects: Accomplishments and Limitations  by Birman, Kenneth, Robert L. Constable, Mark Hayden, Jason Hickey, Christoph Kreitz, Robbert van Renesse, Ohad Rodeh, and Werner Vogels, Proceedings of DARPA Information Survivability Conference and Exhibition (DISCEX '00), 2000.

           MetaPRL -- A Modular Logical Environment  by Hickey, Jason, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, and Lori Lorigo, Proceedings of 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'03), D. Basin and B. Wolff (eds.), LNCS 2758, pp. 287-303, Springer-Verlag, 2003.

           The MetaPRL Logical Programming Environment  by Hickey, Jason, Cornell University Ph.D. Thesis, 2001.

           Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization  by O'Leary, John, Miriam Leeser, Jason Hickey, and Mark Aagaard, Theorem Provers in Circuit Design, Theory Practice and Experience (TPCD '94), Springer-Verlag, 1994.

       Nuprl-Light: An Implementation Framework for Higher-Order Logics  by Hickey, Jason, Proceedings of 14th International Conference on Automated Deduction, W. McCune (ed.), LNAI 1249, pp. 395-399, Springer-Verlag, 1997.

       Nuprl's Class Theory and Its Applications  by Constable, Robert L., and Jason Hickey, Foundations of Secure Computation, F. L. Bauer and R. Steinbruggen (eds.), pp. 91-115, IOS Press:Amsterdam, 2000.

       An Object-Oriented Approach to Verifying Group Communication Systems  by Bickford, Mark, and Jason Hickey, Proceedings of CADE-16, 1999.

       A Proof Environment for the Development of Group Communication Systems  by Kreitz, Christoph, Mark Hayden, and Jason Hickey, Proceedings of 15th International Conference on Automated Deduction (CADE-15), C. and H. Kirchner (eds.), LNAI 1421, pp. 317-331, Springer-Verlag, 1998.

       A Semantics of Objects in Type Theory  by Hickey, Jason, Unpublished manuscript, Cornell University, 1997.

       Specifications and Proofs for Ensemble Layers  by Hickey, Jason, Nancy Lynch, and Robbert van Renesse, Proceedings of Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '99), R. Cleaveland (ed.), LNCS 1579, pp. 119-133, Springer-Verlag, 1999.

           Planning Proof Content for Communicating Induction  by Holland-Minkley, Amanda, Proceedings of Second International Natural Language Generation Conference, pp. 167-172, 2002.

           Verbalization of High-Level Formal Proofs  by Holland-Minkley, Amanda, Regina Barzilay, and Robert L. Constable, Proceedings of Sixteenth National Conference on Artificial Intelligence, pp. 277-284, 1999.

           The Nuprl Proof Development System  by Horn, Christian, Deptartment of Artificial Intelligence Edinburgh Working Paper 214, 1988.

           The Oyster-Clam System  by Bundy, Alan, Frank Van Harmelen, Christian Horn, and Alan Smaill, Proceedings of 10th International Conference on Automated Design, LNAI 449, M. E. Stickel (ed.), pp. 647-648, Springer-Verlag, 1990.

           Automating Reasoning in an Implementation of Constructive Type Theory  by Howe, Douglas J., Cornell University Ph.D. Thesis, 1988.

           The Computational Behaviour of Girard's Paradox  by Howe, Douglas J., Proceedings of Second IEEE Symposium on Logic in Computer Science, pp. 205-214, (also Cornell TR 87-820), 1987.

           Computational Metatheory in Nuprl  by Howe, Douglas J., Proceedings of Ninth International Conference on Automated Deduction, E. Lusk and R. Overbeek (eds.), LNCS 310, pp. 238-257, Springer-Verlag:NY, (also Cornell TR 88-899), 1988.

           Equality in Lazy Computation Systems  by Howe, Douglas J., Proceedings of Fourth IEEE Symposium on Logic in Computer Science, pp. 198-203, 1989.

           Implementing Mathematics with the Nuprl Development System  by Constable, Robert L., Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith, Prentice-Hall:NJ, 1986.

           Implementing Metamathematics as an Approach to Automatic Theorem Proving  by Constable, Robert L., and Douglas J. Howe, Formal Techniques in Artificial Intelligence: A Source Book, R.B. Banerji (ed.), pp. 45-76, Elsevier Science Publishers:North-Holland, (also Cornell TR 89-982), 1990.

           Implementing Number Theory: An Experiment with Nuprl  by Howe, Douglas J., Proceedings of Eighth International Conference on Automated Deduction, LNCS 230, pp. 404-415, (also Cornell TR 86-752), 1987.

           Importing Mathematics from HOL into Nuprl  by Howe, Douglas J., Theorem Proving in Higher Order Logics, J. von Wright, J. Grundy, and J. Harrison (eds.), LNCS 1125, pp. 267-282, Springer-Verlag:Berlin, 1996.

           Nuprl as a General Logic  by Constable, Robert L., and Douglas J. Howe, Logic in Computer Science Academic Press, P. Odifreddi (ed.), pp. 77-90, (also Cornell Technical Report 89-1021), 1990.

       An Operational Approach to Combining Classical Set Theory and Functional Programming Languages  by Howe, Douglas J., and Scott D. Stoller, Proceedings of International Symposium on Theoretical Aspects of Computer Software (TACS '94), M. Hagiya and J. Mitchell (eds.), LNCS 789, pp. 36-55, Springer-Verlag, 1994.

       Reasoning About Functional Programs in Nuprl  by Howe, Douglas J., Functional Programming Concurrency Simulation and Automated Reasoning, LNCS, 1993.

       Reflecting the Open-Ended Computation System of Constructive Type Theory  by Constable, Robert L., Stuart F. Allen, and Douglas J. Howe, Logic Algebra and Computation (NATO ASI Series), H. Schwichtenberg (ed.), vol. F79, 1990.

       Semantic Foundations for Embedding HOL in Nuprl  by Howe, Douglas J., Algebraic Methodology and Software Technology, M. Wirsing and M. Nivat (eds.), LNCS 1101, pp. 85-101, Springer-Verlag:Berlin, 1996.

       The Semantics of Reflected Proof  by Allen, Stuart F., Robert L. Constable, Douglas J. Howe, and William Aitken, Proceedings of Fifth IEEE Symposium on Logic in Computer Science, pp. 95-197, 1990.

       A Simple Type Theory for Reasoning About Functional Programs  by Howe, Douglas J., Computer Science Department Cornell University (Pre-print), 1992.

       Some Normalization Properties of Martin-Lof's Type Theory and Applications  by Basin, David A., and Douglas J. Howe, International Conference on Theoretical Aspects of Computer Software (TACS '91), LNCS 526, pp. 475-494, Springer-Verlag, 1991.

           Developing a Toolkit for Floating-Point Hardware in the Nuprl Proof Development System  by Jackson, Paul B., Proceedings of Advanced Research Workshop on Correct Hardware Design Methodologies, pp. 401-419, Elsevier, 1991.

           Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra  by Jackson, Paul B., Cornell University Ph.D. Thesis, 1995.

           Exploring Abstract Algebra in Constructive Type Theory  by Jackson, Paul B., Proceedings of 12th Conference on Automated Deduction, A. Bundy (ed.), Springer-Verlag:NY, 1994.

           Formalizing Automata Theory I: Finite Automata  by Constable, Robert L., Paul B. Jackson, Pavel Naumov, and Juan Uribe, Unpublished manuscript, Cornell University, 1996.

           Logic-Based Knowledge Representation  by Jackson, Paul B., MIT Press:Cambridge MA, 1989.

           Nuprl and Its Use in Circuit Design  by Jackson, Paul B., Theorem Provers in Circuit Design, Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, V. Stavridou, T. Melham, and R. Boute (eds.), pp. 311-336, 1992.

           The Nuprl Proof Development System, Version 4.2 Reference Manual and User's Guide  by Jackson, Paul B., Unpublished manuscript, Cornell University, 1996.

           Towards Integrated Systems for Symbolic Algebra and Formal Constructive Mathematics  by Constable, Robert L., and Paul B. Jackson, Cornell University Technical Report 2003-1893, 1994.

           A Graph-Based Approach towards Discerning Inherent Structures in a Digital Library of Formal Mathematics.  by Lorigo, Lori, Jon Kleinberg, Richard Eaton, and Robert L. Constable, International Conference on Mathematical Knowledge Management, Lecture Notes in Computer Science, Springer-Verlag, 2004.

           A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics  by Kleinberg, Jon, Mark Bickford, Robert L. Constable, Richard Eaton, and Christoph Kreitz, Cornell University Technical Report 2003-1889, 2003.

           Formalized Metareasoning in Type Theory  by Knoblock, Todd B., and Robert L. Constable, Proceedings of First IEEE Symposium on Logic in Computer Science, pp. 237-248, 1986.

           Implementing Mathematics with the Nuprl Development System  by Constable, Robert L., Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith, Prentice-Hall:NJ, 1986.

           Metamathematical Extensibility in Type Theory  by Knoblock, Todd B., Cornell University Ph.D. Thesis, 1987.

           Writing Programs That Construct Proofs  by Constable, Robert L., Todd B. Knoblock, and Joseph L. Bates, Journal of Automated Reasoning, vol. 1, no. 3, pp. 285-326, 1984.

           Dependent Intersection: A New Way of Defining Records in Type Theory  by Kopylov, Alexei, Proceedings of 18th Annual IEEE Symposium on Logic in Computer Science, pp. 86-95, 2003.

           Markov’s Principle For Propositional Type Theory  by Nogin, Aleksey, and Alexei Kopylov, Computer Science Logic, 2001, LNCS 2142, publisher Springer-Verlag, Berlin, pages 570-584, 2001.

           Type Theoretical Foundations for Data Structures, Classes, and Objects  by Kopylov, Alexei, Cornell University Ph.D. Thesis, 2004.

           Automating Proofs in Category Theory  by Kozen, Dexter, Christoph Kreitz, and Eva Richter, International Conference - IJCAR 2006, LNAI 4130, pp. 392-407, Springer Verlag, 2006., 2006.

           Automated Fast-Track Reconfiguration of Group Communication Systems  by Kreitz, Christoph, Proceedings of Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99), R. Cleaveland (ed.), LNCS 1579, pp. 104-118, Springer-Verlag, 1999.

           Automating Inductive Specification Proofs  by Pientka, Brigitte, and Christoph Kreitz, Fundamenta Informatica, vol. 39, nos. 1-2, pp. 189-208, 1999.

           Automating Proofs in Category Theory  by Kozen, Dexter, Christoph Kreitz, and Eva Richter, International Conference - IJCAR 2006, LNAI 4130, pp. 392-407, Springer Verlag, 2006., 2006.

           Building Reliable, High-Performance Communication Systems from Components  by Liu, Xiaoming, Christoph Kreitz, Robbert van Renesse, Jason Hickey, Mark Hayden, Kenneth Birman, and Robert L. Constable, Proceedings of 17th ACM Symposium on Operating System Principles (SOSP'99), Operating Systems Review, vol. 34, no. 5, pp. 80-92, 1999.

           Connection-Based Theorem Proving in Classical and Non-Classical Logics  by Kreitz, Christoph, and Jens Otten, Journal of Universal Computer Science, vol. 5, no. 3, pp. 88-112, Springer-Verlag, 1999.

           Connection-Driven Inductive Theorem Proving  by Kreitz, Christoph, and Brigitte Pientka, Studia Logica, vol. 69, no. 2, pp. 293-326, 2001.

           Constructive Automata Theory Implemented with the Nuprl Proof Development System  by Kreitz, Christoph, Cornell University Technical Report 86-779, 1986.

           Dependence Analysis Through Type Inference  by Hafizogullari, Ozan, and Christoph Kreitz, Proceedings of Sixth Workshop on Logic, Language, Information and Computation (WoLLIC'99), R. de Queiroz and W. A. Carnielli (eds.), pp. 127-138, 1999.

           An Experiment in Formal Design Using Meta-Properties  by Bickford, Mark, Christoph Kreitz, Robbert van Renesse, and Robert L. Constable, Proceedings of DARPA Information Survivability Conference and Exposition II (DISCEX II), pp. 100-107, 2001.

       The FDL Navigator: Browsing and Manipulating Formal Content  by Kreitz, Christoph, Unpublished manuscript, Cornell University, 2003.

       FDL: A Prototype Formal Digital Library  by Allen, Stuart F., Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, and Lori Lorigo, Cornell University Technical Report 2004-1941, 2002.

       Formal Reasoning About Communication Systems I: Embedding ML in Type Theory  by Kreitz, Christoph, Cornell University Technical Report 97-1637, 1997.

       Formal Reasoning About Communication Systems II: Automated Fast-Track Reconfiguration  by Kreitz, Christoph, Cornell University Technical Report 98-1707, 1998.

       Formally Verifying Hybrid Protocols with the Nuprl Logical Programming Environment  by Bickford, Mark, Christoph Kreitz, and Robbert van Renesse, Cornell University Technical Report 2001-1839, 2001.

       The Horus and Ensemble Projects: Accomplishments and Limitations  by Birman, Kenneth, Robert L. Constable, Mark Hayden, Jason Hickey, Christoph Kreitz, Robbert van Renesse, Ohad Rodeh, and Werner Vogels, Proceedings of DARPA Information Survivability Conference and Exhibition (DISCEX '00), 2000.

       Innovations in Computational Type Theory using Nuprl  by Allen, Stuart F., Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, and Evan Moran, Journal of Applied Logic, Volume 4, Issue 4, December 2006, Pages 428-469, 2006.

       Instantiation of Existentially Quantified Variables in Inductive Specification Proofs  by Pientka, Brigitte, and Christoph Kreitz, Proceedings of Fourth International Conference on Artificial Intelligence and Symbolic Computation (AISC'98), J. Calmet and J. Plaza (eds.), LNAI 1476, pp. 247-258, Springer-Verlag, 1998.

       JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants  by Schmitt, Stephan, Lori Lorigo, Christoph Kreitz, and Aleksey Nogin, International Joint Conference on Automated Reasoning, (IJCAR 2001), R. Gore, A. Leitsch, and T. Nipkow (eds.), LNAI 2083, pp. 421-426, Springer-Verlag, 2001.

       A Matrix Characterization for MELL  by Mantel, Heiko, and Christoph Kreitz, Proceedings of Sixth European Workshop on Logics in Artificial Intelligence (JELIA'98), J. Dix, F. L. Del Cerro, and U. Furbach (eds.), LNAI 1489, pp. 169-183, Springer-Verlag, 1998.

       Matrix-Based Constructive Theorem Proving  by Kreitz, Christoph, Jens Otten, Stephan Schmitt, and Brigitte Pientka, Intellectics and Computational Logic: Papers in Honor of Wolfgang Bibel, S. Hölldobler (ed.), pp. 189-205, Kluwer, 2000.

       Matrix-Based Inductive Theorem Proving  by Kreitz, Christoph, and Brigitte Pientka, International Conference TABLEAUX-2000, R. Dyckhoff (ed.), LNAI 1847, pp. 294-308, Springer-Verlag, 2000.

       Meta-Synthesis: Deriving Programs That Develop Programs  by Kreitz, Christoph, Unpublished manuscript, Technical University of Darmstadt, 1992.

       The Nuprl Open Logical Environment  by Allen, Stuart F., Robert L. Constable, Richard Eaton, Christoph Kreitz, and Lori Lorigo, Proceedings of 17th International Conference on Automated Deduction, LNAI 1831, pp. 170-176, Springer-Verlag, 2000.

       A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics  by Kleinberg, Jon, Mark Bickford, Robert L. Constable, Richard Eaton, and Christoph Kreitz, Cornell University Technical Report 2003-1889, 2003.

       A Proof Environment for the Development of Group Communication Systems  by Kreitz, Christoph, Mark Hayden, and Jason Hickey, Proceedings of 15th International Conference on Automated Deduction (CADE-15), C. and H. Kirchner (eds.), LNAI 1421, pp. 317-331, Springer-Verlag, 1998.

       Protocol Switching: Exploiting Meta-Properties  by Liu, Xiaoming, Robbert van Renesse, Mark Bickford, Christoph Kreitz, and Robert L. Constable, ProceedingsInternational Workshop on Applied Reliable Group Communication (WARGC'01), IEEE Computer Society Press, 2001.

       Proving Hybrid Protocols Correct  by Bickford, Mark, Christoph Kreitz, Robbert van Renesse, and Xiaoming Liu, Proceedings of 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'01), R. Boulton and P. Jackson (eds.), LNCS 2152, pp. 105-120, Springer-Verlag, 2001.

       A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems  by Kreitz, Christoph, and Stephan Schmitt, Journal of Information and Computation, vol. 162, nos. 1-2, pp. 226-254, 2000.

           Formally Verified Synthesis of Combinational Circuits  by Basin, David A., Geoffrey Brown, and Miriam Leeser, Integration: The International Journal of VLSI Design, vol. 11, pp. 235-250, 1991.

           Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization  by O'Leary, John, Miriam Leeser, Jason Hickey, and Mark Aagaard, Theorem Provers in Circuit Design, Theory Practice and Experience (TPCD '94), Springer-Verlag, 1994.

           Using Nuprl for the Verification and Synthesis of Hardware  by Leeser, Miriam, Philosophical Transactions of the Royal Society London, vol. 339, pp. 49-68, 1992.

           Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification  by Aagaard, Mark, and Miriam Leeser, Proceedings of Computer Aided Verification: Proceedings of the Fourth International Workshop (CAV'92), G. von Bochmann and D. Probst (eds.), pp. 69-81, Springer-Verlag, 1993.

           Building Reliable, High-Performance Communication Systems from Components  by Liu, Xiaoming, Christoph Kreitz, Robbert van Renesse, Jason Hickey, Mark Hayden, Kenneth Birman, and Robert L. Constable, Proceedings of 17th ACM Symposium on Operating System Principles (SOSP'99), Operating Systems Review, vol. 34, no. 5, pp. 80-92, 1999.

           Protocol Switching: Exploiting Meta-Properties  by Liu, Xiaoming, Robbert van Renesse, Mark Bickford, Christoph Kreitz, and Robert L. Constable, ProceedingsInternational Workshop on Applied Reliable Group Communication (WARGC'01), IEEE Computer Society Press, 2001.

           Proving Hybrid Protocols Correct  by Bickford, Mark, Christoph Kreitz, Robbert van Renesse, and Xiaoming Liu, Proceedings of 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'01), R. Boulton and P. Jackson (eds.), LNCS 2152, pp. 105-120, Springer-Verlag, 2001.

           FDL: A Prototype Formal Digital Library  by Allen, Stuart F., Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, and Lori Lorigo, Cornell University Technical Report 2004-1941, 2002.

           A Graph-Based Approach towards Discerning Inherent Structures in a Digital Library of Formal Mathematics.  by Lorigo, Lori, Jon Kleinberg, Richard Eaton, and Robert L. Constable, International Conference on Mathematical Knowledge Management, Lecture Notes in Computer Science, Springer-Verlag, 2004.

           Information Management in the Service of Knowledge and Discovery  by Lorigo, Lori, Cornell University Ph.D. Thesis, 2006.

           Innovations in Computational Type Theory using Nuprl  by Allen, Stuart F., Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, and Evan Moran, Journal of Applied Logic, Volume 4, Issue 4, December 2006, Pages 428-469, 2006.

           JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants  by Schmitt, Stephan, Lori Lorigo, Christoph Kreitz, and Aleksey Nogin, International Joint Conference on Automated Reasoning, (IJCAR 2001), R. Gore, A. Leitsch, and T. Nipkow (eds.), LNAI 2083, pp. 421-426, Springer-Verlag, 2001.

           MetaPRL -- A Modular Logical Environment  by Hickey, Jason, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, and Lori Lorigo, Proceedings of 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'03), D. Basin and B. Wolff (eds.), LNCS 2758, pp. 287-303, Springer-Verlag, 2003.

           The Nuprl Open Logical Environment  by Allen, Stuart F., Robert L. Constable, Richard Eaton, Christoph Kreitz, and Lori Lorigo, Proceedings of 17th International Conference on Automated Deduction, LNAI 1831, pp. 170-176, Springer-Verlag, 2000.

           Using Formal Reference to Enhance Authority and Integrity in Online Mathematical Texts  by Allen, Stuart F., Robert L. Constable, and Lori Lorigo, To appear in Journal of Electronic Publishing, February, 2006.

           Specifications and Proofs for Ensemble Layers  by Hickey, Jason, Nancy Lynch, and Robbert van Renesse, Proceedings of Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '99), R. Cleaveland (ed.), LNCS 1579, pp. 119-133, Springer-Verlag, 1999.

           Automatic Program Optimization Via the Transformation of Nuprl Synthesis Proofs  by Madden, Peter, Proceedings of 1988 Alvey Technical Conference, L. Clarke (ed.), (also available from Edinburgh as DAI Research Paper No. 392), 1988.

           A Matrix Characterization for MELL  by Mantel, Heiko, and Christoph Kreitz, Proceedings of Sixth European Workshop on Logics in Artificial Intelligence (JELIA'98), J. Dix, F. L. Del Cerro, and U. Furbach (eds.), LNAI 1489, pp. 169-183, Springer-Verlag, 1998.

           Implementing Mathematics with the Nuprl Development System  by Constable, Robert L., Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith, Prentice-Hall:NJ, 1986.

           Inductive Definition in Type Theory  by Mendler, Nax P., Cornell University Ph.D. Thesis, 1988.

           Infinite Objects in Type Theory  by Mendler, Nax P., Robert L. Constable, and Prakash Panangaden, Proceedings of First IEEE Symposium on Logic in Computer Science, pp. 249-255, (also Cornell Technical Report 86-743), 1986.

           Recursive Definitions in Type Theory  by Constable, Robert L., and Nax P. Mendler, Proceedings of Logics of Progams Conference, pp. 61-78, (also Cornell Technical Report 85-659), 1985.

           Recursive Types and Type Constraints in Second-Order Lambda Calculus   by Mendler, Nax P., Proceedings of Second IEEE Symposium on Logic in Computer Science, pp. 30-36, 1987.

           A Dependent Set Theory  by Moczydlowski, Wojciech, To appear in Proceedings of Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS 2007)., 2007.

           Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics  by Constable, Robert L., and Wojciech Moczydlowski, , 2006.

           Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus  by Moczydlowski, Wojciech, and Robert L. Constable, Cornell University Technical Report 2006-2061. To appear in Proceedings of Symposium on Logical Foundations of Computer Science 2007, 2007.

           Normalization of intuitionistic set theories.  by Moczydlowski, Wojciech, Proceedings of Eighth International Workshop on Termination (WST 2006), 27-31., 2006.

           A Normalizing Intuitionistic Set Theory with Inaccessible Sets.  by Moczydlowski, Wojciech, Cornell University Technical Report 2006-2051. In submission., 2006.

           Termination of Single-Threaded One-rule Semi-Thue Systems  by Moczydlowski, Wojciech, and Alfons Geser, Proceedings of 16th International Conference on Rewriting Techniques and Applications (RTA 2005), LNCS 3467, 338-352, Springer., 2005.

           Innovations in Computational Type Theory using Nuprl  by Allen, Stuart F., Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, and Evan Moran, Journal of Applied Logic, Volume 4, Issue 4, December 2006, Pages 428-469, 2006.

           Concurrent Refinement in Nuprl  by Moten, Roderick, Cornell University Ph.D. Thesis, 1997.

           A Computational Analysis of Girard's Translation and LC  by Murthy, Chetan, Proceedings of Seventh IEEE Symposium on Logic in Computer Science, 1992.

           A Constructive Proof of Higman's Lemma  by Murthy, Chetan, and James R. Russell, Proceedings of Fifth IEEE Symposium on Logic in Computer Science, pp. 257-269, (also Cornell TR 89-1049), 1990.

           An Evaluation Semantics for Classical Proofs  by Murthy, Chetan, Proceedings of Sixth IEEE Symposium on Logic in Computer Science, pp. 96-109, (also Cornell TR 91-1213), 1991.

           Extracting Constructive Content from Classical Proofs  by Murthy, Chetan, Cornell University Ph.D. Thesis, 1990.

           Finding Computational Content from Classical Proofs  by Constable, Robert L., and Chetan Murthy, Logical Frameworks, G. Huet and G. Plotkin (eds.), pp. 341-362, Cambridge University Press, 1991.

           Formalizing Automata II: Decidable Properties  by Constable, Robert L., and Pavel Naumov, Unpublished manuscript, Cornell University, 1996.

           Formalizing Automata Theory I: Finite Automata  by Constable, Robert L., Paul B. Jackson, Pavel Naumov, and Juan Uribe, Unpublished manuscript, Cornell University, 1996.

           Formalizing Reference Types in Nuprl  by Naumov, Pavel, Cornell University Ph.D. Thesis, 1998.

           Fast Tactic-Based Theorem Proving  by Hickey, Jason, and Aleksey Nogin, Proceedings of 13th International Conference (TPHOLs 2000), LNCS 1869, pp. 252-266, Springer-Verlag, 2000.

           Formal Compiler Implementation in a Logical Framework  by Hickey, Jason, and Aleksey Nogin, Proceedings of MERLIN 2003, Second ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding, 2003.

           JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants  by Schmitt, Stephan, Lori Lorigo, Christoph Kreitz, and Aleksey Nogin, International Joint Conference on Automated Reasoning, (IJCAR 2001), R. Gore, A. Leitsch, and T. Nipkow (eds.), LNAI 2083, pp. 421-426, Springer-Verlag, 2001.

           Markov’s Principle For Propositional Type Theory  by Nogin, Aleksey, and Alexei Kopylov, Computer Science Logic, 2001, LNCS 2142, publisher Springer-Verlag, Berlin, pages 570-584, 2001.

           MetaPRL -- A Modular Logical Environment  by Hickey, Jason, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, and Lori Lorigo, Proceedings of 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'03), D. Basin and B. Wolff (eds.), LNCS 2758, pp. 287-303, Springer-Verlag, 2003.

           Quotient Types: A Modular Approach  by Nogin, Aleksey, Proceedings of 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'02), V.A. Carreño, C. Muñoz, and S. Tahar (eds.), LNCS 2410, pp. 263-280, Springer-Verlag, 2002.

           Writing Constructive Proofs Yielding Efficient Extracted Programs  by Nogin, Aleksey, Electronic Notes in Theoretical Computer Science, vol. 37, 2001.

           A Programming Logic  by Constable, Robert L., and Michael J. O'Donnell, Winthrop, MA, 1978.

           Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization  by O'Leary, John, Miriam Leeser, Jason Hickey, and Mark Aagaard, Theorem Provers in Circuit Design, Theory Practice and Experience (TPCD '94), Springer-Verlag, 1994.

           Connection-Based Theorem Proving in Classical and Non-Classical Logics  by Kreitz, Christoph, and Jens Otten, Journal of Universal Computer Science, vol. 5, no. 3, pp. 88-112, Springer-Verlag, 1999.

           Matrix-Based Constructive Theorem Proving  by Kreitz, Christoph, Jens Otten, Stephan Schmitt, and Brigitte Pientka, Intellectics and Computational Logic: Papers in Honor of Wolfgang Bibel, S. Hölldobler (ed.), pp. 189-205, Kluwer, 2000.

           Implementing Mathematics with the Nuprl Development System  by Constable, Robert L., Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith, Prentice-Hall:NJ, 1986.

           Infinite Objects in Type Theory  by Mendler, Nax P., Robert L. Constable, and Prakash Panangaden, Proceedings of First IEEE Symposium on Logic in Computer Science, pp. 249-255, (also Cornell Technical Report 86-743), 1986.

           Knowledge-Based Synthesis of Distributed Systems Using Event Structures  by Bickford, Mark, Robert L. Constable, Joseph Y. Halpern, and Sabina Petride, Cornell University Technical Report 2004-1927, 2004.

           Knowledge-based synthesis of distributed systems using event structures.  by Bickford, Mark, Robert L. Constable, Joseph Y. Halpern, and Sabina Petride, In Franz Baader and Andreo Voronsky, editors, Logic for Programming, Artificial Intelligence, and Reasoning, volume 3452 of Lecture Notes in Computer Science, pages 449-465, 2005.

           Automating Inductive Specification Proofs  by Pientka, Brigitte, and Christoph Kreitz, Fundamenta Informatica, vol. 39, nos. 1-2, pp. 189-208, 1999.

           Connection-Driven Inductive Theorem Proving  by Kreitz, Christoph, and Brigitte Pientka, Studia Logica, vol. 69, no. 2, pp. 293-326, 2001.

           Instantiation of Existentially Quantified Variables in Inductive Specification Proofs  by Pientka, Brigitte, and Christoph Kreitz, Proceedings of Fourth International Conference on Artificial Intelligence and Symbolic Computation (AISC'98), J. Calmet and J. Plaza (eds.), LNAI 1476, pp. 247-258, Springer-Verlag, 1998.

           Matrix-Based Constructive Theorem Proving  by Kreitz, Christoph, Jens Otten, Stephan Schmitt, and Brigitte Pientka, Intellectics and Computational Logic: Papers in Honor of Wolfgang Bibel, S. Hölldobler (ed.), pp. 189-205, Kluwer, 2000.

           Matrix-Based Inductive Theorem Proving  by Kreitz, Christoph, and Brigitte Pientka, International Conference TABLEAUX-2000, R. Dyckhoff (ed.), LNAI 1847, pp. 294-308, Springer-Verlag, 2000.

           Collaborative Mathematics Environments  by Constable, Robert L., Paul Chew, Keshav Pingali, Steve Vavasis, and Richard Zippel, Unpublished manuscript, Cornell University, 1996.

           Automating Proofs in Category Theory  by Kozen, Dexter, Christoph Kreitz, and Eva Richter, International Conference - IJCAR 2006, LNAI 4130, pp. 392-407, Springer Verlag, 2006., 2006.

           The Horus and Ensemble Projects: Accomplishments and Limitations  by Birman, Kenneth, Robert L. Constable, Mark Hayden, Jason Hickey, Christoph Kreitz, Robbert van Renesse, Ohad Rodeh, and Werner Vogels, Proceedings of DARPA Information Survivability Conference and Exhibition (DISCEX '00), 2000.

           A Constructive Proof of Higman's Lemma  by Murthy, Chetan, and James R. Russell, Proceedings of Fifth IEEE Symposium on Logic in Computer Science, pp. 257-269, (also Cornell TR 89-1049), 1990.

           Extracting Efficient Code from Constructive Proofs  by Sasaki, James T., Cornell University Ph.D. Thesis, 1985.

           Implementing Mathematics with the Nuprl Development System  by Constable, Robert L., Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith, Prentice-Hall:NJ, 1986.

           JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants  by Schmitt, Stephan, Lori Lorigo, Christoph Kreitz, and Aleksey Nogin, International Joint Conference on Automated Reasoning, (IJCAR 2001), R. Gore, A. Leitsch, and T. Nipkow (eds.), LNAI 2083, pp. 421-426, Springer-Verlag, 2001.

           Matrix-Based Constructive Theorem Proving  by Kreitz, Christoph, Jens Otten, Stephan Schmitt, and Brigitte Pientka, Intellectics and Computational Logic: Papers in Honor of Wolfgang Bibel, S. Hölldobler (ed.), pp. 189-205, Kluwer, 2000.

           A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems  by Kreitz, Christoph, and Stephan Schmitt, Journal of Information and Computation, vol. 162, nos. 1-2, pp. 226-254, 2000.

           The Oyster-Clam System  by Bundy, Alan, Frank Van Harmelen, Christian Horn, and Alan Smaill, Proceedings of 10th International Conference on Automated Design, LNAI 449, M. E. Stickel (ed.), pp. 647-648, Springer-Verlag, 1990.

           Reflection in Constructive and Non-Constructive Automated Reasoning  by Giunchiglia, Fausto, and Alan Smaill, Meta-Programming in Logic Programming, H. Abramson and M.H. Rogers (eds.), pp. 123-140, MIT Press, 1989.

           Computational Foundations of Basic Recursive Function Theory  by Constable, Robert L., and Scott F. Smith, Proceedings of Third IEEE Symposium on Logic in Computer Science, pp. 360-371, (also Cornell Technical Report 88-904), 1988.

           Implementing Mathematics with the Nuprl Development System  by Constable, Robert L., Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith, Prentice-Hall:NJ, 1986.

           Partial Objects in Constructive Type Theory  by Smith, Scott F., and Robert L. Constable, Proceedings of Second IEEE Symposium on Logic in Computer Science, pp. 183-193, (also Cornell TR 87-822), 1987.

           Partial Objects in Type Theory  by Smith, Scott F., Cornell University Ph.D. Thesis, 1989.

           An Operational Approach to Combining Classical Set Theory and Functional Programming Languages  by Howe, Douglas J., and Scott D. Stoller, Proceedings of International Symposium on Theoretical Aspects of Computer Software (TACS '94), M. Hagiya and J. Mitchell (eds.), LNCS 789, pp. 36-55, Springer-Verlag, 1994.

           Aspects of the Computational Content of Proofs  by Underwood, Judith, Cornell University Ph.D. Thesis, 1994.

           Classical Tools for Constructive Proof Search  by Caldwell, James L., and Judith Underwood, Proceedings of CADE-13 Workshop on Proof Search in Type-Theoretic Languages, D. Galmiche (ed.), Rutgers:NJ, 1996.

           A Constructive Completeness Proof for the Intuitionistic Propositional Calculus  by Underwood, Judith, Cornell University Technical Report 90-1179, 1990.

           Search Algorithms in Type Theory  by Caldwell, James L., Ian Gent, and Judith Underwood, Theoretical Computer Science, vol. 232, nos. 1-2, pp. 55-90, 2000.

           The Tableau Algorithm for Intuitionistic Propositional Calculus as a Constructive Completeness Proof  by Underwood, Judith, Proceedings of Workshop on Theorem Proving with Analytic Tableaux, pp. 245-248, 1993.

           Formalizing Automata Theory I: Finite Automata  by Constable, Robert L., Paul B. Jackson, Pavel Naumov, and Juan Uribe, Unpublished manuscript, Cornell University, 1996.

           Building Reliable, High-Performance Communication Systems from Components  by Liu, Xiaoming, Christoph Kreitz, Robbert van Renesse, Jason Hickey, Mark Hayden, Kenneth Birman, and Robert L. Constable, Proceedings of 17th ACM Symposium on Operating System Principles (SOSP'99), Operating Systems Review, vol. 34, no. 5, pp. 80-92, 1999.

           An Experiment in Formal Design Using Meta-Properties  by Bickford, Mark, Christoph Kreitz, Robbert van Renesse, and Robert L. Constable, Proceedings of DARPA Information Survivability Conference and Exposition II (DISCEX II), pp. 100-107, 2001.

           Formally Verifying Hybrid Protocols with the Nuprl Logical Programming Environment  by Bickford, Mark, Christoph Kreitz, and Robbert van Renesse, Cornell University Technical Report 2001-1839, 2001.

           The Horus and Ensemble Projects: Accomplishments and Limitations  by Birman, Kenneth, Robert L. Constable, Mark Hayden, Jason Hickey, Christoph Kreitz, Robbert van Renesse, Ohad Rodeh, and Werner Vogels, Proceedings of DARPA Information Survivability Conference and Exhibition (DISCEX '00), 2000.

           Protocol Switching: Exploiting Meta-Properties  by Liu, Xiaoming, Robbert van Renesse, Mark Bickford, Christoph Kreitz, and Robert L. Constable, ProceedingsInternational Workshop on Applied Reliable Group Communication (WARGC'01), IEEE Computer Society Press, 2001.

           Proving Hybrid Protocols Correct  by Bickford, Mark, Christoph Kreitz, Robbert van Renesse, and Xiaoming Liu, Proceedings of 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'01), R. Boulton and P. Jackson (eds.), LNCS 2152, pp. 105-120, Springer-Verlag, 2001.

           Specifications and Proofs for Ensemble Layers  by Hickey, Jason, Nancy Lynch, and Robbert van Renesse, Proceedings of Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '99), R. Cleaveland (ed.), LNCS 1579, pp. 119-133, Springer-Verlag, 1999.

           Collaborative Mathematics Environments  by Constable, Robert L., Paul Chew, Keshav Pingali, Steve Vavasis, and Richard Zippel, Unpublished manuscript, Cornell University, 1996.

           The Horus and Ensemble Projects: Accomplishments and Limitations  by Birman, Kenneth, Robert L. Constable, Mark Hayden, Jason Hickey, Christoph Kreitz, Robbert van Renesse, Ohad Rodeh, and Werner Vogels, Proceedings of DARPA Information Survivability Conference and Exhibition (DISCEX '00), 2000.

           Collaborative Mathematics Environments  by Constable, Robert L., Paul Chew, Keshav Pingali, Steve Vavasis, and Richard Zippel, Unpublished manuscript, Cornell University, 1996.