*The versions given here are not necessarily identical to
any of the previously published ones. I believe that the technical contents are
the same. *

*The documents distributed by this server have been provided as a means to
ensure timely dissemination of scholarly and technical work on a noncommercial
basis. Copyright and all rights therein are maintained by the authors or by
other copyright holders, notwithstanding that they have offered their works
here electronically. It is understood that all persons copying this information
will adhere to the terms and constraints invoked by each author's copyright.
These works may not be reposted without the explicit permission of the
copyright holder.*

On Protection by Layout Randomization

[with Gordon Plotkin]

ACM Transactions on Information and System Security 15, 2 (July 2012),
8:1-8:29.

© ACM.

Guessing Attacks and the Computational
Soundness of Static Equivalence

[with Mathieu Baudet and Bogdan Warinschi]

Journal of Computer Security 18, 5 (August 2010), 909-968.

© IOS Press.

Control-Flow Integrity: Principles,
Implementations, and Applications

[with Mihai Budiu, Úlfar Erlingsson, and Jay Ligatti]

ACM Transactions on Information and System Security 13, 1 (October 2009), 1-40.

© ACM

Security Analysis of Cryptographically
Controlled Access to XML Documents

[with Bogdan Warinschi]

Journal of the ACM 55, 2 (May 2008), 6:1-6:29.

© ACM.

Automated Verification of
Selected Equivalences for Security Protocols

[with Bruno Blanchet and Cédric Fournet]

Journal of Logic and Algebraic Programming 75, 1 (February-March 2008), 3-51.

© Elsevier Science.

Just Fast Keying in the Pi
Calculus

[with Bruno Blanchet and Cédric Fournet]

ACM Transactions on Information and System Security 10, 3 (July 2007), 1-59.

© ACM.

Access
Control in a Core Calculus of Dependency

Computation,
Meaning, and Logic: Articles dedicated to Gordon Plotkin, Electronic Notes
in Theoretical Computer Science 172 (April 2007), 5-31.

© Elsevier Science.

Deciding Knowledge
in Security Protocols under Equational Theories

[with Véronique Cortier]

Theoretical Computer Science 367, 1-2 (November 2006), 2-32.

© Elsevier Science.

Computer-Assisted
Verification of a Protocol for Certified Email

[with Bruno Blanchet]

Science of Computer Programming 58, 1-2 (October 2005), 3-27.

© Elsevier Science.

Moderately Hard, Memory-bound Functions

[with Mike Burrows, Mark Manasse, and Edward Wobber]

ACM Transactions on Internet Technology 5, 2 (May 2005), 299-327.

© ACM.

Analyzing
Security Protocols with Secrecy Types and Logic Programs

[with Bruno Blanchet]

Journal of the ACM 52, 1 (January 2005), 102-146.

© ACM.

Private
Authentication

[with Cédric Fournet]

Theoretical Computer Science 322, 3 (September 2004), 427-476.

© Elsevier Science.

Secrecy Types for
Asymmetric Communication

[with Bruno Blanchet]

Theoretical Computer Science 298, 3 (2003), 387-415.

© Elsevier Science.

Reasoning about Secrecy for
Active Networks

[with Pankaj Kakkar and
Carl A. Gunter]

Journal of Computer Security 11, 2 (2003), 245-287.

© IOS Press.

Reconciling Two Views of
Cryptography (The Computational Soundness of Formal Encryption)

[with Phillip Rogaway]

Journal of Cryptology 15, 2 (2002), 103-127.

© Springer-Verlag.

Secure Implementation of Channel Abstractions

[with Cédric Fournet and Georges Gonthier]

Information and Computation 174, 1 (April 2002), 37-83.

The on-line version contains additional
detail.

© Academic Press.

Secrecy
by Typing in Security Protocols

Journal of the ACM 46, 5 (September 1999), 749-786.

© ACM.

A Bisimulation
Method for Cryptographic Protocols

[with Andrew D. Gordon]

Nordic Journal of Computing 5, 4 (Winter 1998), 267-303.

© Publishing Association Nordic Journal of
Computing.

A Calculus for Cryptographic Protocols: The Spi Calculus

[with Andrew D. Gordon]

Information and Computation 148, 1 (January 1999), 1-70.

© Academic Press.

An extended version of this paper appeared as SRC
Research Report 149 (January 1998), and, in preliminary form, as Technical
Report 414,

On SDSI's
Linked Local Name Spaces

Journal of Computer Security 6, 1-2 (1998), 3-21.

(This paper is largely based on SDSI 1.1, by Rivest and Lampson; a copy of
their description of SDSI 1.1 is here.)

© IOS Press.

Explicit Communication Revisited: Two New
Attacks on Authentication Protocols

IEEE Transactions on Software Engineering 23, 3 (March 1997), 185-186.

© IEEE.

Prudent Engineering Practice
for Cryptographic Protocols

[with Roger

IEEE Transactions on Software Engineering 22, 1 (January 1996), 6-15.

© IEEE.

Authentication in
the Taos Operating System

[with Edward Wobber, Michael Burrows, and

ACM Transactions on Computer Systems 12, 1 (February 1994), 3-32.

Also appeared as SRC Research Report 117.

© ACM.

Authentication and
Delegation with Smart-Cards

[with Michael Burrows, Charles Kaufman, and

Science of Computer Programming 21, 2 (October 1993), 93-113.

© Elsevier Science.

A Calculus for Access
Control in Distributed Systems

[with Michael Burrows,

ACM Transactions on Programming Languages and Systems 15, 4 (September 1993),
706-734.

Also appeared as SRC Research Report 70.

© ACM.

Authentication in
Distributed Systems: Theory and Practice

[with

ACM Transactions on Computer Systems 10, 4 (November 1992), 265-310.

Also appeared as SRC Research Report 83.

© ACM.

Secure Circuit
Evaluation: A Protocol Based on Hiding Information from an Oracle

[with Joan Feigenbaum]

Journal of Cryptology 2, 1 (May 1990), 1-12.

© Springer-Verlag.

A Logic of Authentication

[with Michael Burrows and Roger Needham]

Proceedings of the Royal Society, Series A, 426, 1871 (December 1989), 233-271.

Also appeared as SRC Research Report 39 and, in a shortened form, in ACM
Transactions on Computer Systems 8, 1 (February 1990), 18-36.

© Royal Society.

On Hiding Information
from an Oracle

[with Joan Feigenbaum and Joe Kilian]

Journal of Computer and System Sciences 39, 1 (August 1989), 21-50.

© John Wiley & Sons.

[with Anna Leontjeva, Moises Goldszmidt, Yinglian Xie, and Fang Yu]

To appear in 2013 ACM Workshop on Artificial Intelligence and Security (November 2013).

© ACM.

[with Dan Boneh, Ilya Mironov, Ananth Raghunathan, and Gil Segev]

Advances in Cryptology -- CRYPTO 2013, Springer-Verlag (August 2013), 374-391.

© Springer-Verlag.

[with Jérémy Planul and Gordon Plotkin]

To appear in Mathematical Foundations of Programming Semantics---Twenty-ninth Conference (June 2013).

© Elsevier Science.

[with Andrew Birrell, Ilya Mironov, Ted Wobber, and Yinglian Xie]

HotOS XIV: Fourteenth Workshop on Hot Topics in Operating Systems (May 2013).

[with Junxian Huang, Yinglian Xie, Fang Yu, Qifa Ke, Eliot Gillum, and Z. Morley Mao]

Proceedings of the 8th ACM Symposium on Information, Computer and Communications Security (ASIACCS 2013) (May 2013).

© ACM.

[with Jérémy Planul]

Principles of Security and Trust -- Second International Conference, POST 2013, Springer-Verlag (March 2013), 167-185.

© Springer-Verlag.

[with Thomas Austin and Cormac Flanagan]

Proceedings of the Tenth ASIAN Symposium on Programming Languages and Systems -- APLAS 2012, Springer-Verlag (December 2012), 34-49.

© Springer-Verlag.

[with Yinglian Xie, Fang Yu, Qifa Ke, Eliot Gillum, Krish Vitaldevaria, Jason Walter, Junxian Huang, and Z. Morley Mao]

Proceedings of the 19th ACM Conference on Computer and Communications Security (October 2012), 353-364.

© ACM.

FM 2012: 18th International Symposium on Formal Methods, Springer-Verlag (August 2012), 1-5.

© Springer-Verlag.

Host Fingerprinting and Tracking on the Web:
Privacy and Security Implications

[with Ting-Fang Yen, Yinglian Xie, Fang Yu, and Roger Peng Yu]

Proceedings of the 19th Annual Network and Distributed System Security
Symposium (February 2012).

© Internet
Society.

deSEO: Combating
Search-Result Poisoning

[with John P. John, Fang Yu, Yinglian Xie, and Arvind Krishnamurthy]

Proceedings of the 20th USENIX Security Symposium (August 2011), 299-313.

Position Paper: Differential Privacy with
Information Flow Control

[with Arnar Birgisson and Frank McSherry]

Proceedings of ACM SIGPLAN Sixth Workshop on Programming Languages and Analysis
for Security (June 2011).

© ACM.

Heat-seeking Honeypots: Design and Experience

[with John P. John, Fang Yu, Yinglian Xie, and Arvind Krishnamurthy]

Proceedings of the Twentieth International World Wide Web Conference (March
2011), 207-216.

© ACM.

Searching the Searchers with SearchAudit

[with John P. John, Fang Yu, Yinglian Xie, and Arvind Krishnamurthy]

Proceedings of the 19th USENIX Security Symposium (August 2010), 127-142.

On Protection by Layout Randomization

[with Gordon Plotkin]

Proceedings of the 23rd IEEE Computer Security Foundations Symposium (July
2010), 337-351.

The on-line version contains minor
corrections and an additional appendix. This is a preliminary version of a
journal paper (see citation).

© IEEE.

The Fine
Print of Security (Invited Lecture)

Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science
(July 2010), 110.

© IEEE

De-anonymizing
the Internet Using Unreliable IDs

[with Yinglian Xie and Fang Yu]

Proceedings of the ACM SIGCOMM 2009 Conference on Applications, Technologies,
Architectures, and Protocols for Computer Communications (August 2009), 75-86.

© ACM

Models and Proofs of Protocol Security: A
Progress Report

[with Bruno Blanchet and Hubert Comon-Lundh]

Computer Aided Verification, 21^{st} International Conference 2009,
Springer-Verlag (June/July 2009), 35-49.

© Springer-Verlag.

Unified Declarative Platform for Secure
Networked Information Systems

[with Wenchao Zhou, Yun Mao, and Boon Thau Loo]

Proceedings of the 25th International Conference on Data Engineering (March
2009), 150-161.

© IEEE.

Code-Carrying Authorization

[with Sergio Maffeis, Cédric Fournet, and Andrew D. Gordon]

Computer Security -- ESORICS 2008, Springer-Verlag
(October 2008), 563-579.

© Springer-Verlag.

Variations in Access Control
Logic

Ninth International Conference on Deontic Logic in Computer Science (DEON
2008), Springer-Verlag (July 2008), 96-109.

© Springer-Verlag.

A Modal Deconstruction of Access Control
Logics

[with Deepak Garg]

Foundations of Software Science and Computation Structures, FOSSACS 2008,
Springer-Verlag (April 2008), 216-230.

© Springer-Verlag.

Policies and Proofs for Code Auditing

[with Nathan Whitehead and Jordan Johnson]

Automated Technology for Verification and Analysis, 5th International
Symposium, ATVA 2007, Springer-Verlag (October 2007),
1-14.

© Springer-Verlag.

Towards a Declarative Language and System
for Secure Networking

[with Boon Thau Loo]

Proceedings of the Third
International Workshop on Networking Meets Databases (NetDB
'07) (April 2007).

Authorizing Applications in Singularity

[with Ted Wobber, Aydan Yumerefendi,
Andrew Birrell, and Daniel R. Simon]

Proceedings of the EuroSys 2007 Conference (March
2007), 355-368.

© ACM.

XFI: Software Guards for System Address Spaces

[with Mihai Budiu, Úlfar Erlingsson, George Necula, and Michael Vrable]

Proceedings of the 7th USENIX Symposium on Operating Systems Design and
Implementation (November 2006), 75-88.

Computational Secrecy by Typing for the Pi
Calculus

[with Ricardo Corin and Cédric Fournet]

Proceedings of the 4th ASIAN Symposium on Programming Languages and Systems,
Springer-Verlag (November 2006), 253-269.

© Springer-Verlag.

Architectural
Support for Software-Based Protection

[with Mihai Budiu and Úlfar Erlingsson]

Proceedings of the 1st Workshop on Architectural and System Support for
Improving Software Dependability, ASID 2006 (October 2006), 42-51.

© ACM.

Access Control in a Core Calculus of
Dependency

Proceedings of the 2006 ACM International Conference on Functional Programming
(September 2006), 263-273.

This is a preliminary version of a journal paper (see citation).

© ACM.

Formal Analysis of Dynamic, Distributed
File-System Access Controls

[with Avik Chaudhuri]

Formal Methods for Networked and Distributed Systems, FORTE 2006, Springer-Verlag (September 2006), 99-114.

© Springer-Verlag.

Secrecy by Typing and File-Access Control

[with Avik Chaudhuri]

Proceedings of the 19th IEEE Computer Security Foundations Workshop (July
2006), 112-123.

© IEEE.

Guessing Attacks and the Computational
Soundness of Static Equivalence

[with Mathieu Baudet and Bogdan Warinschi]

Foundations of Software Science and Computation Structures, FOSSACS 2006,
Springer-Verlag (March 2006), 398-412.

This is a preliminary version of a journal paper (see citation).

© Springer-Verlag.

Control-Flow Integrity: Principles, Implementations, and Applications

[with Mihai Budiu, Úlfar Erlingsson, and Jay Ligatti]

Proceedings of the 12th ACM Symposium on Computer and Communications Security
(November 2005), 340-353.

This paper is subsumed by a journal paper (see citation).

© ACM.

Formal Security Analysis of Basic Network-Attached
Storage

[with Avik Chaudhuri]

Proceedings of the 2005 ACM Workshop on Formal Methods in Security Engineering
(November 2005), 43-52.

© ACM.

A Theory of Secure Control Flow

[with Mihai Budiu, Úlfar Erlingsson, and Jay Ligatti]

Formal Methods and Software Engineering, 7th International Conference on Formal
Engineering Methods, ICFEM 2005, Springer-Verlag
(July 2005), 111-124.

This paper is subsumed by a journal paper (see citation).

© Springer-Verlag.

Password-Based Encryption Analyzed

[with Bogdan Warinschi]

Automata, Languages and Programming: 25th International Colloquium, ICALP 2005,
Springer-Verlag (July 2005), 664-676.

© Springer-Verlag.

Access
Control in a World of Software Diversity

[with Andrew Birrell and Ted Wobber]

Tenth Workshop on Hot Topics in Operating Systems (HotOS
X) (June 2005), 127-132.

Automated Verification of Selected Equivalences
for Security Protocols

[with Bruno Blanchet and Cédric Fournet]

Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science
(June 2005), 331-340.

This is a preliminary version of a journal paper (see citation).

© IEEE.

Deciding Knowledge in Security
Protocols under (Many More) Equational Theories

[with Véronique Cortier]

Proceedings of the 18th IEEE Computer Security Foundations Workshop (June
2005), 62-76.

This paper is subsumed by a journal paper (see citation).

© IEEE.

Security Analysis of Cryptographically
Controlled Access to XML Documents

[with Bogdan Warinschi]

Proceedings of the 24th ACM Symposium on Principles of Database Systems (June
2005), 108-117.

This is a preliminary version of a journal paper (see citation).

© ACM.

BCiC: A
System for Code Authentication and Verification

[with Nathan Whitehead]

Logic for Programming, Artificial Intelligence, and Reasoning, 11th
International Conference, Springer-Verlag (March
2005), 110-124.

© Springer-Verlag.

Language-Based Enforcement of Privacy Policies

[with Katia Hayati]

Privacy Enhancing Technologies, 4th International Workshop, PET 2004, Revised
Selected Papers, Springer-Verlag (2005), 302-313.

© Springer-Verlag.

A
Logical Account of NGSCB

[with Ted Wobber]

Formal Techniques for Networked and Distributed Systems -- FORTE 2004,
Springer-Verlag (September 2004), 1-12.

© Springer-Verlag.

Trusted Computing, Trusted Third Parties, and Verified Communications

Security and Protection in Information Processing Systems, IFIP 18th World
Computer Congress, TC11 19th International Information Security Conference,
Kluwer (August 2004), 291-308.

The on-line version contains additional detail.

© Kluwer.

Deciding Knowledge in Security
Protocols under Equational Theories

[with Véronique Cortier]

Automata, Languages and Programming: 31st International Colloquium, ICALP 2004,
Springer-Verlag (July 2004), 46-58.

This paper is subsumed by a journal paper (see citation).

© Springer-Verlag.

By Reason and Authority: A System for
Authorization of Proof-Carrying Code

[with Nathan Whitehead and George Necula]

Proceedings of the 17th IEEE Computer Security Foundations Workshop (June
2004), 236-250.

© IEEE.

Just Fast Keying in the Pi Calculus

[with Bruno Blanchet and Cédric Fournet]

Programming Languages and Systems: 13th European Symposium on Programming, ESOP
2004, Springer-Verlag (March 2004), 340-354.

This is a preliminary version of a journal paper (see citation).

© Springer-Verlag.

Bankable Postage for Network Services

[with Andrew Birrell, Mike Burrows, Frank Dabek, and
Ted Wobber]

Advances in Computing Science -- ASIAN 2003, Programming Languages and
Distributed Computation, 8th Asian Computing Science Conference, Springer-Verlag (December 2003), 72-90.

© Springer-Verlag.

Built-in Object Security

Object-Oriented Programming -- ECOOP 2003, Springer-Verlag
(July 2003), 1.

© Springer-Verlag.

Logic in Access Control

Proceedings of the Eighteenth Annual IEEE Symposium on Logic in Computer
Science (June 2003), 228-233.

This is subsumed by a tutorial (see citation).

© IEEE.

Computer-Assisted Verification of a Protocol for Certified Email

[with Bruno Blanchet]

Static Analysis, 10th International Symposium, SAS 2003, Springer-Verlag (June 2003), 316-335.

This is a preliminary version of a journal paper (see citation).

© Springer-Verlag.

Moderately Hard, Memory-bound Functions

[with Mike Burrows, Mark Manasse, and Edward Wobber]

Proceedings of the 10th Annual Network and Distributed System Security
Symposium (February 2003), 25-39.

This is a preliminary version of a journal paper (see citation).

© Internet
Society.

Access Control based on Execution History

[with Cédric Fournet]

Proceedings of the 10th Annual Network and Distributed System Security
Symposium (February 2003), 107-121.

© Internet
Society.

Hiding Names: Private Authentication in the Applied Pi Calculus

[with Cédric Fournet]

Software Security -- Theories and Systems. Mext-NSF-JSPS
International Symposium (ISSS'02), Springer-Verlag
(2003), 317-338.

This paper is subsumed by a journal paper (see citation).

© Springer-Verlag.

Private Authentication

Privacy Enhancing Technologies, Second International Workshop, PET 2002,
Revised Papers, Springer-Verlag (2003), 27-40.

This paper is subsumed by a journal paper (see citation).

© Springer-Verlag.

Certified Email with a Light On-Line Trusted
Third Party: Design and Implementation

[with Neal Glew, Bill Horne, and Benny Pinkas]

Proceedings of the Eleventh International World Wide Web Conference (May 2002),
387-395.

© ACM.

Analyzing Security Protocols with Secrecy Types and Logic Programs

[with Bruno Blanchet]

Proceedings of the 29th ACM Symposium on Principles of Programming Languages
(January 2002), 33-44.

This is a preliminary version of a journal paper (see citation).

© ACM.

Formal Eavesdropping and its Computational Interpretation

[with Jan Jürjens]

Theoretical Aspects of Computer Software, Springer-Verlag
(October 2001), 82-94.

© Springer-Verlag.

Computing
Symbolic Models for Verifying Cryptographic Protocols

[with Marcelo Fiore]

Proceedings of the 14th IEEE Computer Security Foundations Workshop (June
2001), 160-173.

© IEEE.

Secrecy Types for Asymmetric Communication

[with Bruno Blanchet]

Foundations of Software Science and Computation Structures: Fourth
International Conference, FOSSACS 2001, Springer-Verlag
(April 2001), 25-41.

This is a preliminary version of a journal paper (see citation).

Mobile Values, New Names, and
Secure Communication

[with Cédric Fournet]

Proceedings of the 28th ACM Symposium on Principles of Programming Languages
(January 2001), 104-115.

© ACM.

Reconciling Two Views of Cryptography (The Computational Soundness of Formal
Encryption)

[with Phillip Rogaway]

Theoretical Computer Science, Proceedings of the International Conference IFIP
TCS 2000, Springer-Verlag (August 2000), 3-22.

This is a preliminary version of a journal paper (see citation).

© Springer-Verlag.

Taming the Adversary

Advances in Cryptology -- CRYPTO 2000, Springer-Verlag
(August 2000), 353-358.

© Springer-Verlag.

Reasoning about Secrecy for Active Networks

[with Pankaj Kakkar and
Carl A. Gunter]

Proceedings of the 13th IEEE Computer Security Foundations Workshop (July
2000), 118-129.

This is a preliminary version of a journal paper (see citation).

Authentication Primitives
and their Compilation

[with Cédric Fournet and Georges Gonthier]

Proceedings of the 27th ACM Symposium on Principles of Programming Languages
(January 2000), 302-315.

© ACM.

A Top-Down Look at a Secure Message

[with Cédric Fournet and Georges Gonthier]

Proceedings of the 19th International Conference on Foundations of Software
Technology and Theoretical Computer Science, Springer-Verlag
(December 1999), 122-141.

This paper is partly subsumed by the journal paper Secure Implementation of
Channel Abstractions (see citation).

© Springer-Verlag.

Secure Communications Processing for Distributed Languages

[with Cédric Fournet and Georges Gonthier]

Proceedings of the 1999 IEEE Symposium on Security and Privacy (May 1999),
74-88.

This paper is subsumed by the journal paper Secure Implementation of Channel
Abstractions (see citation).

© IEEE.

Secrecy in Programming-Language Semantics

Proceedings of MFPS XV (Mathematical Foundations of Programming Semantics,
Fifteenth Annual Conference), Electronic
Notes in Theoretical Computer Science 20 (April 1999).

Security Protocols and Specifications

Foundations of Software Science and Computation Structures: Second
International Conference, FOSSACS '99 Springer-Verlag
(March 1999), 1-13.

This paper is subsumed by Security Protocols and their Properties (see citation).

© Springer-Verlag.

Protection in Programming-Language
Translations

Automata, Languages and Programming: 25th International Colloquium, ICALP'98,
Springer-Verlag (July 1998), 868-883.

Also appeared as SRC Research Report 154 (April 1998).

© Springer-Verlag.

Secure Implementation of Channel Abstractions

[with Cédric Fournet and Georges Gonthier]

Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer
Science (June 1998), 105-116.

This paper is subsumed by a journal paper (see citation).

© IEEE.

Two Facets of Authentication

Proceedings of the 11th IEEE Computer Security Foundations Workshop (June
1998), 25-32.

Also appeared as SRC Technical Note 1998-007 (March 1998).

This paper is subsumed by Security Protocols and their Properties (see citation).

© IEEE.

Secure Web Tunneling

[with Andrew Birrell, Raymie Stata, and Edward Wobber]

Proceedings of the Seventh International World Wide Web Conference. Computer
Networks and ISDN Systems 30, 1-7 (April 1998), 531-539.

© Elsevier Science.

A Bisimulation Method for Cryptographic Protocols

[with Andrew D. Gordon]

Programming Languages and Systems: 7th European Symposium on Programming, ESOP
'98 (April 1998), 12-26.

This is a preliminary version of a journal paper (see citation).

Secrecy by Typing in Security Protocols

Theoretical Aspects of Computer Software, Springer-Verlag
(September 1997), 611-638.

This is a preliminary version of a journal paper (see citation).

Reasoning about Cryptographic Protocols in the Spi
Calculus

[with Andrew D. Gordon]

CONCUR'97, Springer-Verlag (July 1997), 59-73.

This is a preliminary version of part of a journal paper (see citation).

On SDSI's Linked Local Name Spaces

Proceedings of the 10th IEEE Computer Security Foundations Workshop (June
1997), 98-108.

This is a preliminary version of a journal paper (see citation).

A Calculus for Cryptographic Protocols: The Spi Calculus

[with Andrew D. Gordon]

Proceedings of the 4th ACM Conference on Computer and Communications Security
(April 1997), 36-47.

This is a preliminary version of part of a journal paper (see citation).

Secure Network Objects

[with Leendert van Doorn,
Mike Burrows, and Edward Wobber]

Proceedings of the 1996 IEEE Symposium on Security and Privacy (May 1996),
211-221.

© IEEE.

The Millicent Protocol for Inexpensive
Electronic Commerce

[with Steve Glassman, Mark Manasse, Paul Gauthier, and Patrick Sobalvarro]

World Wide Web Journal -- Fourth International World Wide Web Conference
Proceedings, O'Reilly & Associates, Inc. (December 1995), 603-618.

© O'Reilly &
Associates.

Prudent Engineering Practice for Cryptographic Protocols

[with Roger

Proceedings of the 1994 IEEE Symposium on Security and Privacy (May 1994),
122-136.

Also appeared as SRC Research Report 125.

This is a preliminary version of a journal paper (see citation).

Authentication in the

[with Edward Wobber, Michael Burrows, and

Proceedings of the Fourteenth Symposium on Operating System Principles
(December 1993), 256-269.

This is a preliminary version of a journal paper (see citation).

Authentication in Distributed Systems: Theory and Practice

[with

Proceedings of the Thirteenth Symposium on Operating System Principles (October
1991), 165-182.

This is a preliminary version of a journal paper (see citation).

Authentication and Delegation with Smart-Cards

[with Michael Burrows, Charles Kaufman, and

Theoretical Aspects of Computer Software, Springer-Verlag
(September 1991), 326-345.

Also appeared as SRC Research Report 67.

This is a preliminary version of a journal paper (see citation).

A Calculus for Access Control in Distributed Systems

[with Michael Burrows,

Advances in Cryptology -- CRYPTO '91, Springer-Verlag
(August 1991), 1-23.

This is a preliminary version of a journal paper (see citation).

A Semantics for a Logic of Authentication

[with Mark Tuttle]

Proceedings of the Tenth Annual ACM Symposium on Principles of Distributed
Computing (August 1991), 201-216.

© ACM.

A Logic of Authentication

[with Michael Burrows and Roger Needham]

Proceedings of the Twelfth Symposium on Operating System Principles (December
1989), 1-13.

This is a preliminary version of a journal paper (see citation).

The Scope of a Logic of Authentication

[with Michael Burrows and Roger Needham]

Distributed Computing and Cryptography: Proceedings of a DIMACS Workshop
(October 1989), 119-126.

Also appeared as appendix to SRC Research Report 39.

© American Mathematical Society.

On Generating Solved Instances of Computational
Problems

[with Eric Allender, Andrei Broder, Joan Feigenbaum, and Lane Hemachandra]

Advances in Cryptology -- CRYPTO '88, Springer-Verlag
(August 1988), 297-310.

© Springer-Verlag.

Authentication: A Practical Study in Belief and Action

[with Michael Burrows and Roger Needham]

Proceedings of the 2nd Conference in Theoretical Aspects of Reasoning about
Knowledge, Morgan Kaufmann (March 1988), 325-342.

This paper is subsumed by the journal paper A Logic of Authentication (see citation).

A Simple Protocol for Secure Circuit Evaluation

[with Joan Feigenbaum]

STACS 88, Springer-Verlag (February 1988), 264-272.

This paper is subsumed by the journal paper Secure Circuit Evaluation: A
Protocol Based on Hiding Information from an Oracle (see citation).

On Hiding Information from an Oracle

[with Joan Feigenbaum and Joe Kilian]

Proceedings of the Nineteenth Annual ACM Symposium on the Theory of Computing
(May 1987), 195-203.

This is a preliminary version of a journal paper (see citation).

Informatique
et Sciences Numériques : La Sécurité Informatique

Cours et travaux du Collège de
France, Résumés 2010—2011 (2011), 805-810.

Logic in Access Control (Tutorial Notes)

Foundations of Security Analysis and Design V, FOSAD 2008/2009 Tutorial
Lectures, Springer-Verlag (2009), 145-165.

© Springer-Verlag.

Security Protocols: Principles and
Calculi (Tutorial Notes)

Foundations of Security Analysis and Design IV, FOSAD 2006/2007 Tutorial
Lectures, Springer-Verlag (2007), 1-23.

© Springer-Verlag.

Operating
System Protection against Side-Channel Attacks that Exploit Memory Latency

[with Úlfar Erlingsson]

Microsoft Research Technical Report MSR-TR-2007-117 (August 2007).

An
Overview of the Singularity Project

[with Galen C. Hunt, James R. Larus, Mark Aiken, Paul Barham, Manuel Fähndrich, Chris Hawblitzel, Orion Hodson,
Steven Levi, Nick Murphy, Bjarne Steensgaard,
David Tarditi, Ted Wobber, and Brian Zill]

Microsoft Research Technical Report MSR-TR-2005-135 (October 2005).

On Access Control, Data
Integration, and Their Languages

Computer Systems: Theory, Technology and Applications, A
Tribute to Roger Needham, Springer-Verlag (2004),
9-14.

© Springer-Verlag.

Security Protocols and
their Properties

Foundations of Secure Computation, NATO Science Series, IOS Press (2000),
39-60. Volume for the 20th International Summer School on Foundations of Secure
Computation, held in

© IOS Press.

Strengthening Passwords

[with T. Mark A. Lomas and Roger Needham]

SRC Technical Note 1997-033 (September/December 1997).

(Also in html.)

Formal, Informal, and Null
Methods

Position statement for National Research Council workshop on Information
Systems Trustworthiness (January 1997).

Conjoining
Specifications

[with Leslie Lamport]

ACM Transactions on Programming Languages and Systems 17, 3 (May 1995),
507-534.

Also appeared as SRC Research Report 118.

© ACM.

An Old-Fashioned Recipe
for Real Time

[with Leslie Lamport]

ACM Transactions on Programming Languages and Systems 16, 5 (September 1994), 1543-1571.

Also appeared as SRC Research Report 91.

© ACM.

A Logical View of Composition

[with Gordon Plotkin]

Theoretical Computer Science 114, 1 (June 1993), 3-30.

Also appeared as SRC Research Report 86.

© Elsevier Science.

Composing Specifications

[with Leslie Lamport]

ACM Transactions on Programming Languages and Systems 15, 1 (January 1993),
73-132.

Also appeared as SRC Research Report 66.

© ACM.

Preserving Liveness:
Comments on `Safety and Liveness from a
Methodological Point of View'

[with Bowen Alpern, Krzysztof Apt, Nissim Francez, Shmuel Katz, Leslie Lamport, and Fred Schneider]

Information Processing Letters 40, 3 (November 1991), 141-142.

© Elsevier Science.

The Existence of Refinement Mappings

[with Leslie Lamport]

Theoretical Computer Science 82, 2 (May 1991), 253-284.

Also appeared as SRC Research Report 29.

© Elsevier Science.

Nonclausal Deduction in First-order Temporal Logic

[with Zohar Manna]

Journal of the ACM 37, 2 (April 1990), 279-317.

Temporal Logic Programming

[with Zohar Manna]

Journal of Symbolic Computation 8, 3 (September 1989), 277-295.

The Power of Temporal Proofs

Theoretical Computer Science 65, 1 (June 1989), 35-84. See corrigendum in Theoretical Computer Science 70
(1990), 275.

Also appeared as SRC Research Report 30.

[with Frank McSherry, Derek G. Murray, and Thomas L. Rodeheffer]

2013 IFIP Joint International Conference on Formal Techniques for Distributed Systems, Springer-Verlag (June 2013), 5-19.

© Springer-Verlag.

Leslie Lamport's
Properties and Actions

Proceedings of the Twentieth Annual ACM Symposium on Principles of Distributed
Computing (August 2001), 15.

© ACM.

A TLA Solution to the RPC-Memory
Specification Problem

[with Leslie Lamport and Stephan Merz]

Formal Systems Specification: The RPC-Memory Specification Case Study,
Springer-Verlag (December 1996), 21-66.

© Springer-Verlag.

An Abstract Account of Composition

[with Stephan Merz]

Mathematical Foundations of Computer Science, Springer-Verlag
(August 1995), 499-508.

© Springer-Verlag.

Open Systems in TLA

[with Leslie Lamport]

Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed
Computing (August 1994), 81-90.

This is subsumed by the journal paper Conjoining Specifications (see citation).

© ACM.

Decomposing Specifications of Concurrent Systems

[with Leslie Lamport]

Programming Concepts, Methods and Calculi: Proceedings of the IFIP
TC2/WG2.1/WG2.2/WG2.3 Working Conference on Programming Concepts, Methods and
Calculi, North-Holland (June 1994), 327-340.

This is subsumed by the journal paper Conjoining Specifications (see citation).

An Old-Fashioned Recipe for Real Time

[with Leslie Lamport]

Real-Time: Theory in Practice, Springer-Verlag (June
1991), 1-27.

This is a preliminary version of a journal paper (see citation).

A Logical View of Composition and Refinement

[with Gordon Plotkin]

Proceedings of the Eighteenth Annual ACM Symposium on Principles of Programming
Languages (January 1991), 323-332.

Part of this is a preliminary version of the journal paper A Logical View of
Composition (see citation).

© ACM.

An Axiomatization
of Lamport's Temporal Logic of Actions

CONCUR '90, Springer-Verlag (August 1990), 57-69.

Also appeared as SRC Research Report 65.

© Springer-Verlag.

Realizable and Unrealizable Specifications of
Reactive Systems

[with Leslie Lamport and Pierre Wolper]

Automata, Languages and Programming: 16th International Colloquium, ICALP'89,
Springer-Verlag (July 1989), 1-17.

© Springer-Verlag.

Composing Specifications

[with Leslie Lamport]

Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness,
Springer-Verlag (May 1989), 1-41.

This is a preliminary version of a journal paper (see citation).

The Existence of Refinement Mappings

[with Leslie Lamport]

Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science
(July 1988), 165-177.

This is a preliminary version of a journal paper (see citation).

Temporal Logic Programming

[with Zohar Manna]

Proceedings of the 1987 Symposium on Logic Programming (August 1987), 4-16.

This is a preliminary version of a journal paper (see citation).

The Power of Temporal Proofs

Proceedings of the IEEE Symposium on Logic in Computer Science (June 1987),
123-130.

This is a preliminary version of a journal paper (see citation).

A Timely Resolution

[with Zohar Manna]

Proceedings of the IEEE Symposium on Logic in Computer Science (June 1986),
176-186.

This paper is subsumed by the journal paper Nonclausal
Deduction in First-order Temporal Logic (see citation).

Nonclausal Temporal Deduction

[with Zohar Manna]

Logics of Programs, Springer-Verlag (June 1985),
1-15.

This paper is subsumed by the journal paper Nonclausal
Deduction in First-order Temporal Logic (see citation).

Temporal-Logic Theorem Proving

Doctoral Thesis, Stanford University (March 1987).

On TLA as a Logic

[with Stephan Merz]

Deductive Program Design, NATO ASI Series, Springer-Verlag
(1995), 235-271. Proceedings of the NATO Advanced Study
Institute on Deductive Program Design, held in Marktoberdorf,
Germany (1994).

© Springer-Verlag.

Semantics of Transactional Memory
and Automatic Mutual Exclusion

[with Andrew Birrell, Tim Harris, and Michael Isard]

ACM Transactions on Programming Languages and Systems 33, 1 (January 2011),
2:1-2:50.

© ACM.

A Model of Cooperative Threads

[with Gordon Plotkin]

Logical Methods in Computer Science 6, 4 (October 2010), paper 2, 1-39.

A Model of Dynamic
Separation for Transactional Memory

[with Tim Harris and Katherine F. Moore]

Information and Computation 208, 10 (October 2010), 1093-1117.

© Elsevier.

Types for Safe Locking: Static Race
Detection for Java

[with Cormac Flanagan and Stephen Freund]

ACM Transactions on Programming Languages and Systems 28, 2 (March 2006),
207-255.

© ACM.

TT-Closed Relations and
Admissibility

Mathematical Structures in Computer Science 10, 3 (June 2000), 313-320.

© Cambridge University Press.

A Type System for Java Bytecode Subroutines

[with Raymie Stata]

ACM Transactions on Programming Languages and Systems 21, 1 (January 1999),
90-137.

Also appeared as SRC Research Report 158 (June 1998).

© ACM.

On Subtyping and Matching

[with Luca Cardelli]

ACM Transactions on Programming Languages and Systems 18, 4 (July 1996),
401-423.

See A Theory of Objects.

An Imperative Object Calculus

[with Luca Cardelli]

Theory and Practice of Object Systems 1, 3 (1995), 151-166.

See A Theory of Objects.

A Theory of Primitive Objects: Untyped and First-Order Systems

[with Luca Cardelli]

Information and Computation 125, 2 (March 1996), 78-102.

See A Theory of Objects.

A Theory of Primitive Objects: Second-Order Systems

[with Luca Cardelli]

Science of Computer Programming 25, 2-3 (December 1995), 81-116.

See A Theory of Objects.

Methods as Assertions

[with John Lamping]

Theory and Practice of Object Systems 1, 1 (1995), 5-18.

© John Wiley & Sons.

Dynamic Typing in
Polymorphic Languages

[with Luca Cardelli, Benjamin Pierce, and Didier Rémy]

Journal of Functional Programming 5, 1 (January 1995), 111-130.

Also appeared as SRC Research Report 120.

© Cambridge University Press.

Baby Modula-3 and a Theory of
Objects

Journal of Functional Programming 4, 2 (April 1994), 249-283.

Also appeared as SRC Research Report 95.

© Cambridge University Press.

A Semantics for Static Type Inference in a
Nondeterministic Language

Information and Computation 109, 1-2 (February/March 1994), 300-306.

© Academic Press.

Formal Parametric Polymorphism

[with Luca Cardelli and Pierre-Louis Curien]

Theoretical Computer Science 121, 1-2, A Collection of Contributions in Honour of Corrado Boehm on the
Occasion of his 70th Birthday (December 1993), 9-58.

Also appeared as SRC Research Report 109.

© Elsevier Science.

Explicit Substitutions

[with Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy]

Journal of Functional Programming 1, 4 (October 1991), 375-416.

Also appeared as SRC Research Report 54.

© Cambridge University Press.

Faithful Ideal Models
for Recursive Polymorphic Types

[with Benjamin Pierce and Gordon Plotkin]

International Journal of Foundations of Computer Science 2, 1 (August 1991),
1-21.

© World Scientific Publishing.

Dynamic Typing in a
Statically-Typed Language

[with Luca Cardelli, Benjamin Pierce, and Gordon Plotkin]

ACM Transactions on Programming Languages and Systems 13, 2 (April 1991),
237-268.

Also appeared as SRC Research Report 47.

© ACM.

AC: Composable Asynchronous IO for Native Languages

[with Tim Harris, Rebecca Isaacs, and Ross McIlroy]

Proceedings of the 2011 ACM Conference on Object-Oriented Programming Languages
and Systems (October 2011), 903-920.

© ACM

Perspectives on Transactional Memory

[with Tim Harris]

CONCUR 2009, Springer-Verlag (August 2009), 1-14.

© Springer-Verlag.

Implementation and Use of Transactional
Memory with Dynamic Separation

[with Andrew Birrell, Tim Harris, Johnson Hsieh, and Michael Isard]

International Conference on Compiler Construction 2009, Springer-Verlag (March 2009), 63-77.

© Springer-Verlag.

Transactional Memory with Strong
Atomicity Using Off-the-Shelf Memory Protection Hardware

[with Tim Harris and Mojtaba Mehrara]

Proceedings of the 14th ACM SIGPLAN Symposium on Principles and Practice of
Parallel Programming (February 2009), 185-196.

© ACM

A Model of Cooperative Threads

[with Gordon Plotkin]

Proceedings of the 36th Annual ACM Symposium on Principles of Programming
Languages (January 2009), 29-40.

This is a preliminary version of a journal paper (see citation).

© ACM

A Model of Dynamic Separation for Transactional Memory

[with Tim Harris and Katherine F. Moore]

CONCUR 2008, Springer-Verlag (August 2008), 6-20.

This is a preliminary version of a journal paper (see citation).

© Springer-Verlag.

Semantics of Transactional Memory and Automatic Mutual Exclusion

[with Andrew Birrell, Tim Harris, and Michael Isard]

Proceedings of the 35th Annual ACM Symposium on Principles of Programming Languages
(January 2008), 63-74.

This is a preliminary version of a journal paper (see citation).

© ACM.

Choice in Dynamic Linking

[with Georges Gonthier and Benjamin Werner]

Foundations of Software Science and Computation Structures: Seventh
International Conference, FOSSACS 2004, Springer-Verlag
(March 2004), 12-26.

© Springer-Verlag.

Object Types against Races

[with Cormac Flanagan]

CONCUR'99, Springer-Verlag (August 1999), 288-303.

Parts of this paper are subsumed by a journal paper (see citation).

© Springer-Verlag.

Types for Safe Locking

[with Cormac Flanagan]

Programming Languages and Systems: 8th European Symposium on Programming, ESOP
'99, Springer-Verlag (March 1999), 91-108.

Parts of this paper are subsumed by a journal paper (see citation).

© Springer-Verlag.

A Core Calculus of Dependency

[with Anindya Banerjee, Nevin
Heintze, and Jon G. Riecke]

Proceedings of the 26th Annual ACM Symposium on Principles of Programming
Languages (January 1999), 147-160.

© ACM.

A Type System for Java Bytecode Subroutines

[with Raymie Stata]

Proceedings of the 25th Annual ACM Symposium on Principles of Programming
Languages (January 1998), 149-160.

This is a preliminary version of a journal paper (see citation).

A Logic of Object-Oriented Programs

[with K. Rustan M. Leino]

TAPSOFT '97: Theory and Practice of Software Development, Springer-Verlag (April 1997), 682-696.

© Springer-Verlag.

This is a preliminary version of a paper in a collection (see citation).

Syntactic Considerations on Recursive Types

[with Marcelo Fiore]

Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science
(July 1996), 242-252.

© IEEE.

Analysis and Caching of Dependencies

[with Jean-Jacques Lévy and

Proceedings of the 1996 ACM International Conference on Functional Programming
(May 1996), 83-91.

© ACM.

An Interpretation of Objects and Object Types

[with Luca Cardelli and Ramesh Viswanathan]

Proceedings of the 23rd Annual ACM Symposium on Principles of Programming
Languages (January 1996), 396-409.

See A Theory of Objects.

On Subtyping and Matching

[with Luca Cardelli]

ECOOP '95 -- Object-Oriented Programming, Springer-Verlag
(August 1995), 145-167.

See A Theory of Objects.

An Imperative Object Calculus

[with Luca Cardelli]

TAPSOFT '95: Theory and Practice of Software Development, Springer-Verlag (May 1995), 471-485.

This is a preliminary version of a journal paper (see citation).

See A Theory of Objects.

A Model for Formal Parametric Polymorphism: A PER
Interpretation for System R

[with Roberto Bellucci and Pierre-Louis Curien]

Typed Lambda Calculi and Applications -- TLCA '95, Springer-Verlag
(April 1995), 32-46.

© Springer-Verlag.

An Imperative Object Calculus: Basic Typing and Soundness

[with Luca Cardelli]

SIPL '95 - Proceedings of the Second ACM SIGPLAN Workshop on State in
Programming Languages, Technical Report UIUCDCS-R-95-1900, Department of
Computer Science, University of Illinois at Urbana-Champaign (January 1995),
19-32.

See A Theory of Objects.

Methods as Assertions

[with John Lamping]

Object-Oriented Programming - Eighth European Conference, ECOOP '94, Springer-Verlag (July 1994), 60-80.

This is a preliminary version of a journal paper (see citation).

A Semantics of Object Types

[with Luca Cardelli]

Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science
(July 1994), 332-341.

See A Theory of Objects.

Subtyping and Parametricity

[with Gordon Plotkin and Luca Cardelli]

Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science
(July 1994), 310-319.

© IEEE.

A Theory of Primitive Objects: Second-Order Systems

[with Luca Cardelli]

Programming Languages and Systems -- ESOP '94, Springer-Verlag
(April 1994), 1-25.

This is a preliminary version of a journal paper (see citation).

See A Theory of Objects.

A Theory of Primitive Objects: Untyped and
First-Order Systems

[with Luca Cardelli]

Theoretical Aspects of Computer Software, Springer-Verlag
(April 1994), 296-320.

This is a preliminary version of a journal paper (see citation).

See A Theory of Objects.

Extensible Grammars for Language Specialization

[with Luca Cardelli and Florian Matthes]

Database Programming Languages (DBPL-4), Springer-Verlag
(February 1994), 11-31.

This is a preliminary version of the report Extensible Syntax with Lexical
Scoping (see citation).

A Logic for Parametric Polymorphism

[with Gordon Plotkin]

Typed Lambda Calculi and Applications -- TLCA '93, Springer-Verlag
(March 1993), 361-375.

© Springer-Verlag.

Formal Parametric Polymorphism

[with Luca Cardelli and Pierre-Louis Curien]

Proceedings of the Twentieth Annual ACM Symposium on Principles of Programming
Languages (January 1993), 157-170.

This is a preliminary version of a journal paper (see citation).

Dynamic Typing in Polymorphic Languages

[with Luca Cardelli, Benjamin Pierce, and Didier Rémy]

ACM Sigplan Workshop on ML and its Applications,
Technical Report CMU-CS-93-105,

This is a preliminary version of a journal paper (see citation).

Linear Logic Without Boxes

[with Georges Gonthier and Jean-Jacques Lévy]

Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science
(June 1992), 223-234.

© IEEE.

The Geometry of Optimal Lambda Reduction

[with Georges Gonthier and Jean-Jacques Lévy]

Proceedings of the Nineteenth Annual ACM Symposium on Principles of Programming
Languages (January 1992), 15-26.

© ACM.

A Per Model of Polymorphism and Recursive Types

[with Gordon Plotkin]

Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science
(June 1990), 355-365.

© IEEE.

Explicit Substitutions

[with Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy]

Proceedings of the Sixteenth Annual ACM Symposium on Principles of Programming
Languages (January 1990), 31-46.

This is a preliminary version of a journal paper (see citation).

Faithful Ideal Models for Recursive Polymorphic Types

[with Benjamin Pierce and Gordon Plotkin]

Proceedings of the Fourth Annual IEEE Symposium on Logic in Computer Science
(June 1989), 216-225.

This is a preliminary version of a journal paper (see citation).

Dynamic Typing in a Statically-Typed Language

[with Luca Cardelli, Benjamin Pierce, and Gordon Plotkin]

Proceedings of the Sixteenth Annual ACM Symposium on Principles of Programming
Languages (January 1989), 213-227.

This is a preliminary version of a journal paper (see citation).

Dynamic
Separation for Transactional Memory

[with Andrew Birrell, Tim Harris, Johnson Hsieh, and Michael Isard]

MSR-TR-2008-43 (March 2008).

Automatic Mutual Exclusion and
Atomicity Checks

Concurrency, Graphs and Models: Essays Dedicated to Ugo Montanari on the
Occasion of His 65th Birthday, Springer-Verlag
(2008), 510-526.

© Springer-Verlag.

A Logic of Object-Oriented Programs

[with K. Rustan M. Leino]

Verification: Theory and Practice, Springer-Verlag
(2004), 11-41.

© Springer-Verlag.

Extensible Syntax with
Lexical Scoping

[with Luca Cardelli and Florian Matthes]

SRC Research Report 121 (February 1994).

Decidability
and Expressiveness for First-order Logics of Probability

[with Joe Halpern]

Information and Computation 112, 1 (July 1994), 1-36.

Also appeared as SRC Research Report 73.

© Academic Press.

Naiad: A Timely Dataflow System

[with Derek G. Murray, Frank McSherry, Rebecca Isaacs, Michael Isard, and Paul Barham]

To appear in Proceedings of the 24th ACM Symposium on Operating System Principles (November 2013).

How to Tell an Airport from a Home: Techniques and Applications

[with Andreas Pitsillidis, Yinglian Xie, Fang Yu, Geoffrey M. Voelker, and Stefan Savage]

Proceedings of HotNets-IX: Ninth ACM Workshop on Hot Topics in Networks (October 2010).

Decidability and Expressiveness for First-order Logics of Probability

[with Joe Halpern]

Proceedings of the 30th Annual Symposium on the Foundations of Computer Science
(October 1989), 148-153.

This is a preliminary version of a journal paper (see citation).

Modal Theorem Proving

[with Zohar Manna]

Proceedings of the 8th International Conference on Automated Deduction,
Springer-Verlag (July 1986) 172-189.