## Chapters in Books

- Polymorphic Logic. In
*Logic, Construction, Computation*, editors U. Berger, H. Diener, P. Schuster, M. Seisenberger, Ontos Verlag, 2013 (with M. Bickford). - Russell's Orders in Kripke's Theory of Truth and Computational Type Theory. In
*Handbook of the History of Logic: Sets and Extensions in the Twentieth Century*, editors D. M. Gabbay, A. Kanamori, and J. Woods, Elsevier B.V., Vol. 6, 2012, pages 801-845 (with F. Kamareddine and T. Laan). - The Triumph of Types: Principia Mathematica's Impact on Computer Science. In
*Principia Mathematica Anniversary Symposium*, 2010. - 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. - 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 M. Bickford). - 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. - 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. - 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). - 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. - 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). - Formalizing Decidability Theorems about Automata. In
*Computational Logic*, editors U. Berger and H. Schwichtenberg, NATO ASI Series, Springer, Vol. 165, 1999, pages 179–213. - Types in Logic, Mathematics and Programming. In
*Handbook of Proof Theory*, editor S. R. Buss, Elsevier Science B.V., 1998, pages 683–786. - The Structure of Nuprl’s Type Theory. In
*Logic and Computation, NATO ASI Series*, Springer-Verlag, 1996, pages 123–156. - Using Reflection to Explain and Enhance Type Theory. In
*Proof and Computation, NATO ASI Series*, Springer-Verlag, 1994, pages 65–100. - Metalogical Frameworks. In
*Logical Environments*, editors G. Huet and G. Plotkin, Cambridge University Press, 1993, pages 1–29 (with D. A. Basin). - 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. - Metalevel Programming in Constructive Type Theory. In
*Programming and Mathematical Method*, NATO ASI Series, Vol. F88, Springer-Verlag, 1992, pages 45–93. - 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. - 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). - Nuprl as a General Logic. In
*Logics for Computer Science*, Academic Press, 1990, pages 77–90 (with D. Howe). - 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). - 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. - Themes in the Development of Programming Logics Circa 1963-1987. In
*Annual Review of Computer Science*, Vol. 3, 1988, pages 147–165. - The Role of Finite Automata in the Development of Modern Computing Theory. In
*Proceedings of the Kleene Symposium*, North-Holland, 1980, pages 59–81. - 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.