1.          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.

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

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

4.          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.

5.          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.

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

7.          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.

8.          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.

9.          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.

10.      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.

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

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

13.      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.

14.      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.

15.      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.

16.      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.

17.      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.

18.      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.

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

20.      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.

21.      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.

22.      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.

23.      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.

24.      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.

25.      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.

26.      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.

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

28.      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.

29.      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.

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

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

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

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

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

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

36.      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.

37.      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.

38.      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.

39.      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.

40.      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.

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

42.      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.

43.      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.

44.      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.

45.      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.

46.      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.

47.      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.

48.      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.

49.      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.

50.      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.

51.      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.

52.      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.

53.      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.

54.      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.

55.      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.

56.      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.

57.      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.

58.      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.

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

60.      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.

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

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