1.Abstract Identifiers and Textual Reference
by Allen, Stuart F.,
Cornell University Technical Report 2002-1885, 2002.
2.Abstract Identifiers, Intertextual Reference and a Computational Basis for Recordkeeping
by Allen, Stuart F.,
First Monday, vol. 9, no. 2, 2004.
3.An Abstract Semantics for Atoms in Nuprl
by Allen, Stuart F.,
Cornell Tech Report TR2006-2032, 2006.
4.Aspects of the Computational Content of Proofs
by Underwood, Judith,
Cornell University Ph.D. Thesis, 1994.
5.Aspects of the Implementation of Type Theory
by Harper, Robert W.,
Cornell University Ph.D. Thesis, 1985.
6.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.
7.Automated Complexity Analysis of Nuprl Extracted Programs
by Benzinger, Ralph,
Journal of Functional Programming, vol. 11, no.1, pp. 3-31, 2001.
8.Automated Computational Complexity Analysis
by Benzinger, Ralph,
Cornell University Ph.D. Thesis, 2001.
9.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.
10.Automated Proof of Authentication Protocols in a Logic of Events
by Bickford, Mark,
, 2010.
11.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.
12.Automating Inductive Specification Proofs
by Pientka, Brigitte, and Christoph Kreitz,
Fundamenta Informatica, vol. 39, nos. 1-2, pp. 189-208, 1999.
13.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.
14.Automating Reasoning in an Implementation of Constructive Type Theory
by Howe, Douglas J.,
Cornell University Ph.D. Thesis, 1988.
15.Building Mathematics-Based Software Systems to Advance
Science and Create Knowledge
by Constable, Robert L.,
From: Efficient Algorithms: Essays Dedicated to Kurt Mehlhorn on the Occasion of His 60th Birthday. Springer, 2009., 2009.
16.Building Problem Solving Environments in Constructive Type Theory
by Basin, David A.,
Cornell University Ph.D. Thesis, 1990.
17.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.
18.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.
19.A Causal Logic of Events in Formalized Computational Type Theory
by Bickford, Mark, and Robert L. Constable,
Cornell University Technical Report, 2005.
20.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.
21.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.
22.Collaborative Mathematics Environments
by Constable, Robert L., Paul Chew, Keshav Pingali, Steve Vavasis, and Richard Zippel,
Unpublished manuscript, Cornell University, 1996.
23.Component Specification Using Event Classes
by Bickford, Mark,
Lecture Notes in Computer Science, Vol. 5582, pp. 140-155., 2009.
24.Component Specification Using Event Classes
by Bickford, Mark,
, 2009.
25.A Computational Analysis of Girard's Translation and LC
by Murthy, Chetan,
Proceedings of Seventh IEEE Symposium on Logic in Computer Science, 1992.
26.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.
27.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.
28.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.
29.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.
30.Computational Type Theory -- Extended Version
by Constable, Robert L.,
Cornell University Tech Report Ref Number 11513, 2008.
31.Concurrent Refinement in Nuprl
by Moten, Roderick,
Cornell University Ph.D. Thesis, 1997.
32.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.
33.Connection-Driven Inductive Theorem Proving
by Kreitz, Christoph, and Brigitte Pientka,
Studia Logica, vol. 69, no. 2, pp. 293-326, 2001.
34.Constructive Automata Theory Implemented with the Nuprl Proof Development System
by Kreitz, Christoph,
Cornell University Technical Report 86-779, 1986.
35.A Constructive Completeness Proof for the Intuitionistic Propositional Calculus
by Underwood, Judith,
Cornell University Technical Report 90-1179, 1990.
36.Constructive Mathematics and Automatic Program Writers
by Constable, Robert L.,
Proceedings of IFIP Congress, pp. 229-233, 1971.
37.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.
38.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.
39.Creating and Evaluating Interactive Formal Courseware for Mathematics and Computing
by Constable, Robert L.,
Unpublished manuscript, Cornell University, 1996.
40.Decidability Extracted: Synthesizing "Correct-by-Construction" Decision Procedures from Constructive Proofs
by Caldwell, James L.,
Cornell University Ph.D Thesis, 1998.
41.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.
42.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.
43.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.
44.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.
45.Effectively Nonblocking Concensus Procedures Can Execute Forever - a Constructive Version of FLP
by Constable, Robert L.,
Revised 2011 in arXiv:1109.3370.
Cornell University Tech Report Ref Number 11512, 2008.
46.Enabling Large Scale Coherency Among Mathematical Texts
by Allen, Stuart F., and Robert L. Constable,
Cornell University Technical Report, 2006-2014, 2006.
47.Encoding Pi Calculus
by Guaspari, David,
Encodes the pi calculus in the general process model of LICS paper by Bickford and Constable 2010, 2010.
48.Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra
by Jackson, Paul B.,
Cornell University Ph.D. Thesis, 1995.
49.The Ensemble System
by Hayden, Mark,
Cornell University Ph.D. Thesis, 1998.
50.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.
51.Equality in Lazy Computation Systems
by Howe, Douglas J.,
Proceedings of Fourth IEEE Symposium on Logic in Computer Science, pp. 198-203, 1989.
52.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.
53.Experience Using Type Theory as a Foundation for Computer Science Circa 1985-1995
by Constable, Robert L.,
Unpublished manuscript, Cornell University, 1996.
54.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.
55.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.
56.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.
57.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.
58.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.
59.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.
60.Extracting Constructive Content from Classical Proofs
by Murthy, Chetan,
Cornell University Ph.D. Thesis, 1990.
61.Extracting Efficient Code from Constructive Proofs
by Sasaki, James T.,
Cornell University Ph.D. Thesis, 1985.
62.Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics
by Constable, Robert L., and Wojciech Moczydlowski,
, 2006.
63.Extracting Propositional Decidability: A Proof of Propositional Decidability in Constructive Type Theory and its Extracted Program
by Caldwell, James L.,
Unpublished manuscript, 1997.
64.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.
65.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.
66.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.
67.The FDL Navigator: Browsing and Manipulating Formal Content
by Kreitz, Christoph,
Unpublished manuscript, Cornell University, 2003.
68.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.
69.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.
70.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.
71.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.
72.Formal Objects in Type Theory Using Very Dependent Types
by Hickey, Jason,
Foundations of Object-Oriented Languages 3, 1996.
73.Formal Reasoning About Communication Systems I: Embedding ML in Type Theory
by Kreitz, Christoph,
Cornell University Technical Report 97-1637, 1997.
74.Formal Reasoning About Communication Systems II: Automated Fast-Track Reconfiguration
by Kreitz, Christoph,
Cornell University Technical Report 98-1707, 1998.
75.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.
76.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.
77.Formalizing Automata II: Decidable Properties
by Constable, Robert L., and Pavel Naumov,
Unpublished manuscript, Cornell University, 1996.
78.Formalizing Automata Theory I: Finite Automata
by Constable, Robert L., Paul B. Jackson, Pavel Naumov, and Juan Uribe,
Unpublished manuscript, Cornell University, 1996.
79.Formalizing chain replication
by Guaspari, David, and Mark Bickford,
, 2006.
80.Formalizing Constructive Real Analysis
by Forester, Max B.,
Unpublished manuscript, Cornell University, 1993.
81.Formalizing Reference Types in Nuprl
by Naumov, Pavel,
Cornell University Ph.D. Thesis, 1998.
82.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.
83.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.
84.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.
85.From dy/dx to []P: A Matter of Notation
by Allen, Stuart F.,
Proceedings of Conference on User Interfaces for Theorem Provers, 1998.
86.Generating Event Logics with Higher-Order Processes as Realizers
by Bickford, Mark, Robert L. Constable, and David Guaspari,
, 2010.
87.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.
88.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.
89.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.
90.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.
91.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.
92.Implementing Reflection in Nuprl
by Barzilay, Eli,
Cornell University Ph.D. Thesis, 2006.
93.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.
94.Inductive Definition in Type Theory
by Mendler, Nax P.,
Cornell University Ph.D. Thesis, 1988.
95.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.
96.Information Management in the Service of Knowledge and Discovery
by Lorigo, Lori,
Cornell University Ph.D. Thesis, 2006.
97.Information-Intensive Proof Technology
by Constable, Robert L.,
Lecture Notes for the Marktoberdorf NATO Summer School, 2003.
98.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.
99.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.
100.Introduction to Classic ML and EventML Handbook
by Kreitz, Christoph, and Vincent Rahli,
EventML is an interface to components of a Logical Programming Environment (LPE) developed by the PRL group., 2011.
101.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.
102.Investigating Correct-by-Construction Attack-Tolerant Systems
by Constable, Robert L., Mark Bickford, and Robbert van Renesse,
, 2010.
103.Investigations in intersection types:Confluence, and semantics of expansion in the lambda-calculus, and a type error slicing method
by Rahli, Vincent,
, 2011.
104.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.
105.Knowledge-Based Synthesis of Distributed Systems Using Event Structures
by Bickford, Mark, Robert L. Constable, Joseph Y. Halpern, and Sabina Petride,
Also see logical methods is CS Vol 7, IS 2, #14
Cornell University Technical Report
2004-1927, 2004.
106.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 and Logical Methods is CS Vol 7, IS 2, #14, 2005.
107.Lectures on: Classical Proofs as Programs
by Constable, Robert L.,
Constructive Methods of Computing Science (NATO ASI Series), M. Broy (ed.), 1992.
108.A Logic for Correct Program Development
by Bates, Joseph L.,
Revision of Cornell University Ph.D. Thesis submitted August 1979, 1981.
109.A Logic of Events
by Bickford, Mark, and Robert L. Constable,
Cornell University Technical Report 2003-1893, 2003.
110.The Logic of Events, a framework to reason about distributed systems
by Rahli, Vincent, Robert L. Constable, and Mark Bickford,
, 2012.
111.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.
112.Logic-Based Knowledge Representation
by Jackson, Paul B.,
MIT Press:Cambridge MA, 1989.
113.Markov’s Principle For Propositional Type Theory
by Kopylov, Alexei, and Aleksey Nogin,
Computer Science Logic, 2001, LNCS 2142, publisher Springer-Verlag, Berlin, pages 570-584, 2001.
114.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.
115.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.
116.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.
117.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.
118.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.
119.Metalogical Frameworks II: Developing a Reflected Decision Procedure
by Constable, Robert L.,
Journal of Automated Reasoning, Volume 22, Issue 2, pp. 171-221., 1999.
120.Metamathematical Extensibility in Type Theory
by Knoblock, Todd B.,
Cornell University Ph.D. Thesis, 1987.
121.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.
122.The MetaPRL Logical Programming Environment
by Hickey, Jason,
Cornell University Ph.D. Thesis, 2001.
123.Meta-Synthesis: Deriving Programs That Develop Programs
by Kreitz, Christoph,
Unpublished manuscript, Technical University of Darmstadt, 1992.
124.Moving Proofs-as-Programs into Practice
by Caldwell, James L.,
Proceedings of 12th IEEE International Conference Automated Software Engineering (ASE'97), 1997.
125.Naive Computational Type Theory
by Constable, Robert L.,
Proof and System-Reliability, H. Schwichtenberg and R. Steinbruggen (eds.), pp. 213-259, 2002.
126.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.
127.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.
128.A Non-Type-Theoretic Semantics for Type-Theoretic Language
by Allen, Stuart F.,
Cornell University Ph.D. Thesis, 1987.
129.Normalization of intuitionistic set theories.
by Moczydlowski, Wojciech,
Proceedings of Eighth International Workshop on Termination (WST 2006), 27-31., 2006.
130.A Normalizing Intuitionistic Set Theory with Inaccessible Sets.
by Moczydlowski, Wojciech,
Cornell University Technical Report 2006-2051. In submission., 2006.
131.Notational Definition and Top-down Refinement for Interactive Proof Development Systems
by Griffin, Timothy G.,
Cornell University Ph.D. Thesis, 1988.
132.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.
133.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.
134.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.
135.The Nuprl Proof Development System
by Horn, Christian,
Deptartment of Artificial Intelligence Edinburgh Working Paper 214, 1988.
136.The Nuprl Proof Development System, Version 4.2 Reference Manual and User's Guide
by Jackson, Paul B.,
Unpublished manuscript, Cornell University, 1996.
137.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.
138.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.
139.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.
140.An Object-Oriented Approach to Verifying Group Communication Systems
by Bickford, Mark, and Jason Hickey,
Proceedings of CADE-16, 1999.
141.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.
142.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.
143.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.
144.Partial Objects in Type Theory
by Smith, Scott F.,
Cornell University Ph.D. Thesis, 1989.
145.Planning Proof Content for Communicating Induction
by Holland-Minkley, Amanda,
Proceedings of Second International Natural Language Generation Conference, pp. 167-172, 2002.
146.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.
147.A Programming Logic
by Constable, Robert L., and Michael J. O'Donnell,
Winthrop, MA, 1978.
148.A Programming Logic for Distributed Systems
by Bickford, Mark, and David Guaspari,
ATC-NY Technical Report, 2005.
149.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.
150.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.
151.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.
152.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.
153.Quotation and Reflection in Nuprl and Scheme
by Barzilay, Eli,
Cornell University Technical Report 2001-1832, 2001.
154.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.
155.Reasoning About Functional Programs in Nuprl
by Howe, Douglas J.,
Functional Programming Concurrency Simulation and Automated Reasoning, LNCS, 1993.
156.Recent results in type theory and their relationship to automath
by Constable, Robert L.,
, 2003.
157.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.
158.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.
159.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.
160.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.
161.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.
162.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.
163.Reversal-Bounded Computations
by Chan, Tat-hung,
Cornell University Ph.D. Thesis, 1980.
164.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.
165.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.
166.Semantics of Evidence
by Constable, Robert L.,
Cornell University Technical Report 84-684, 1985.
167.A Semantics of Objects in Type Theory
by Hickey, Jason,
Unpublished manuscript, Cornell University, 1997.
168.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.
169.A Simple Type Theory for Reasoning About Functional Programs
by Howe, Douglas J.,
Computer Science Department Cornell University (Pre-print), 1992.
170.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.
171.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.
172.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.
173.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.
174.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.
175.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.
176.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.
177.The Triumph of Types: Principia Mathematica's Impact on Computer Science
by Constable, Robert L.,
Presented at Principia Symposium 2010, 2010.
178.Type Theoretical Foundations for Data Structures, Classes, and Objects
by Kopylov, Alexei,
Cornell University Ph.D. Thesis, 2004.
179.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.
180.Type-Theoretic Methodology for Practical Programming Languages
by Crary, Karl,
Cornell University Ph.D. Thesis, 1998.
181.Type-Theoretic Models of Concurrency
by Cleaveland, Walter Rance,
Cornell University Ph.D. Thesis, 1987.
182.Unguessable Atoms: A Logical Foundation for Security
by Bickford, Mark,
, 2006.
183.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.
184.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.
185.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.
186.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.
187.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.
188.The Value of Automated Deduction
by Constable, Robert L.,
Unpublished manuscript, Cornell University, 1996.
189.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.
190.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.
191.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.
192.Writing Constructive Proofs Yielding Efficient Extracted Programs
by Nogin, Aleksey,
Electronic Notes in Theoretical Computer Science, vol. 37, 2001.
193.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.
