| 2014 | CADE | Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics. | Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz |
| 2014 | PODC | An incomplete history of concurrency chapter 1. 1965-1977. | Leslie Lamport |
| 2012 | FM | TLA + Proofs. | Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernn Vanzetto |
| 2010 | CADE | Verifying Safety Properties with the TLA+ Proof System. | Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz |
| 2010 | ICTAC | The TLA | Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz |
| 2009 | ICTAC | The PlusCal Algorithm Language. | Leslie Lamport |
| 2009 | PODC | Vertical paxos and primary-backup replication. | Leslie Lamport, Dahlia Malkhi, Lidong Zhou |
| 2008 | LPAR | A TLA+ Proof System. | Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz |
| 2006 | FORTE | The | Leslie Lamport |
| 2006 | NCA | The +CAL Algorithm Language. | Leslie Lamport |
| 2005 | DSN | How Fast Can Eventual Synchrony Lead to Consensus?. | Partha Dutta, Rachid Guerraoui, Leslie Lamport |
| 2004 | DSN | Recent Discoveries from Paxos. | Leslie Lamport |
| 2004 | DSN | Cheap Paxos. | Leslie Lamport, Mike Massa |
| 2002 | OPODIS | Paxos Made Simple, Fast, and Byzantine. | Leslie Lamport |
| 2000 | PODC | Distributed algorithms in TLA (abstract). | Leslie Lamport |
| 1999 | FM | Cache Coherence Verification with TLA+. | Homayoon Akhiani, Damien Doligez, Paul Harter, Leslie Lamport, Joshua Scheid, Mark R. Tuttle, Yuan Yu |
| 1998 | CONCUR | Reduction in TLA. | Ernie Cohen, Leslie Lamport |
| 1996 | TACAS | Managing Proofs (Abstract). | Leslie Lamport |
| 1994 | FORTE | How good is your specification method? | Leslie Lamport |
| 1994 | PODC | Open Systems in TLA. | Martn Abadi, Leslie Lamport |
| 1993 | CAV | Verification of a Multiplier: 64 Bits and Beyond. | Robert P. Kurshan, Leslie Lamport |
| 1992 | CAV | Mechanical Verification of Concurrent Systems with TLA. | Urban Engberg, Peter Grnning, Leslie Lamport |
| 1992 | CAV | Computer-Hindered Verification (Humans Can Do It Too). | Leslie Lamport |
| 1989 | ICALP | Realizable and Unrealizable Specifications of Reactive Systems. | Martn Abadi, Leslie Lamport, Pierre Wolper |
| 1988 | CONCUR | While Waiting for the Millennium: Formal Specification and Verficiation of Concurrent Systems Now (Abstract). | Leslie Lamport |
| 1988 | LICS | The Existence of Refinement Mappings | Martn Abadi, Leslie Lamport |
| 1988 | PODC | A Lattice-Structured Proof of a Minimum Spanning. | Jennifer L. Welch, Leslie Lamport, Nancy A. Lynch |
| 1985 | POPL | What It Means for a Concurrent Program to Satisfy a Specification: Why No One Has Specified Priority. | Leslie Lamport |
| 1985 | POPL | Constraints: A Uniform Approach to Aliasing and Typing. | Leslie Lamport, Fred B. Schneider |
| 1984 | PODC | Solved Problems, Unsolved Problems and Non-Problems in Concurrency (Invited Address). | Leslie Lamport |
| 1984 | PODC | Byzantine Clock Synchronization. | Leslie Lamport, P. M. Melliar-Smith |
| 1983 | POPL | Reasoning About Nonatomic Operations. | Leslie Lamport |
| 1980 | POPL | "Sometime" is Sometimes "Not Never" - On the Temporal Logic of Programs. | Leslie Lamport |