Selected Research Publications
An Epistemic Foundation for Authentication Logics. (With Joe Halpern and Ron van der Meyden.) TARK 2017.
Security. In Handbook of Epistemic Logic,
College Publications, 2015.
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.
Affine Types. (With J. A. Tov). In 38th ACM
SIGPLAN-SIGACT Symposium on Principles of Programming
Languages (POPL'11), 2011.
Logical Omniscience: Expressiveness and
Pragmatics. (With J. Halpern). Artificial
Intelligence 175 (1), pp. 220-235, 2011.
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,
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.
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),
Haskell Session Types with (Almost) no Class. (With
J. Tov). In 1st SIGPLAN Symp. on Haskell (HASKELL'08),
pp. 25-36, 2008.
and Reasoning about Probabilistic and Non-Probabilistic
Expectation. (With J. Y. Halpern). Journal of the
ACM 54 (3), 2007.
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.
and Subtyping. (With M. Fluet). Journal of Functional
Programming 16 (6), pp. 751-791, 2006.
Algorithmic Knowledge. (With J. Y. Halpern). Logical
Methods in Computer Science 1 (3:1), 2005.
Datatype Specializations with Phantom Types and Recursion
Schemes. (With M. Fluet). In 2005 ACM SIGPLAN Workshop
on ML, September 2005.
Web Service Security Abstraction by Typing. (With
A. D. Gordon). Formal Aspects of Computing 17 (3),
pp. 277-318, 2005.
Additive Kleene Algebras. Full version of paper in 8th
Int. Conf. on Relational Methods in Computer Science
(RelMiCS 8), February 2005.
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
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),
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.
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.
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
Review of Type-Logical
Semantics. (With S. Chong) SIGACT News 34 (1), March
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
Locally-Adaptive Grid Generation Using
Quadtrees. (With C. Verbrugge and P. Panangaden) Technical
Report SOCS 95.3, McGill University, June 1995.