Skip to main content
more options

Journal Articles

  1. Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics. In Logical Methods in Computer Science, Volume 4, Issue 3, Paper 5, Creative Commons, September 2008, (with Wojciech Moczydlowski).
  2. Innovations in Computational Type Theory using Nuprl. In Journal of Applied Logic, Volume 4, Issue 4, December 2006, Pages 428 – 469,(with S. Allen, M. Bickford, R. Eaton, C. Kreitz, L. Lorigo, and E. Moran).
  3. Using Formal Reference to Enhance Authority and Integrity in Online Mathematical Texts. In Journal of Electronic Publishing, Summer 2006, vol. 9, no. 2, 2006 (with L. Lorigo and S. Allen)
  4. 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)
  5. 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).
  6. A Note on Complexity Measures for Inductive Classes in Constructive Type Theory. In Information and Computation, Vol. 143(2), 1998, pages 137–153.
  7. 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).
  8. On Writing Programs that Construct Proofs. In Journal of Automated Reasoning, Vol. 1, 1985, pages 285–326 (with T. Knoblock and J. Bates).
  9. Proofs as Programs. In Transactions on Programming Languages and Systems, Vol. 7(1), 1985, pages 113–136.
  10. 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.
  11. 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.
  12. Programs as Proofs. In Information Processing Letters, Vol. 16(3), 1983, pages 105–112.
  13. 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).
  14. 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).
  15. A Constructive Programming Logic. In Proceedings of the World Computer Congress of the IFIP 77, 1977, pages 733–738.
  16. 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).
  17. Two Types of Hierarchy Theorem for Axiomatic Complexity Classes. In Courant Computer Science Symposium 7, Computational Complexity, Algorithmic Press, NY, 1973, pages 733–738.
  18. 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).
  19. 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).
  20. On Classes of Program Schemata. In SIAM Journal of Computing, Vol. 1(1), 1972, pages 66–118 (with D. Gries).
  21. 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).
  22. Constructive Mathematics and Automatic Program Writers. In Proceedings of the World Computer Congress of the IFIP, 1971, pages 229–233.