Publications - by Author

Click to re-sort items:

Aagaard, Mark

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.

Aitken, William

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.

Allen, Stuart F.

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.

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

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.

Aydemir, Brian

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.

Barzilay, Eli

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

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.

Barzilay, Regina

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.

Basin, David A.

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.

Bates, Joseph L.

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.

Benzinger, Ralph

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.

Bickford, Mark

Automated Proof of Authentication Protocols in a Logic of Events by Bickford, Mark,
, 2010.

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

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.

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.

Generating Event Logics with Higher-Order Processes as Realizers by Bickford, Mark, Robert L. Constable, and David Guaspari
, 2010.

Investigating Correct-by-Construction Attack-Tolerant Systems by Constable, Robert L., Mark Bickford, and Robbert van Renesse
, 2010.

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.

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.

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

The Logic of Events, a framework to reason about distributed systems by Rahli, Vincent, Robert L. Constable, and Mark Bickford
, 2012.

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,
Verified Software: Theories, Tools, Experiments, Second International Conference, VSTTE 2008 Toronto, Canada, pp 30 - 53, 2008.

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

Birman, Kenneth

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.

Bromley, H. M.

Brown, Geoffrey

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.

Bundy, Alan

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.

Caldwell, James L.

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.

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.

Chan, Tat-hung

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

Chen, Wilfred Z.

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.

Chew, Paul

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

Cleaveland, Walter Rance

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

Constable, Robert L.

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

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.,
Revised 2011 in arXiv:1109.3370. 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.

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

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

Generating Event Logics with Higher-Order Processes as Realizers by Bickford, Mark, Robert L. Constable, and David Guaspari
, 2010.

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.

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.

Investigating Correct-by-Construction Attack-Tolerant Systems by Constable, Robert L., Mark Bickford, and Robbert van Renesse
, 2010.

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.

The Logic of Events, a framework to reason about distributed systems by Rahli, Vincent, Robert L. Constable, and Mark Bickford
, 2012.

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.

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.

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.

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.

Recent results in type theory and their relationship to automath by Constable, Robert L.,
, 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.

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.

The Triumph of Types: Principia Mathematica's Impact on Computer Science by Constable, Robert L.,
Presented at Principia Symposium 2010, 2010.

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

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.

Crary, Karl

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.

Cremer, J. F.

Del Vecchio, Peter

Eaton, Richard

Fluet, Matthew

Forester, Max B.

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

Gent, Ian

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.

Geser, Alfons

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.

Giunchiglia, Fausto

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.

Griffin, Timothy G.

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

Guaspari, David

Encoding Pi Calculus by Guaspari, David,
Encodes the pi calculus in the general process model of LICS paper by Bickford and Constable 2010, 2010.

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

Generating Event Logics with Higher-Order Processes as Realizers by Bickford, Mark, Robert L. Constable, and David Guaspari
, 2010.

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

Hafizogullari, Ozan

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.

Halpern, Joseph Y.

Harmelen, Frank Van

Harper, Robert W.

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

Hayden, Mark

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

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.

Hickey, Jason

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 MetaPRL Logical Programming Environment by Hickey, Jason,
Cornell University Ph.D. Thesis, 2001.

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

Holland-Minkley, Amanda

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

Horn, Christian

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

Howe, Douglas J.

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

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.

Jackson, Paul B.

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.

Kleinberg, Jon

Knoblock, Todd B.

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.

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.

Kopylov, Alexei

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.

Kozen, Dexter

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.

Kreitz, Christoph

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.

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.

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

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.

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.

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.

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.

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.

Leeser, Miriam

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.

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.

Liu, Xiaoming

Lorigo, Lori

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

Lynch, Nancy

Madden, Peter

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.

Mantel, Heiko

Mendler, Nax P.

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

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.

Moczydlowski, Wojciech

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.

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.

Moran, Evan

Moten, Roderick

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

Murthy, Chetan

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.

Naumov, Pavel

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.

Nogin, Aleksey

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.

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.

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.

O'Donnell, Michael J.

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

O'Leary, John

Otten, Jens

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.

Panangaden, Prakash

Petride, Sabina

Pientka, Brigitte

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.

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.

Pingali, Keshav

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

Rahli, Vincent

Investigations in intersection types:Confluence, and semantics of expansion in the lambda-calculus, and a type error slicing method by Rahli, Vincent,
, 2011.

The Logic of Events, a framework to reason about distributed systems by Rahli, Vincent, Robert L. Constable, and Mark Bickford
, 2012.

Richter, Eva

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.

Rodeh, Ohad

Russell, James R.

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.

Sasaki, James T.

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

Schmitt, Stephan

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.

Smaill, Alan

Smith, Scott F.

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

Stoller, Scott D.

Underwood, Judith

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

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.

Uribe, Juan

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

van Renesse, Robbert

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.

Investigating Correct-by-Construction Attack-Tolerant Systems by Constable, Robert L., Mark Bickford, and Robbert van Renesse
, 2010.

Vavasis, Steve

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

Vogels, Werner

Zippel, Richard

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