## Journal Articles

- Intuitionistic Completeness of First-Order Logic. In
*Annals of Pure and Applied Logic*, Elsevier B.V., Vol. 165, Issue 1, 2014, pages 164–198 (with M. Bickford). - Knowledge-Based Synthesis of Distributed Systems Using Event Structures. In
*Logical Methods in Computer Science*, Vol. 7, Issue 2, 2011, (with M. Bickford, J. Halpern, and S. Petride). - Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics. In
*Logical Methods in Computer Science*, Vol. 4, Issue 3, 2008, (with W. Moczydlowski). - Transforming the Academy: Knowledge Formation in the Age of Digital Information,
*Physica Plus*, Issue No. 9, Jan 2007. - Innovations in Computational Type Theory using Nuprl. In
*Journal of Applied Logic*, Vol. 4, Issue 4, 2006, Pages 428–469,(with S. Allen, M. Bickford, R. Eaton, C. Kreitz, L. Lorigo, and E. Moran). - Using Formal Reference to Enhance Authority and Integrity in Online Mathematical Texts. In
*Journal of Electronic Publishing*, Vol. 9, No. 2, 2006 (with L. Lorigo and S. Allen). - The Future of Departments. In
*Academic Leader*, 19, 2003, pages 1–12 (with G. C. Altschuler). - The Horus and Ensemble Projects: Accomplishments and Limitations. In
*DISCEX ’00*, Vol. I, 2000, pages 149–161 (with K. Birman, M. Hayden, J. Hickey, C. Kreitz, R. van Renesse, O. Rodeh, and W. Vogels). - Metalogical Frameworks II: Developing a Reflected Decision Procedure. In
*Journal of Automated Reasoning*, Vol. 22(2), 1999, pages 171–221 (with W. E. Aitken and J. L. Underwood). - A Note on Complexity Measures for Inductive Classes in Constructive Type Theory. In
*Information and Computation*, Vol. 143(2), 1998, pages 137–153. - Computational Foundations of Basic Recursive Function Theory. In
*Theoretical Computer Science B: Logic, Semantics, and Theory of Programming*, Vol. 120, 1993, pages 89–112 (with S. F. Smith). - On Writing Programs that Construct Proofs. In
*Journal of Automated Reasoning*, Vol. 1, 1985, pages 285–326 (with T. Knoblock and J. Bates). - Proofs as Programs. In
*Transactions on Programming Languages and Systems*, Vol. 7(1), 1985, pages 113–136. - Remembrances of Errett Bishop. In
*Contemporary Mathematics*, American Mathematical Society, Vol. 39, 1985, pages 79-84 (with A. Nerode and G. Metakides). - Constructive Mathematics as a Programming Logic I: Some Principles of Theory. In
*Foundations of Computing Theory, Lecture Notes in Computer Science*158, Springer-Verlag, NY, 1983, pages 64–77; also*Annals of Discrete Mathematics*, Vol. 24, 1985, pages 21–38. - The Type Theory of PL/CV3. In
*Logics of Programs, Lecture Notes in Computer Science*135, Springer-Verlag, 1982, pages 72–93 (with D. Zlatin); also in*Transactions on Programming Languages and Systems*, Vol. 6(1), 1984, pages 94–117. - Programs as Proofs. In
*Information Processing Letters*, Vol. 16(3), 1983, pages 105–112. - A Hierarchical Approach to Formal Semantics with Application to the Definition of PL/CS.
In
*Transactions on Programming Languages and Systems*, Vol. 1(1), 1979, pages 98–114 (with J. Donahue). - On Computational Complexity of Scheme Equivalence. In
*Proceedings of the Eighth Princeton Conference on Information Sciences and Systems*, 1974; also*SICOMP*, Vol. 9(2), 1980, pages 396–416 (with H. Hunt and S. Sahni). - A Constructive Programming Logic. In
*Proceedings of the World Computer Congress of the IFIP 77*, 1977, pages 733–738. - Computability Concepts for Programming Language Semantics. In
*Proceedings of the Seventh ACM Symposium on the Theory of Computing*, 1975, pages 98–105; also*Theoretical Computer Science 2*, 1976, pages 133–145 (with H. Egli). - Two Types of Hierarchy Theorem for Axiomatic Complexity Classes. In
*Courant Computer Science Symposium 7*, Computational Complexity, Algorithmic Press, NY, 1973, pages 733–738. - The Operator Gap. In
*Proceedings of the Ninth IEEE Symposium on Switching and Automata Theory*, 1969, pages 20–26 (expanded in Journal of the ACM, Vol. 19(1), 1972, pages 175–183). - On the Efficiency of Programs in Subrecursive Formalisms. In
*Proceedings of the Tenth IEEE Symposium on Switching and Automata Theory*, 1972, pages 60–67; also as Subrecursive Programming Languages I; also, in*Journal of the ACM*, Vol. 19(3), 1972, pages 526–586 (with A. Borodin). - On Classes of Program Schemata. In
*SIAM Journal of Computing*, Vol. 1(1), 1972, pages 66–118 (with D. Gries). - Subrecursive Program Schemata I Undecidable Equivalence Problems. In
*Proceedings of the Fourth Symposium on the Theory of Computing*, 1972; also*Journal of Computer and System Sciences*Vol. 6(6), 1972, pages 480–518 (with S. Muchnick). - Constructive Mathematics and Automatic Program Writers. In
*Proceedings of the World Computer Congress*of the IFIP, 1971, pages 229–233.