Skip to main content
more options

Conference Proceedings (selected)

  1. Developing Correctly Replicated Databases Using Formal Tools. In the 44th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), Atlanta, GA, 2014 (with N. Schiper, V. Rahli, R. van Renesse, and M. Bickford).
  2. A Type Theory with Partial Equivalence Relations as Types. In TYPES 2014: Types for Proofs and Programs, Paris, France, 2014 (with A. Anand, M. Bickford, and V. Rahli).
  3. Inductive Construction in Nuprl Type Theory Using Bar Induction. In TYPES 2014: Types for Proofs and Programs, Paris, France, 2014 (with M. Bickford).
  4. A Diversified and Correct-by-Construction Broadcast Service. Presented at the 2nd International Workshop on Rigorous Protocol Engineering (WRiPE), Austin, TX, 2012 (with V. Rahli, N. Schiper, R. van Renesse, and M. Bickford).
  5. ShadowDB: A Replicated Database on a Synthesized Consensus Core. Presented at the 8th Workshop on Hot Topics in System Dependability (HotDep), Hollywood, CA, 2012 (with N. Schiper, V. Rahli, R. van Renesse, and M. Bickford).
  6. On Building Constructive Formal Theories of Computation Noting the Roles of Turing, Church, and Brouwer. In Proceedings of the 27th Annual ACM/IEEE Symposium on Logic In Computer Science (LICS), Dubrovnik, Croatia, 2012.
  7. Proof Assistants and the Dynamic Nature of Formal Theories. In Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, editors D. Pichardie and T. Weber, Manchester, UK, 2012, pages 1–15.
  8. The Logic of Events, a Framework to Reason about Distributed Systems. Presented at the 2012 Languages for Distributed Algorithms (LADA) Workshop, Philadelphia, PA, 2012 (with M. Bickford and V. Rahli).
  9. Investigating Correct-by-Construction Attack-Tolerant Systems. In Proceedings of the Workshop on Survivability in Cyberspace, Stockholm, 2010 (with M. Bickford and R. van Renesse).
  10. Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus. In Proceedings of Symposium on Logical Foundations of Computer Science (LFCS), 2007, LNCS 4514, 147–161, Springer, Invited to the special issue of Annals of Pure and Applied Logic, (with W. Moczydlowski).
  11. Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics. In Proceedings of the 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 W. Moczydlowski).
  12. 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).
  13. 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).
  14. 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).
  15. 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).
  16. 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).
  17. Verbalization of High–Level Formal Proofs. In Sixteenth National Conference on Artificial Intelligence, 1999, pages 277–284 (with R. Barzilay and A. Holland-Minkley).
  18. 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.
  19. 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.
  20. Meta-Logical Frameworks. In Proceedings of the Second Workshop on Logical Frameworks, Edinburgh, UK, 1991 (with D. Basin).
  21. Extracting Computational Content from Classical Proofs. In Proceedings of the First Annual BRA Workshop on Logical Frameworks, Sophia-Antipolis, France, 1990, pages 141–156.
  22. 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).
  23. 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).
  24. Partial Objects in Constructive Type Theory. In Proceedings of the Third Symposium on Logic in Computer Science, May 1988, pages 183–193.
  25. 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).
  26. 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).
  27. 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).
  28. Mathematics as Programming. Proceedings of the Workshop on Programming Logics, Lecture Notes in Computer Science 164, Springer-Verlag, 1983, pages 116–128.
  29. Partial Functions in Constructive Formal Theories. In Proceedings of the Sixth G. I. Conference. Lectures Notes in Computer Science 145, 1983, pages 1–18.
  30. Programs and Types. Proceedings of the 21st IEEE Symposium on the Foundations of Computer Science, 1980, pages 118–128.
  31. A PL/CV precis. In Proceedings of the ACM Symposium on the Principles of Programming Languages, 1979, pages 7–20 (with S. Johnson).
  32. On the Theory of Programming Logics. In Proceedings of the Ninth ACM Symposium on the Theory of Computing, 1977, pages 269–285.