## Conference Proceedings (selected)

- 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). - 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). - Inductive Construction in Nuprl Type Theory Using Bar Induction. In
*TYPES 2014: Types for Proofs and Programs*, Paris, France, 2014 (with M. Bickford). - 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). - 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). - 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. - 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 115. - 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). - 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). - 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, 147161, Springer, Invited to the special issue of*Annals of Pure and Applied Logic*, (with W. Moczydlowski). - 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, 162176, Springer. Invited to the special issue of*Logical Methods in Computer Science*(with W. Moczydlowski). - 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 220235 (with L. Lorigo, J. Kleinberg, and R. Eaton). - 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 449465 (with M. Bickford, J. Halpern, and S. Petride). - 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 100107 (with M. Bickford, C. Kreitz, and R. van Renesse). - The Nuprl Open Logical Environment. In
*17th International Conference on Automated Deduction*, editor D. McAllester, Springer-Verlag, 2000, pages 170176 (with S. Allen, R. Eaton, C. Kreitz, and L. Lorigo). - Building Reliable, HighPerformance Communication Systems from Components. In
*Proceedings of the 17th ACM Symposium on Operating System Principles*, 1999, pages 8092 (with X. Liu, C. Kreitz, R. van Renesse, J. Hickey, M. Hayden, and K. Birman). - Verbalization of HighLevel Formal Proofs. In
*Sixteenth National Conference on Artificial Intelligence*, 1999, pages 277284 (with R. Barzilay and A. Holland-Minkley). - 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 420423, 1996. - Experience Using Type Theory as a Foundation for Computer Science. In
*Proceedings of the Tenth Symposium on Logic in Computer Science*, IEEE, 1995, pages 266279. - Meta-Logical Frameworks. In
*Proceedings of the Second Workshop on Logical Frameworks*, Edinburgh, UK, 1991 (with D. Basin). - Extracting Computational Content from Classical Proofs. In
*Proceedings of the First Annual BRA Workshop on Logical Frameworks*, Sophia-Antipolis, France, 1990, pages 141156. - The Semantics of Reflected Proof. In
*Proceedings of the Fourth Symposium on Logic in Computer Science*, IEEE, May 1990, pages 95105 (with D. Howe, S. Allen, and W. Aitken). - Computational Foundations of Basic Recursive Function Theory. In
*Proceedings of the Third Symposium on Logic in Computer Science*, IEEE, May 1988, pages 360371 (with S. Smith). - Partial Objects in Constructive Type Theory. In
*Proceedings of the Third Symposium on Logic in Computer Science*, May 1988, pages 183193. - Infinite Objects in Type Theory. In
*Proceedings of the Symposium on Logic in Computer Science*, IEEE, Computer Science Press,Washington, DC, 1986, pages 249257 (with N. P.Mendler and P. Panangaden). - Formalized Metareasoning in Type Theory. In
*Proceedings of the Symposium on Logic in Computer Science*, IEEE, Computer Society Press, Washington, DC, 1986, pages 237248 (with T. Knoblock). - Recursive Definitions in Type Theory. In
*Logics of Program, Lecture Notes in Computer Science*193, editor R. Parihk, Springer-Verlag, NY, 1985, pages 6178 (with N. P. Mendler). - Mathematics as Programming.
*Proceedings of the Workshop on Programming Logics, Lecture Notes in Computer Science*164, Springer-Verlag, 1983, pages 116128. - Partial Functions in Constructive Formal Theories. In
*Proceedings of the Sixth G. I. Conference. Lectures Notes in Computer Science*145, 1983, pages 118. - Programs and Types.
*Proceedings of the 21st IEEE Symposium on the Foundations of Computer Science*, 1980, pages 118128. - A PL/CV precis. In
*Proceedings of the ACM Symposium on the Principles of Programming Languages*, 1979, pages 720 (with S. Johnson). - On the Theory of Programming Logics. In
*Proceedings of the Ninth ACM Symposium on the Theory of Computing*, 1977, pages 269285.