Selected Research Publications

• An Epistemic Foundation for Authentication Logics. (With Joe Halpern and Ron van der Meyden.) TARK 2017.
• Knowledge and Security. In Handbook of Epistemic Logic, College Publications, 2015.
• Roles, Stacks, Histories: A Triple for Hoare. (With A. D. Gordon and J. Borgstroem). Journal of Functional Programming 21 (2), pp. 159-207, 2012.
• Modeling Adversaries in a Logic for Security Protocol Analysis. (With J. Y. Halpern). Logical Methods in Computer Science 8 (1:21), pp. 1-26, 2012.
• Practical Affine Types. (With J. A. Tov). In 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'11), 2011.
• Dealing with Logical Omniscience: Expressiveness and Pragmatics. (With J. Halpern). Artificial Intelligence 175 (1), pp. 220-235, 2011.
• Stateful Contracts for Affine Types. (With J. A. Tov). In 19th European Symposium on Programming (ESOP'10), 2010.
• Independence from Obfuscation: A Semantic Framework for Diversity. (With F. B. Schneider). Journal of Computer Security 18 (5), pp. 701-749, 2010.
• Future Contracts. (With C. Dimoulas and M. Felleisen). In 11th International ACM SIGPLAN Symp. on Principles and Practice of Declarative Programming (PPDP'09), 2009.
• Categories of Timed Stochastic Relations. (With D. Brown). In 25th Conf. on the Mathematical Foundations of Programming Semantics (MFPS'09), 2009.
• Evidence with Uncertain Likelihoods. (With J. Halpern). Synthese 171 (1), pp. 111-133, 2009.
• A Runs-and-Systems Semantics for Logics of Announcements. (With M. Sadrzadeh). In 8th Conf. on Logic and the Foundations of Games and Decision Theory (LOFT'08), July 2008.
• Haskell Session Types with (Almost) no Class. (With J. Tov). In 1st SIGPLAN Symp. on Haskell (HASKELL'08), pp. 25-36, 2008.
• Characterizing and Reasoning about Probabilistic and Non-Probabilistic Expectation. (With J. Y. Halpern). Journal of the ACM 54 (3), 2007.
• Deductive Algorithmic Knowledge. Journal of Logic and Computation 16 (2), pp. 287-309, 2006.
• A Logic for Reasoning about Evidence. (With J. Y. Halpern). Journal of Artificial Intelligence Research 26, pp. 1-34, 2006.
• Phantom Types and Subtyping. (With M. Fluet). Journal of Functional Programming 16 (6), pp. 751-791, 2006.
• Probabilistic Algorithmic Knowledge. (With J. Y. Halpern). Logical Methods in Computer Science 1 (3:1), 2005.
• Practical Datatype Specializations with Phantom Types and Recursion Schemes. (With M. Fluet). In 2005 ACM SIGPLAN Workshop on ML, September 2005.
• Validating a Web Service Security Abstraction by Typing. (With A. D. Gordon). Formal Aspects of Computing 17 (3), pp. 277-318, 2005.
• On Partially Additive Kleene Algebras. Full version of paper in 8th Int. Conf. on Relational Methods in Computer Science (RelMiCS 8), February 2005.
• TulaFale: A Security Tool for Web Services. (With K. Bhargavan, C. Fournet, and A. D. Gordon). In 2nd Int. Symp. on Formal Methods for Components and Objects (FMCO'03), November 2003.
• A Coalgebraic Approach to Kleene Algebra with Tests. (With H. Chen). Theoretical Computer Science 327 (1-2), pp. 23-44, 2004.
• A Framework for Creating Natural Language User Interfaces for Action-Based Applications. (With S. Chong). Full version of paper in 3rd Int. AMAST Workshop on Algebraic Methods in Language Processing (AMiLP-3), August 2003.
• A Logic for Reasoning about Digital Rights. (With V. Weissman). In 15th IEEE Computer Security Foundations Workshop (CSFW'02), June 2002.
• A Framework for Interoperability. (With K. Fisher and J. Reppy). In 1st Int. Workshop on Multi-Language Infrastructure and Interoperability (BABEL'01), September 2001.
• A Logic for Reasoning about Upper Probabilities. (With J. Y. Halpern). Journal of Artificial Intelligence Research 17, pp. 57-81, 2002.
• On the Relationship between Strand Spaces and Multi-Agent Systems. (With J. Y. Halpern). ACM Transactions on Information and System Security 6 (1), pp.43-70, 2003.
• On the Expressive Power of First-Order Boolean Functions in PCF. (With P. Panangaden). Theoretical Computer Science 266 (1-2), pp. 543-567, 2001.
• An Analysis of Lambek's Production Machines. RAIRO Informatique Théorique et Applications 31 (5), pp. 483-497, 1997.

Other Technical Writings

• Categories for Imperative Semantics. Lecture Notes for PLDG Seminar, Cornell University, September 2004.
• Reasoning about Resource-Bounded Knowledge: Theory and Application to Security Protocol Analysis. Ph.D. Thesis, Cornell University, August 2004.
• Review of The Pi-Calculus: A Theory of Mobile Processes. SIGACT News 34 (1), March 2003.
• Review of Type-Logical Semantics. (With S. Chong) SIGACT News 34 (1), March 2003.
• Review of Dynamic Logic. SIGACT News 32 (4), December 2001.
• Review of Control Flow Semantics. SIGACT News 32 (3), September 2001.
• Notes on Programming Standard ML of New Jersey. January 2001. (SML/NJ 110.0.6 so pretty obsolete, but may still be useful for some folks.)
• Investigations on Relative Definability in PCF. M.Sc. Thesis, McGill University, August 1996.
• Locally-Adaptive Grid Generation Using Quadtrees. (With C. Verbrugge and P. Panangaden) Technical Report SOCS 95.3, McGill University, June 1995.