Skip to main content
more options

Chapters in Books

  1. Building Mathematics-Based Software Systems to Advance Science and Create Knowledge. In Lecture Notes in Computer Science, Springer-Verlag, Berlin-Heidelberg, Vol. 5760, 2009, pages 3–17.
  2. Formal Foundations of Computer Security. In NATO Science for Peace and Security Series, D: Information and Communication Security, Vol. 14, 2008, pages 29–52, (with Mark Bickford).
  3. Recent Results in Type Theory and Their Relationship to Automath. In Thirty Five Years of Automating Mathematics, editor F. Kamareddine, Kluwer, Amsterdam, 2003, pages 37–48.
  4. Naive Computational Type Theory. In Proof and System-Reliability, editors H. Schwichtenberg and R. Steinbrueggen, NATO Science Series III, International Summer School Marktoberdorf, Kluwer, Amsterdam, 2002, pages 213–260.
  5. Computational Complexity and Induction for Partial Computable Functions in Type Theory. In Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, editors W. Sieg, R. Sommer, and C. Talcott, Association for Symbolic Logic, 2001, pages 166–183 (with K. Crary).
  6. Nuprl’s Class Theory and its Applications. In Foundations of Secure Computation, editors F. L. Bauer and R. Steinbrueggen, NATO Science Series F, IOS Press, Amsterdam, 2000, pages 91–116.
  7. Constructively Formalizing Automata. In Proof Language and Interaction: Essays in Honour of Robin Milner, MIT Press, Cambridge, 2000, pages 213–238 (with P. B. Jackson, P. Naumov, and J. Uribe).
  8. Formalizing Decidability Theorems about Automata. In Computational Logic, editors U. Berger and H. Schwichtenberg, NATO Advance Study Institute, International Summer School Marktoberdorf, Springer, 1999.
  9. Types in Logic, Mathematics and Programming. In Handbook of Proof Theory, editor S. R. Buss, Elsevier Science B.V., 1998, pages 683–786.
  10. The Structure of Nuprl’s Type Theory. In Logic and Computation, NATO ASI Series, Springer-Verlag, 1996, pages 123–156.
  11. Using Reflection to Explain and Enhance Type Theory. In Proof and Computation, NATO ASI Series, Springer-Verlag, 1994, pages 65–100.
  12. Metalogical Frameworks. In Logical Environments, editors G. Huet and G. Plotkin, Cambridge University Press, 1993, pages 1–29 (with David A. Basin).
  13. Metalevel Programming in Constructive Type Theory. In Programming and Mathematical Method, NATO ASI Series, Vol. F88, Springer-Verlag, 1992, pages 45–93.
  14. Formal Theories and Software Systems: Fundamental Connections between Computer Science and Logic. In Future Tendencies in Computer Science, Control and Applied Mathematics, Lecture Notes in Computer Science 653, Springer-Verlag, 1992, pages 105–127.
  15. Lectures on: Classical Proofs as Programs. In Logic and Algebra of Specification, editors F.L. Bauer, W. Brauer, and H. Schwichtenberg, Springer, 1993, pages 31–61.
  16. Reflecting the Open-ended Computation System of Type Theory. In Logic, Algebra, and Computation, editor F.L. Bauer, Springer, 1991, pages 265–280 (with D. Howe and S. F. Allen).
  17. Nuprl as a General Logic. In Logics for Computer Science, Academic Press, 1990, pages 77–90 (with D. Howe).
  18. Implementing Metamathematics as an Approach to Automatic Theorem Proving. In A Source Book of Formal Approaches in Artificial Intelligence, North-Holland, 1990, pages 45–75 (with D. Howe).
  19. Assigning Meaning to Proofs: A Semantic Basis for Problem Solving Environments. In Constructive Methods in Computing Science, editor M. Broy, NATO ASI Series, Vol. F55, Springer-Verlag, 1989, pages 63–91.
  20. Themes in the Development of Programming Logics Circa 1963-1987. In Annual Review of Computer Science, Vol. 3, 1988, pages 147–165.
  21. The Role of Finite Automata in the Development of Modern Computing Theory. In Proceedings of the Kleene Symposium, North-Holland, 1980, pages 59–81.
  22. A Discussion of Program Verification. In Proceedings of the Conference on Research Directions in Software Technology, editor P. Wegner, MIT Press, Cambridge, 1979, pages 393–403.