Skip to main content
more options

Conference Proceedings (selected)

  1. Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus. In Proceedings of Symposium on Logical Foundations of Computer Science, (LFCS 2009), LNCS 4514, 147–161, Springer, Invited to the special issue of Annals of Pure and Applied Logic, (with Wojciech Moczydlowski).
  2. Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics. In Proceedings of 3rd International Joint Conference on Automated Reasoning (IJCAR 2006), LNCS 4130, 162-176, Springer. Invited to the special issue of Logical Methods in Computer Science (with Wojciech Moczydlowski).
  3. A Graph-Based Approach Towards Discerning Inherent Structures in a Digital Library of Formal Mathematics. In International Conference on Mathematical Knowledge Management, Lecture Notes in Computer Science, editors A. Asperti, G. Bancerek, and A. Trybulec, Springer-Verlag, 2004, pages 220–235 (with L. Lorigo, J. Kleinberg, and R. Eaton).
  4. Knowledge-Based Synthesis of Distributed Systems Using Event Structures. In Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004, Springer, 2005, pages 449–465 (with M. Bickford, J. Halpern, and S. Petride).
  5. An Experiment in Formal Design Using Meta-Properties. In DARPA Information Survivability Conference and Exposition II (DISCEX ’01), Vol. II, IEEE Computer Society Press, 2001, pages 100–107 (with M. Bickford, C. Kreitz, and R. van Renesse).
  6. The Nuprl Open Logical Environment. In 17th International Conference on Automated Deduction, editor D. McAllester, Springer-Verlag, 2000, pages 170–176 (with S. Allen, R. Eaton, C. Kreitz, and L. Lorigo).
  7. Building Reliable, High–Performance Communication Systems from Components. In Proceedings of the 17th ACM Symposium on Operating System Principles, 1999, pages 80–92 (with X. Liu, C. Kreitz, R. van Renesse, J. Hickey, M. Hayden, and K. Birman).
  8. Verbalization of High–Level Formal Proofs. In Sixteenth National Conference on Artificial Intelligence, 1999, pages 277–284 (with R. Barzilay and A. Holland-Minkley).
  9. Creating and Evaluating Interactive Formal Courseware for Mathematics and Computing. In Frontiers in Education, IEEE, editors M. F. Iskander, M. J. Gonzalez, G. L. Engel, C. K. Rushforth, M. A. Yoder, R. W. Grow, and C. H. Durney, Vol. 1, pages 420–423, 1996.
  10. Experience Using Type Theory as a Foundation for Computer Science. In Proceedings of the Tenth Symposium on Logic in Computer Science, IEEE, 1995, pages 266–279.
  11. Meta-Logical Frameworks. In Proceedings of the Second Workshop on Logical Frameworks, Edinburgh, UK, 1991 (with D. Basin).
  12. Extracting Computational Content from Classical Proofs. In Proceedings of the First Annual BRA Workshop on Logical Frameworks, Sophia-Antipolis, France, 1990, pages 141-156.
  13. The Semantics of Reflected Proof. In Proceedings of the Fourth Symposium on Logic in Computer Science, IEEE, May 1990, pages 95–105 (with D. Howe, S. Allen, and W. Aitken).
  14. Computational Foundations of Basic Recursive Function Theory. In Proceedings of the Third Symposium on Logic in Computer Science, IEEE, May 1988, pages 360–371 (with S. Smith).
  15. Partial Objects in Constructive Type Theory. In Proceedings of the Third Symposium on Logic in Computer Science, May 1988, pages 183–193.
  16. Infinite Objects in Type Theory. In Proceedings of the Symposium on Logic in Computer Science, IEEE, Computer Science Press,Washington, DC, 1986, pages 249–257 (with N. P.Mendler and P. Panangaden).
  17. Formalized Metareasoning in Type Theory. In Proceedings of the Symposium on Logic in Computer Science, IEEE, Computer Society Press, Washington, DC, 1986, pages 237–248 (with T. Knoblock).
  18. Recursive Definitions in Type Theory. In Logics of Program, Lecture Notes in Computer Science 193, editor R. Parihk, Springer-Verlag, NY, 1985, pages 61–78 (with N. P. Mendler).
  19. Mathematics as Programming. Proceedings of the Workshop on Programming Logics, Lecture Notes in Computer Science 164, Springer-Verlag, 1983, pages 116–128.
  20. Partial Functions in Constructive Formal Theories. In Proceedings of the Sixth G. I. Conference. Lectures Notes in Computer Science 145, 1983, pages 1–18.
  21. Programs and Types. Proceedings of the 21st IEEE Symposium on the Foundations of Computer Science, 1980, pages 118–128.
  22. A PL/CV precis. In Proceedings of the ACM Symposium on the Principles of Programming Languages, 1979, pages 7–20 (with S. Johnson).
  23. On the Theory of Programming Logics. In Proceedings of the Ninth ACM Symposium on the Theory of Computing, 1977, pages 269–285.