Leslie Lamport

Emeritus Researcher

Publications

View by:

- Who Builds a House without Drawing Blueprints?
  
  Leslie Lamport
  
  Communications of the ACM | April 2015, Vol 58(4): pp. 38-41
  
  Publication Publication
- Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
  
  Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz
  
  Proceedings of the Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARNL 2014) | May 2014
  
  Publication
- Adaptive Register Allocation with a Linear Number of Registers
  
  Carole Delporte-Gallet, Hugues Fauconnier, Eli Gafni, Leslie Lamport
  
  Proceedings of the 27th International Symposium on Distributed Computing (DISC 2013) | August 2013
  
  Publication
- Why We Should Build Software Like We Build Houses
  
  Leslie Lamport
  
  Wired | January 2013
  
  Publication
- TLA+ Proofs
  
  Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernan Vanzetto
  
  Proceedings of the 18th International Symposium on Formal Methods (FM 2012), Dimitra Giannakopoulou and Dominique Mery, editors. Springer-Verlag Lecture Notes in Computer Science | January 2012, Vol 7436: pp. 147-154
  
  Publication
- Leaderless Byzantine Paxos
  
  Leslie Lamport
  
  Distributed Computing: 25th International Symposium: DISC 2011, David Peleg, editor. | December 2011, pp. 141-142
  
  Publication
- How to Write a 21st Century Proof
  
  Leslie Lamport
  
  Journal of Fixed Point Theory and Applications | November 2011
  
  Publication Publication
- Byzantizing Paxos by Refinement
  
  Leslie Lamport
  
  Distributed Computing: 25th International Symposium: DISC 2011, David Peleg, editor. Springer-Verlag. | June 2011, pp. 211-224
  
  Publication
- Euclid Writes an Algorithm: A Fairytale
  
  Leslie Lamport
  
  International Journal of Software and Informatics 5, 1-2 (2011) | June 2011, Vol 1: pp. 7-20
  
  Publication
- Verifying Safety Properties With the TLA+ Proof System
  
  Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
  
  Fifth International Joint Conference on Automated Reasoning (IJCAR), Edinburgh, UK. | July 2010
  
  Publication
- Computer Science and State Machines
  
  Leslie Lamport
  
  Concurrency, Compositionality, and Correctness (Essays in Honor of Willem-Paul de Roever). Dennis Dams, Ulrich Hannemann, and Martin Steffen editors. Lecture Notes in Computer Science, number 5930 (2010), 60-65. | June 2010, pp. 60-65
  
  Publication
- Vertical Paxos and Primary-Backup Replication
  
  Leslie Lamport, Dahlia Malkhi, Lidong Zhou
  
  MSR-TR-2009-63 | May 2009
  
  Publication
- Vertical Paxos and Primary-Backup Replication
  
  Leslie Lamport, Dahlia Malkhi, Lidong Zhou
  
  The ACM Symposium on Principles of Distributed Computing (PODC 2009) | February 2009
  
  Publication Publication
- Teaching Concurrency
  
  Leslie Lamport
  
  ACM SIGACT News | January 2009, Vol 40(1): pp. 58-62
  
  Publication
- The PlusCal Algorithm Language
  
  Leslie Lamport
  
  Theoretical Aspects of Computing-ICTAC 2009, Martin Leucker and Carroll Morgan editors. Lecture Notes in Computer Science, number 5684, 36-60. | January 2009
  
  Publication
- The Mailbox Problem
  
  Leslie Lamport, Eli Gafni, Marcos K. Aguilera
  
  Proceedings of the International Symposium on Distributed Computing | September 2008
  
  Publication Publication
- A TLA+ Proof System
  
  Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
  
  Proceedings of the LPAR Workshops, CEUR Workshop | August 2008
  
  Publication
- Leslie Lamport: The Specification Language TLA+
  
  Leslie Lamport
  
  In Logics of Specification Languages | 2008 | In Logics of Specification Languages, Dines Bjørner and Martin C. Henson, editors. edition
  
  Editor(s): Dines Bjarner and Martin C. Henson
  
  Publication Publication
- Computation and State Machines
  
  Leslie Lamport
  
  April 2008
  
  Publication
- Stoppable Paxos
  
  Dahlia Malkhi, Leslie Lamport, Lidong Zhou
  
  MSR-TR-2008-192 | April 2008
  
  Publication
- Reconfiguring a State Machine
  
  Leslie Lamport, Dahlia Malkhi, Lidong Zhou
  
  MSR-TR-2008-193 | February 2008
  
  Publication
- Implementing Dataflow With Threads
  
  Leslie Lamport
  
  MSR-TR-2006-181 | December 2006
  
  Publication
- Fast Paxos
  
  Leslie Lamport
  
  Distributed Computing | October 2006, Vol 19: pp. 79-103
  
  Publication
- Checking a Multithreaded Algorithm with +CAL
  
  Leslie Lamport
  
  International Symposium on Distributed Computing (DISC) | September 2006
  
  Publication
- Chapter in Software Specification Methods: An Overview Using a Case Study
  
  Leslie Lamport
  
  Software Specification Methods: An Overview Using a Case Study, TLA+ | Published by Hermes | 2006
  
  Publication
- Measuring Celebrity
  
  Leslie Lamport
  
  Annals of Improbable Research | January 2006, Vol 12: pp. 14-15
  
  Publication
- Real-Time Model Checking is Really Simple
  
  Leslie Lamport
  
  13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods | June 2005
  
  Publication
- How Fast Can Eventual Synchrony Lead to Consensus?
  
  Partha Dutta, Rachid Guerraoui, Leslie Lamport
  
  Proceedings of the International Conference on Dependable Systems and Networks (DSN 2005) | June 2005
  
  Publication
- Generalized Consensus and Paxos
  
  Leslie Lamport
  
  MSR-TR-2005-33 | March 2005
  
  Publication
- Real Time is Really Simple
  
  Leslie Lamport
  
  MSR-TR-2005-30 | March 2005
  
  Publication
- Implementing and Combining Specifications
  
  Leslie Lamport
  
  September 2004
  
  Publication
- Lower Bounds for Asynchronous Consensus
  
  Leslie Lamport
  
  MSR-TR-2004-72 | July 2004
  
  Publication Publication
- Cheap Paxos
  
  Leslie Lamport, Mike Massa
  
  International Conference on Dependable Systems and Networks (DSN 2004) | June 2004
  
  Publication
- Formal Specification of a Web Services Protocol
  
  James E. Johnson, David Langworthy, Leslie Lamport, Friedrich H. Vogt
  
  First International Workshop on Web Services and Formal Methods (WS-FM 2004) | February 2004
  
  Publication
- Consensus on Transaction Commit
  
  Jim Gray, Leslie Lamport
  
  MSR-TR-2003-96 | January 2004
  
  Published by Microsoft
  
  ACM Transactions on Database Systems 31, 1 (2006), 133-160
  
  Publication
- On Hair Color in France
  
  Ellen Gilkerson, Leslie Lamport
  
  January 2004
  
  Publication
- The Future of Computing: Logic or Biology
  
  Leslie Lamport
  
  July 2003
  
  Publication
- Disk Paxos
  
  Eli Gafni, Leslie Lamport
  
  Distributed Computing: 14th International Conference, DISC 2000, Maurice Herlihy, editor. Lecture Notes in Computer Science number 1914, Springer-Verlag, (2000) 330-344. | May 2003
  
  Publication Publication
- Checking Cache-Coherence Protocols with TLA+
  
  Rajeev Joshi, Leslie Lamport, John Matthews, Serdar Tasiran, Mark Tuttle, Yuan Yu
  
  Journal of Formal Methods in System Design | March 2003, Vol 22: pp. 125-131
  
  Publication
- High-Level Specifications: Lessons from Industry
  
  Brannon Batson, Leslie Lamport
  
  Formal Methods for Components and Objects | March 2003
  
  Publication Publication
- Specifying and verifying systems with TLA+
  
  Leslie Lamport, John Matthews, Mark Tuttle, Yuan Yu
  
  Proceedings of the Tenth ACM SIGOPS European Workshop | September 2002
  
  Publication Publication
- A Discussion With Leslie Lamport
  
  Leslie Lamport, Dejan Milojicic
  
  August 2002
  
  An interview in IEEE Distributed Systems Online 3, 8
  
  Publication
- Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers
  
  Leslie Lamport
  
  Published by Addison-Wesley | June 2002
  
  Publication
- Arbiter-Free Synchronization
  
  Leslie Lamport
  
  Distributed Computing | March 2002, Vol 16(3): pp. 219-237
  
  Publication Publication
- The Wildfire Challenge Problem
  
  Leslie Lamport, Madhu Sharma, Mark Tuttle, Yuan Yu
  
  January 2001
  
  Publication
- Paxos Made Simple
  
  Leslie Lamport
  
  ACM SIGACT News (Distributed Computing Column) 32, 4 (Whole Number 121, December 2001) | December 2001, pp. 51-58
  
  Publication
- Fairness and Hyperfairness
  
  Leslie Lamport
  
  Distributed Computing. Also appeared as SRC Research Report 152. A preliminary version of this paper was rejected by Concur 99. | May 2000
  
  Publication
- Archival References to Web Pages
  
  Leslie Lamport
  
  Ninth International World Wide Web Conference: Poster Proceedings | May 2000
  
  Publication
- Lower Bounds on Consensus
  
  Leslie Lamport
  
  March 2000
  
  Publication
- When Does a Correct Mutual Exclusion Algorithm Guarantee Mutual Exclusion
  
  Leslie Lamport, Sharon Perl, William Weihl
  
  Information Processing Letters | March 2000, Vol 76(3): pp. 131-134
  
  Publication
- How (La)TeX changed the face of Mathematics
  
  Leslie Lamport
  
  Mitteilungen der Deutschen Mathematiker-Vereinigung | January 2000, pp. 49-51
  
  Publication
- Model Checking TLA+ Specifications
  
  Yuan Yu, Panagiotis Manolios, Leslie Lamport
  
  In Correct Hardware Design and Verification Methods (CHARME '99), Laurence Pierre and Thomas Kropf editors. Lecture Notes in Computer Science, Springer-Verlag. | June 1999
  
  Publication
- Should Your Specification Language Be Typed?
  
  Leslie Lamport, Lawrence C. Paulson
  
  ACM Transactions on Programming Languages and Systems. Also appeared as SRC Research Report 147. | May 1999, Vol 31(3): pp. 502-526
  
  Publication
- Specifying Concurrent Systems with TLA+
  
  Leslie Lamport
  
  Calculational System Design | April 1999, pp. 183-247
  
  Publication
- A Lazy Caching Proof in TLA
  
  Peter Ladkin, Leslie Lamport, Bryan Olivier, Denis Roegel
  
  Distributed Computing 12 | April 1999, Vol 2(3): pp. 151-174
  
  Publication
- TLA+ Verification of Cache-Coherence Protocols
  
  Homayoon Akhiani, Damien Doligez, Paul Harter, Leslie Lamport, Mark Tuttle, Yuan Yu, Joshua Scheid
  
  February 1999
  
  Publication
- Reduction in TLA
  
  Leslie Lamport, Ernie Cohen
  
  CONCUR'98 Concurrency Theory, David Sangiorgi and Robert de Simone editors. Lecture Notes in Computer Science. | May 1998
  
  Publication Publication
- The Part-Time Parliament
  
  Leslie Lamport
  
  ACM Transactions on Computer Systems 16, 2 (May 1998), 133-169. Also appeared as SRC Research Report 49. This paper was first submitted in 1990, setting a personal record for publication delay that has since been broken by [60]. | May 1998
  
  ACM SIGOPS Hall of Fame Award in 2012
  
  Publication
- Substitution: Syntactic versus Semantic
  
  Leslie Lamport
  
  1998-004 | March 1998
  
  The Fifth Internatinal Conference on Theoretical and Methodological Issues in Machine Translation with special emphasis on: MT in the Next Generation
  
  Publication
- Proving Possibility Properties
  
  Leslie Lamport
  
  Theoretical Computer Science. Also appeared as SRC Research Report 137. | March 1998, Vol 206(2): pp. 341-352
  
  Publication
- Composition: A Way to Make Proofs Harder
  
  Leslie Lamport
  
  Compositionality: The Significant Difference (Proceedings of the COMPOS'97 Symposium), Willem-Paul de Roever, Hans Langmaack, and Amir Pnueli editors. Lecture Notes in Computer Science. | December 1997
  
  Publication
- Marching to Many Distant Drummers
  
  Leslie Lamport, Timothy Mann
  
  May 1997
  
  Publication
- Refinement in State-Based Formalisms
  
  Leslie Lamport
  
  1996-001 | December 1996
  
  Publication
- A TLA Solution to the RPC-Memory Specification Problem
  
  Martin Abadi, Leslie Lamport, Stephan Merz
  
  Formal Systems Specification: The RPC-Memory Specification Case Study, Manfred Broy, Stephan Merz, and Katharina Spies editors. Lecture Notes in Computer Science, number 1169, (1996), 21-66. | November 1996
  
  Publication
- The RPC-Memory Specification Problem: Problem Statement
  
  Manfred Broy, Leslie Lamport
  
  Formal Systems Specification: The RPC-Memory Specification Case Study, Manfred Broy, Stephan Merz, and Katharina Spies editors. Lecture Notes in Computer Science. | August 1996, Vol 1169: pp. 1-4
  
  Publication
- TLA in Pictures
  
  Leslie Lamport
  
  IEEE Transactions on Software Engineering | September 1995, Vol 21(9): pp. 768-775
  
  Publication
- How to Write a Proof
  
  Leslie Lamport
  
  American Mathematical Monthly. Also appeared in Global Analysis in Modern Mathematics, Karen Uhlenbeck, editor. Publish or Perish Press, Houston. Also appeared as SRC Research Report 94. | August 1995, Vol 102(7): pp. 600-608
  
  Publication
- Conjoining Specifications
  
  Martin Abadi, Leslie Lamport
  
  ACM Transactions on Programming Languages and Systems. Also appeared as SRC Research Report 118. | May 1995, Vol 17(3): pp. 507-534
  
  Publication
- Adding “Process Algebra” to TLA
  
  Leslie Lamport
  
  January 1995
  
  Publication
- What Process Algebra Proofs Use Instead of Invariance
  
  Leslie Lamport
  
  January 1995
  
  Publication
- Processes are in the Eye of the Beholder
  
  Leslie Lamport
  
  Theoretical Computer Science SRC Research Report 132 | December 1994, Vol 179: pp. 333-351
  
  Publication
- Introduction to TLA
  
  Leslie Lamport
  
  1994-001 | December 1994
  
  The Annals of Statistics
  
  Publication
- How to Write a Long Formula
  
  Leslie Lamport
  
  FACJ 6(5) (September/October 1994) 580-584. Also appeared as SRC Research Report 119. | September 1994
  
  Publication
- Decomposing Specifications of Concurrent Systems
  
  Leslie Lamport, Martin Abadi
  
  Programming Concepts, Methods and Calculi, Ernst-RÃ¼diger Olderog editor. (Proceedings of the IFIP TC2/WG2.1/WG2.2/WG2.3 Working Conference, Procomet '94, San Miniato, Italy.) North-Holland | August 1994
  
  Publication
- Open Systems in TLA
  
  Martin Abadi, Leslie Lamport
  
  Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing | August 1994
  
  Publication
- Specifying and Verifying Fault-Tolerant Systems
  
  Leslie Lamport
  
  Formal Techniques in Real-Time and Fault-Tolerant Systems, H. Langmaack, W.-P. de Roever, J. Vytopil editors. Lecture Notes in Computer Science, Springer-Verlag | July 1994
  
  Publication
- TLZ (Abstract)
  
  Leslie Lamport
  
  Z User's Workshop, Cambridge. J.P. Bowen and J.A. Hall (Eds.) | May 1994
  
  Publication
- The Temporal Logic of Actions
  
  Leslie Lamport
  
  79 | May 1994
  
  Published by Microsoft
  
  ACM Transactions on Programming Languages and Systems 16
  
  Publication
- Composing Specifications
  
  Leslie Lamport, Martin Abadi
  
  ACM Transactions on Programming Languages and Systems 15, 1 (January 1993), 73-132. Also appeared as SRC Research Report 66. A preliminary version appeared in Stepwise Refinement of Distributed Systems, J. W. de Bakker, W.-P. de Roever, and G. Rozenberg editors, Springer-Verlag Lecture Notes in Computer Science Volume 430 (1989), 1-41. | July 1993
  
  Publication
- Verification of a Multiplier: 64 Bits and Beyond
  
  Leslie Lamport
  
  Computer-Aided Verification, Costas Courcoubetis, editor. (Proceedings of the Fifth International Conference, CAV'93.) Lecture Notes in Computer Science, number 697, Springer-Verlag (June, 1993), 166-179. | July 1993
  
  Publication
- Verification and Specification of Concurrent Programs
  
  Leslie Lamport
  
  A Decade of Concurrency: Reflections and Perspectives, J. W. de Bakker, W.-P. de Roever, and G. Rozenberg editors. Lecture Notes in Computer Science, number 803, Springer-Verlag, (June, 1993) 347-374. | June 1993
  
  Publication
- Hybrid Systems in TLA+
  
  Leslie Lamport
  
  Hybrid Systems, Robert L. Grossman, Anil Nerode, Hans Rischel, and Anders P. Ravn, editors. Lecture Notes in Computer Science, Springer-Verlag | 1993, Vol 736 | Hybrid Systems, Robert L. Grossman, Anil Nerode, Hans Rischel, and Anders P. Ravn, editors. Lecture Notes in Computer Science, Springer-Verlag edition
  
  Publication
- How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor
  
  Leslie Lamport
  
  IEEE Transactions on Computers SRC Research Report 96 | February 1993, Vol 46(7): pp. 779-782
  
  Publication
- Critique of the Lake Arrowhead Three
  
  Leslie Lamport
  
  Distributed Computing | August 1992, pp. 65-71
  
  Publication
- Mechanical Verification of Concurrent Systems with TLA
  
  Urban Engberg, Peter Gronning, Leslie Lamport
  
  Computer-Aided Verification, G. v. Bochmann and D. K. Probst editors. (Proceedings of the Fourth International Conference, CAV'92.) Lecture Notes in Computer Science, number 663, Springer-Verlag, (June, 1992) 44-55. | June 1992
  
  Publication
- The Reduction Theorem
  
  Leslie Lamport
  
  April 1992
  
  Publication
- An Old-Fashioned Recipe for Real Time
  
  Martin Abadi, Leslie Lamport
  
  Proceedings of REX Workshop "Real-Time: Theory in Practice", Mook, The Netherlands, June 1991 | January 1992
  
  Publication
- Preserving Liveness: Comments on “Safety and Liveness from a Methodological Point of View”
  
  Martin Abadi, Bowen Alpern, Krzysztof R. Apt, Nissim Francez, Shmuel Katz, Leslie Lamport, Fred B. Schneider
  
  Information Processing Letters | November 1991, Vol 40(3): pp. 141-142
  
  Publication
- The Concurrent Reading and Writing of Clocks
  
  Leslie Lamport
  
  ACM Transactions on Computer Systems. Also appeared as SRC Research Report 27. | November 1990, pp. 305-310
  
  Publication
- A Completeness Theorem for TLA
  
  Leslie Lamport
  
  October 1990
  
  Publication
- The Mutual Exclusion Problem Has Been Solved
  
  Leslie Lamport
  
  Communications of the ACM | September 1990, Vol 34(1): pp. 110
  
  Publication
- A Theorem on Atomicity in Distributed Algorithms
  
  Leslie Lamport
  
  Distributed Computing. Also appeared as SRC Research Report 28. | August 1990, Vol 4(2): pp. 59-68
  
  Publication
- Distributed Computing: Models and Methods
  
  Leslie Lamport, Nancy Lynch
  
  Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, Jan van Leeuwen, editor, Elsevier | August 1990, pp. 1157-1199
  
  Publication
- win and sin: Predicate Transformers for Concurrency
  
  Leslie Lamport
  
  ACM Transactions on Programming Languages and Systems. Also appeared as SRC Research Report 17 (May 1987). | July 1990
  
  Publication
- Realizable and Unrealizable Specifications of Reactive Systems
  
  Martin Abadi, Leslie Lamport, Pierre Wolper
  
  Automata, Languages and Programming, Springer-Verlag | July 1989, pp. 1-17
  
  Publication
- Pretending Atomicity
  
  Leslie Lamport, Fred B. Schneider
  
  SRC Research Report 44 | May 1989
  
  Publication
- A Simple Approach to Specifying Concurrent Systems
  
  Leslie Lamport
  
  Proc. of ACM SIGCOMM. Communications of the ACM 32. Also appeared as SRC Research Report 15. | January 1989
  
  Publication
- A Lattice-Structured Proof of a Minimum Spanning Tree Algorithm
  
  Jennifer Lundelius Welch, Leslie Lamport, Nancy Lynch
  
  Proceedings of the Seventh Annual ACM Symposium on Principles of Distributed Computing | August 1988
  
  Publication
- Another Position Paper on Fairness
  
  Fred B. Schneider, Leslie Lamport
  
  Software Engineering Notes | July 1988, Vol 13(3): pp. 1-2
  
  Publication
- The Existence of Refinement Mappings
  
  Martin Abadi, Leslie Lamport
  
  Proceedings of the 3rd Annual Symposium on Logic in Computer Science | July 1988
  
  LICS 1988 Test of Time Award
  
  Publication
- “EWD 1013”
  
  Leslie Lamport
  
  April 1988
  
  Publication
- Control Predicates Are Better than Dummy Variables for Representing Program Control
  
  Leslie Lamport
  
  ACM Transactions on Programming Languages and Systems. Also appeared as SRC Research Report 11. | April 1988, pp. 267-281
  
  Publication
- Synchronizing Time Servers
  
  Leslie Lamport
  
  | August 1987
  
  The ACM Conference on Human Factors in Computing Systems Workshop on Sensemaking (CHI 2008)
  
  Publication
- The Byzantine Generals
  
  Danny Dolev, Leslie Lamport, Marshall Pease, Robert Shostak
  
  Concurrency Control and Reliability in Distributed Systems, Bharat K. Bhargava, editor, Van Nostrand Reinhold | July 1987, pp. 348-369
  
  Publication
- Document Production: Visual or Logical?
  
  Leslie Lamport
  
  Notices of the American Mathematical Society. | June 1987, pp. 621-624
  
  Publication
- Distribution
  
  Leslie Lamport
  
  May 1987
  
  Email message sent to a DEC SRC bulletin board at 12:23:29 PDT on 28 May 87.
  
  Publication
- A Formal Basis for the Specification of Concurrent Systems
  
  Leslie Lamport
  
  In Distributed Operating Systems: Theory and Practice, Paker, Banatre and Bozyigit, editors, Springer-Verlag | April 1987, pp. 1-46
  
  Publication
- Derivation of a Simple Synchronization Algorithm
  
  Leslie Lamport
  
  February 1987
  
  Publication
- The Mutual Exclusion Problem – Part I: A Theory of Interprocess Communication
  
  Leslie Lamport
  
  Journal of the Association for Computing Machinery | January 1986, Vol 33(2): pp. 313-348
  
  Publication
- The Mutual Exclusion Problem – Part II: Statements and Solutions
  
  Leslie Lamport
  
  Journal of the Association for Computing Machinery | January 1986, Vol 33(2): pp. 313-348
  
  Publication
- On Interprocess Communication-Part I: Basic Formalism, Part II: Algorithms
  
  Leslie Lamport
  
  Distributed Computing. Also appeared as SRC Research Report 8. | December 1985, pp. 77-101
  
  Publication Publication
- A Fast Mutual Exclusion Algorithm
  
  Leslie Lamport
  
  ACM Transactions on Computer Systems 5, 1 (February 1987), 1-11. Also appeared as SRC Research Report 7. | November 1985, pp. 1-11
  
  Publication
- An Axiomatic Semantics of Concurrent Programming Languages
  
  Leslie Lamport
  
  Logics and Models of Concurrent Systems, Krzysztof Apt, editor. Springer-Verlag, Berlin | August 1985, pp. 77-122
  
  Publication
- Distributed Snapshots: Determining Global States of a Distributed System
  
  K. Mani Chandy, Leslie Lamport
  
  ACM Transactions on Computer Systems | February 1985, pp. 63-75
  
  Publication
- Synchronizing Clocks in the Presence of Faults
  
  Leslie Lamport, P. M. Melliar-Smith
  
  Journal of the Association for Computing Machinery | January 1985, Vol 32(1): pp. 52-78
  
  Publication
- What It Means for a Concurrent Program to Satisfy a Specification: Why No One Has Specified Priority
  
  Leslie Lamport
  
  Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages, ACM SIGACT-SIGPLAN | January 1985
  
  Publication
- Buridan’s Principle
  
  Leslie Lamport
  
  Foundations of Physics | October 1984, Vol 42(8): pp. 1056-1066
  
  Publication
- On a “Theorem” of Peterson
  
  Leslie Lamport
  
  October 1984
  
  Publication
- Solved Problems, Unsolved Problems and NonProblems in Concurrency
  
  Leslie Lamport
  
  Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing | August 1984
  
  Publication
- Byzantine Clock Synchronization
  
  Leslie Lamport, Michael Melliar-Smith
  
  Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing | August 1984
  
  Publication
- Recursive Compiling and Programming Environments (Summary)
  
  Leslie Lamport
  
  July 1984 | Rejected from the 1985 POPL Conference edition edition
  
  Rejected from the 1985 POPL Conference
  
  Publication
- Constraints: A Uniform Approach to Aliasing and Typing
  
  Leslie Lamport, Fred B. Schneider
  
  Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages, ACM SIGACT-SIGPLAN | July 1984
  
  Publication
- The Hoare Logic Of CSP, and All That
  
  Leslie Lamport
  
  ACM Transactions on Programming Languages and Systems | April 1984, pp. 281-296
  
  Publication
- Using Time Instead of Timeout for Fault-Tolerant Distributed Systems
  
  Leslie Lamport
  
  ACM Transactions on Programming Languages and Systems | April 1984, pp. 254-280
  
  Publication
- The Weak Byzantine Generals Problem
  
  Leslie Lamport
  
  Journal of the Association for Computing Machinery | June 1983, Vol 30(3): pp. 668-676
  
  Publication
- What Good Is Temporal Logic?
  
  Leslie Lamport
  
  Information Processing 83, R. E. A. Mason, ed., Elsevier Publishers | May 1983, Vol 83: pp. 657-668
  
  Publication
- Specifying Concurrent Program Modules
  
  Leslie Lamport
  
  ACM Transactions on Programming Languages and Systems | April 1983, pp. 190-222
  
  Publication
- Reasoning About Nonatomic Operations
  
  Leslie Lamport
  
  Proceedings of the Tenth ACM Symposium on Principles of Programming Languages, ACM SIGACT-SIGPLAN | January 1983
  
  Publication
- An Assertional Correctness Proof of a Distributed Program
  
  Leslie Lamport
  
  Science of Computer Programming | December 1982, pp. 175-206
  
  Publication
- The Byzantine Generals Problem
  
  Leslie Lamport, Robert Shostak, Marshall Pease
  
  ACM Transactions on Programming Languages and Systems | July 1982, pp. 382-401
  
  Publication
- Proving Liveness Properties of Concurrent Programs
  
  Leslie Lamport, Susan Owicki
  
  ACM Transactions on Programming Languages and Systems | July 1982, Vol 4(3): pp. 455-495
  
  Publication
- Byzantine Generals and Transaction Commit Protocols
  
  Leslie Lamport, Michael Fischer
  
  April 1982
  
  Publication
- Password Authentication with Insecure Communication
  
  Leslie Lamport
  
  Communications of the ACM 24 | November 1981, pp. 770-772
  
  Publication
- Reaching Agreement in the Presence of Faults
  
  Marshall Pease, Robert Shostak, Leslie Lamport
  
  Journal of the Association for Computing Machinery 27 | April 1980, Vol 2
  
  2005 Edsger W. Dijkstra Prize in Distributed Computing
  
  Publication
- Sometime’ is Sometimes ‘Not Never’
  
  Leslie Lamport
  
  Proceedings of the Seventh ACM Symposium on Principles of Programming Languages, ACM SIGACT-SIGPLAN | January 1980
  
  Publication
- Letter to the Editor
  
  Leslie Lamport
  
  Communications of the ACM 22 | November 1979, Vol 11: pp. 624
  
  Publication
- Constructing Digital Signatures from a One Way Function
  
  Leslie Lamport
  
  CSL-98 | October 1979
  
  This paper was published by IEEE in the Proceedings of HICSS-43 in January, 2010.
  
  Publication
- On the Proof of Correctness of a Calendar Program
  
  Leslie Lamport
  
  Communications of the ACM 22 | October 1979, Vol 10: pp. 554-556
  
  Publication
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
  
  Leslie Lamport
  
  IEEE Transactions on Computers C-28 | September 1979, Vol 9: pp. 690-691
  
  Publication
- How to Present a Paper
  
  Leslie Lamport
  
  August 1979
  
  Publication
- A New Approach to Proving the Correctness of Multiprocess Programs
  
  Leslie Lamport
  
  ACM Transactions on Programming Languages and Systems 1 | July 1979, Vol 1: pp. 84-97
  
  Publication Publication
- A General Construction for Expressing Repetition
  
  Leslie Lamport
  
  ACM SIGPLAN Notices 14 | March 1979, Vol 3: pp. 38-42
  
  Publication
- On-the-fly Garbage Collection: an Exercise in Cooperation
  
  Edsger W. Dijkstra, Leslie Lamport, A. J. Martin, C. S. Scholten, E. F. M. Steffens
  
  Communications of the ACM 21 | November 1978, Vol 11: pp. 966-975
  
  Publication
- SIFT: Design and Analysis of a Fault-Tolerant Computer for Aircraft Control
  
  John H. Wensley, Leslie Lamport, Jack Goldberg, Milton W. Green, Karl N. Levitt, P. M. Melliar-Smith, Robert E. Shostak, Charles B. Weinstock
  
  Proceedings of the IEEE 66 | October 1978
  
  Publication
- The Implementation of Reliable Distributed Multiprocess Systems
  
  Leslie Lamport
  
  Computer Networks | August 1978, Vol 2: pp. 95-114
  
  Publication
- Time, Clocks and the Ordering of Events in a Distributed System
  
  Leslie Lamport
  
  Communications of the ACM 21, 7 (July 1978), 558-565. Reprinted in several collections, including Distributed Computing: Concepts and Implementations, McEntire et al., ed. IEEE Press, 1984. | July 1978, pp. 558-565
  
  2000 PODC Influential Paper Award (later renamed the Edsger W. Dijkstra Prize in Distributed Computing). Also awarded an ACM SIGOPS Hall of Fame Award in 2007.
  
  Publication
- State the Problem Before Describing the Solution
  
  Leslie Lamport
  
  ACM SIGSOFT Software Engineering Notes | January 1978, pp. 26
  
  Publication
- On Concurrent Reading and Writing
  
  Leslie Lamport
  
  Communications of the ACM 20 | November 1977, Vol 11: pp. 806-811
  
  Publication
- Proving the Correctness of Multiprocess Programs
  
  Leslie Lamport
  
  IEEE Transactions on Software Engineering SE-3 | March 1977, Vol 2: pp. 125-143
  
  Publication
- How to Tell a Program from an Automobile
  
  Leslie Lamport
  
  In A Dynamic and Quick Intellect, John Tromp editor (1996)--a Liber Amicorum issued by the CWI in honor of Paul Vitanyi's 25-year jubilee. | January 1977
  
  Publication
- On the Glitch Phenomenon
  
  Leslie Lamport, Richard Palais
  
  November 1976 | Rejected by IEEE Transactions on Computers (November 1976). edition edition
  
  Rejected by IEEE Transactions on Computers (November 1976).
  
  Publication
- Multiple Byte Processing with Full-Word Instructions
  
  Leslie Lamport
  
  Communications of the ACM | August 1975, Vol 18(8): pp. 471-475
  
  Publication
- On Self-stabilizing Systems
  
  Leslie Lamport
  
  CA 7412-0511 | December 1974
  
  Publication
- A New Solution of Dijkstra’s Concurrent Programming Problem
  
  Leslie Lamport
  
  Communications of the ACM 17 | August 1974
  
  Publication
- The Parallel Execution of DO Loops
  
  Leslie Lamport
  
  Communications of the ACM 17 | February 1974, Vol 2: pp. 83-93
  
  Publication
- An Extension of a Theorem of Hamada on the Cauchy Problem with Singular Data
  
  Leslie Lamport
  
  American Mathematical Society | July 1973, Vol 174(4): pp. 776
  
  Publication
- The Analytic Cauchy Problem with Singular Data
  
  Leslie Lamport
  
  May 1972
  
  PhD Thesis: Brandeis University | May 1972
  
  Publication
- Comment on Bell’s Quadratic Quotient Algorithm
  
  Leslie Lamport
  
  Communications of the ACM | September 1970, Vol 13(9)
  
  Publication
- Summer Vision Programs
  
  Leslie Lamport
  
  October 1966
  
  Massachusetts Institute of Technology, Project MAC Memorandum MAC-M-332, Artificial Intelligence Project Memo Number Vision 111
  
  Publication
- Braid Theory
  
  Leslie Lamport, Jackson Wright, Neal Plotkin, Robert Teitel, Martin Wenglinsky
  
  November 1957
  
  Publication

- The Wildfire Challenge Problem
  
  Leslie Lamport, Madhu Sharma, Mark Tuttle, Yuan Yu
  
  January 2001
  
  Publication
- Fairness and Hyperfairness
  
  Leslie Lamport
  
  Distributed Computing. Also appeared as SRC Research Report 152. A preliminary version of this paper was rejected by Concur 99. | May 2000
  
  Publication
- Archival References to Web Pages
  
  Leslie Lamport
  
  Ninth International World Wide Web Conference: Poster Proceedings | May 2000
  
  Publication
- Lower Bounds on Consensus
  
  Leslie Lamport
  
  March 2000
  
  Publication
- When Does a Correct Mutual Exclusion Algorithm Guarantee Mutual Exclusion
  
  Leslie Lamport, Sharon Perl, William Weihl
  
  Information Processing Letters | March 2000, Vol 76(3): pp. 131-134
  
  Publication
- How (La)TeX changed the face of Mathematics
  
  Leslie Lamport
  
  Mitteilungen der Deutschen Mathematiker-Vereinigung | January 2000, pp. 49-51
  
  Publication
- Model Checking TLA+ Specifications
  
  Yuan Yu, Panagiotis Manolios, Leslie Lamport
  
  In Correct Hardware Design and Verification Methods (CHARME '99), Laurence Pierre and Thomas Kropf editors. Lecture Notes in Computer Science, Springer-Verlag. | June 1999
  
  Publication
- Should Your Specification Language Be Typed?
  
  Leslie Lamport, Lawrence C. Paulson
  
  ACM Transactions on Programming Languages and Systems. Also appeared as SRC Research Report 147. | May 1999, Vol 31(3): pp. 502-526
  
  Publication
- Specifying Concurrent Systems with TLA+
  
  Leslie Lamport
  
  Calculational System Design | April 1999, pp. 183-247
  
  Publication
- A Lazy Caching Proof in TLA
  
  Peter Ladkin, Leslie Lamport, Bryan Olivier, Denis Roegel
  
  Distributed Computing 12 | April 1999, Vol 2(3): pp. 151-174
  
  Publication
- TLA+ Verification of Cache-Coherence Protocols
  
  Homayoon Akhiani, Damien Doligez, Paul Harter, Leslie Lamport, Mark Tuttle, Yuan Yu, Joshua Scheid
  
  February 1999
  
  Publication
- Reduction in TLA
  
  Leslie Lamport, Ernie Cohen
  
  CONCUR'98 Concurrency Theory, David Sangiorgi and Robert de Simone editors. Lecture Notes in Computer Science. | May 1998
  
  Publication Publication
- The Part-Time Parliament
  
  Leslie Lamport
  
  ACM Transactions on Computer Systems 16, 2 (May 1998), 133-169. Also appeared as SRC Research Report 49. This paper was first submitted in 1990, setting a personal record for publication delay that has since been broken by [60]. | May 1998
  
  ACM SIGOPS Hall of Fame Award in 2012
  
  Publication
- Substitution: Syntactic versus Semantic
  
  Leslie Lamport
  
  1998-004 | March 1998
  
  The Fifth Internatinal Conference on Theoretical and Methodological Issues in Machine Translation with special emphasis on: MT in the Next Generation
  
  Publication
- Proving Possibility Properties
  
  Leslie Lamport
  
  Theoretical Computer Science. Also appeared as SRC Research Report 137. | March 1998, Vol 206(2): pp. 341-352
  
  Publication
- Composition: A Way to Make Proofs Harder
  
  Leslie Lamport
  
  Compositionality: The Significant Difference (Proceedings of the COMPOS'97 Symposium), Willem-Paul de Roever, Hans Langmaack, and Amir Pnueli editors. Lecture Notes in Computer Science. | December 1997
  
  Publication
- Marching to Many Distant Drummers
  
  Leslie Lamport, Timothy Mann
  
  May 1997
  
  Publication
- Refinement in State-Based Formalisms
  
  Leslie Lamport
  
  1996-001 | December 1996
  
  Publication
- A TLA Solution to the RPC-Memory Specification Problem
  
  Martin Abadi, Leslie Lamport, Stephan Merz
  
  Formal Systems Specification: The RPC-Memory Specification Case Study, Manfred Broy, Stephan Merz, and Katharina Spies editors. Lecture Notes in Computer Science, number 1169, (1996), 21-66. | November 1996
  
  Publication
- The RPC-Memory Specification Problem: Problem Statement
  
  Manfred Broy, Leslie Lamport
  
  Formal Systems Specification: The RPC-Memory Specification Case Study, Manfred Broy, Stephan Merz, and Katharina Spies editors. Lecture Notes in Computer Science. | August 1996, Vol 1169: pp. 1-4
  
  Publication
- TLA in Pictures
  
  Leslie Lamport
  
  IEEE Transactions on Software Engineering | September 1995, Vol 21(9): pp. 768-775
  
  Publication
- How to Write a Proof
  
  Leslie Lamport
  
  American Mathematical Monthly. Also appeared in Global Analysis in Modern Mathematics, Karen Uhlenbeck, editor. Publish or Perish Press, Houston. Also appeared as SRC Research Report 94. | August 1995, Vol 102(7): pp. 600-608
  
  Publication
- Conjoining Specifications
  
  Martin Abadi, Leslie Lamport
  
  ACM Transactions on Programming Languages and Systems. Also appeared as SRC Research Report 118. | May 1995, Vol 17(3): pp. 507-534
  
  Publication
- Adding “Process Algebra” to TLA
  
  Leslie Lamport
  
  January 1995
  
  Publication
- Processes are in the Eye of the Beholder
  
  Leslie Lamport
  
  Theoretical Computer Science SRC Research Report 132 | December 1994, Vol 179: pp. 333-351
  
  Publication
- Introduction to TLA
  
  Leslie Lamport
  
  1994-001 | December 1994
  
  The Annals of Statistics
  
  Publication
- How to Write a Long Formula
  
  Leslie Lamport
  
  FACJ 6(5) (September/October 1994) 580-584. Also appeared as SRC Research Report 119. | September 1994
  
  Publication
- Open Systems in TLA
  
  Martin Abadi, Leslie Lamport
  
  Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing | August 1994
  
  Publication
- Decomposing Specifications of Concurrent Systems
  
  Leslie Lamport, Martin Abadi
  
  Programming Concepts, Methods and Calculi, Ernst-RÃ¼diger Olderog editor. (Proceedings of the IFIP TC2/WG2.1/WG2.2/WG2.3 Working Conference, Procomet '94, San Miniato, Italy.) North-Holland | August 1994
  
  Publication
- Specifying and Verifying Fault-Tolerant Systems
  
  Leslie Lamport
  
  Formal Techniques in Real-Time and Fault-Tolerant Systems, H. Langmaack, W.-P. de Roever, J. Vytopil editors. Lecture Notes in Computer Science, Springer-Verlag | July 1994
  
  Publication
- TLZ (Abstract)
  
  Leslie Lamport
  
  Z User's Workshop, Cambridge. J.P. Bowen and J.A. Hall (Eds.) | May 1994
  
  Publication
- Verification of a Multiplier: 64 Bits and Beyond
  
  Leslie Lamport
  
  Computer-Aided Verification, Costas Courcoubetis, editor. (Proceedings of the Fifth International Conference, CAV'93.) Lecture Notes in Computer Science, number 697, Springer-Verlag (June, 1993), 166-179. | July 1993
  
  Publication
- Composing Specifications
  
  Leslie Lamport, Martin Abadi
  
  ACM Transactions on Programming Languages and Systems 15, 1 (January 1993), 73-132. Also appeared as SRC Research Report 66. A preliminary version appeared in Stepwise Refinement of Distributed Systems, J. W. de Bakker, W.-P. de Roever, and G. Rozenberg editors, Springer-Verlag Lecture Notes in Computer Science Volume 430 (1989), 1-41. | July 1993
  
  Publication
- Verification and Specification of Concurrent Programs
  
  Leslie Lamport
  
  A Decade of Concurrency: Reflections and Perspectives, J. W. de Bakker, W.-P. de Roever, and G. Rozenberg editors. Lecture Notes in Computer Science, number 803, Springer-Verlag, (June, 1993) 347-374. | June 1993
  
  Publication
- Hybrid Systems in TLA+
  
  Leslie Lamport
  
  Hybrid Systems, Robert L. Grossman, Anil Nerode, Hans Rischel, and Anders P. Ravn, editors. Lecture Notes in Computer Science, Springer-Verlag | 1993, Vol 736 | Hybrid Systems, Robert L. Grossman, Anil Nerode, Hans Rischel, and Anders P. Ravn, editors. Lecture Notes in Computer Science, Springer-Verlag edition
  
  Publication
- How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor
  
  Leslie Lamport
  
  IEEE Transactions on Computers SRC Research Report 96 | February 1993, Vol 46(7): pp. 779-782
  
  Publication
- Critique of the Lake Arrowhead Three
  
  Leslie Lamport
  
  Distributed Computing | August 1992, pp. 65-71
  
  Publication
- Mechanical Verification of Concurrent Systems with TLA
  
  Urban Engberg, Peter Gronning, Leslie Lamport
  
  Computer-Aided Verification, G. v. Bochmann and D. K. Probst editors. (Proceedings of the Fourth International Conference, CAV'92.) Lecture Notes in Computer Science, number 663, Springer-Verlag, (June, 1992) 44-55. | June 1992
  
  Publication
- The Reduction Theorem
  
  Leslie Lamport
  
  April 1992
  
  Publication
- Preserving Liveness: Comments on “Safety and Liveness from a Methodological Point of View”
  
  Martin Abadi, Bowen Alpern, Krzysztof R. Apt, Nissim Francez, Shmuel Katz, Leslie Lamport, Fred B. Schneider
  
  Information Processing Letters | November 1991, Vol 40(3): pp. 141-142
  
  Publication
- The Concurrent Reading and Writing of Clocks
  
  Leslie Lamport
  
  ACM Transactions on Computer Systems. Also appeared as SRC Research Report 27. | November 1990, pp. 305-310
  
  Publication
- A Completeness Theorem for TLA
  
  Leslie Lamport
  
  October 1990
  
  Publication
- The Mutual Exclusion Problem Has Been Solved
  
  Leslie Lamport
  
  Communications of the ACM | September 1990, Vol 34(1): pp. 110
  
  Publication
- Distributed Computing: Models and Methods
  
  Leslie Lamport, Nancy Lynch
  
  Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, Jan van Leeuwen, editor, Elsevier | August 1990, pp. 1157-1199
  
  Publication
- A Theorem on Atomicity in Distributed Algorithms
  
  Leslie Lamport
  
  Distributed Computing. Also appeared as SRC Research Report 28. | August 1990, Vol 4(2): pp. 59-68
  
  Publication
- win and sin: Predicate Transformers for Concurrency
  
  Leslie Lamport
  
  ACM Transactions on Programming Languages and Systems. Also appeared as SRC Research Report 17 (May 1987). | July 1990
  
  Publication
- Realizable and Unrealizable Specifications of Reactive Systems
  
  Martin Abadi, Leslie Lamport, Pierre Wolper
  
  Automata, Languages and Programming, Springer-Verlag | July 1989, pp. 1-17
  
  Publication
- Pretending Atomicity
  
  Leslie Lamport, Fred B. Schneider
  
  SRC Research Report 44 | May 1989
  
  Publication
- A Simple Approach to Specifying Concurrent Systems
  
  Leslie Lamport
  
  Proc. of ACM SIGCOMM. Communications of the ACM 32. Also appeared as SRC Research Report 15. | January 1989
  
  Publication
- A Lattice-Structured Proof of a Minimum Spanning Tree Algorithm
  
  Jennifer Lundelius Welch, Leslie Lamport, Nancy Lynch
  
  Proceedings of the Seventh Annual ACM Symposium on Principles of Distributed Computing | August 1988
  
  Publication
- Another Position Paper on Fairness
  
  Fred B. Schneider, Leslie Lamport
  
  Software Engineering Notes | July 1988, Vol 13(3): pp. 1-2
  
  Publication
- “EWD 1013”
  
  Leslie Lamport
  
  April 1988
  
  Publication
- Control Predicates Are Better than Dummy Variables for Representing Program Control
  
  Leslie Lamport
  
  ACM Transactions on Programming Languages and Systems. Also appeared as SRC Research Report 11. | April 1988, pp. 267-281
  
  Publication
- Synchronizing Time Servers
  
  Leslie Lamport
  
  | August 1987
  
  The ACM Conference on Human Factors in Computing Systems Workshop on Sensemaking (CHI 2008)
  
  Publication
- The Byzantine Generals
  
  Danny Dolev, Leslie Lamport, Marshall Pease, Robert Shostak
  
  Concurrency Control and Reliability in Distributed Systems, Bharat K. Bhargava, editor, Van Nostrand Reinhold | July 1987, pp. 348-369
  
  Publication
- Document Production: Visual or Logical?
  
  Leslie Lamport
  
  Notices of the American Mathematical Society. | June 1987, pp. 621-624
  
  Publication
- Distribution
  
  Leslie Lamport
  
  May 1987
  
  Email message sent to a DEC SRC bulletin board at 12:23:29 PDT on 28 May 87.
  
  Publication
- A Formal Basis for the Specification of Concurrent Systems
  
  Leslie Lamport
  
  In Distributed Operating Systems: Theory and Practice, Paker, Banatre and Bozyigit, editors, Springer-Verlag | April 1987, pp. 1-46
  
  Publication
- Derivation of a Simple Synchronization Algorithm
  
  Leslie Lamport
  
  February 1987
  
  Publication
- The Mutual Exclusion Problem – Part I: A Theory of Interprocess Communication
  
  Leslie Lamport
  
  Journal of the Association for Computing Machinery | January 1986, Vol 33(2): pp. 313-348
  
  Publication
- The Mutual Exclusion Problem – Part II: Statements and Solutions
  
  Leslie Lamport
  
  Journal of the Association for Computing Machinery | January 1986, Vol 33(2): pp. 313-348
  
  Publication
- On Interprocess Communication-Part I: Basic Formalism, Part II: Algorithms
  
  Leslie Lamport
  
  Distributed Computing. Also appeared as SRC Research Report 8. | December 1985, pp. 77-101
  
  Publication Publication
- A Fast Mutual Exclusion Algorithm
  
  Leslie Lamport
  
  ACM Transactions on Computer Systems 5, 1 (February 1987), 1-11. Also appeared as SRC Research Report 7. | November 1985, pp. 1-11
  
  Publication
- An Axiomatic Semantics of Concurrent Programming Languages
  
  Leslie Lamport
  
  Logics and Models of Concurrent Systems, Krzysztof Apt, editor. Springer-Verlag, Berlin | August 1985, pp. 77-122
  
  Publication
- Distributed Snapshots: Determining Global States of a Distributed System
  
  K. Mani Chandy, Leslie Lamport
  
  ACM Transactions on Computer Systems | February 1985, pp. 63-75
  
  Publication
- What It Means for a Concurrent Program to Satisfy a Specification: Why No One Has Specified Priority
  
  Leslie Lamport
  
  Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages, ACM SIGACT-SIGPLAN | January 1985
  
  Publication
- Synchronizing Clocks in the Presence of Faults
  
  Leslie Lamport, P. M. Melliar-Smith
  
  Journal of the Association for Computing Machinery | January 1985, Vol 32(1): pp. 52-78
  
  Publication
- Buridan’s Principle
  
  Leslie Lamport
  
  Foundations of Physics | October 1984, Vol 42(8): pp. 1056-1066
  
  Publication
- On a “Theorem” of Peterson
  
  Leslie Lamport
  
  October 1984
  
  Publication
- Solved Problems, Unsolved Problems and NonProblems in Concurrency
  
  Leslie Lamport
  
  Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing | August 1984
  
  Publication
- Byzantine Clock Synchronization
  
  Leslie Lamport, Michael Melliar-Smith
  
  Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing | August 1984
  
  Publication
- Recursive Compiling and Programming Environments (Summary)
  
  Leslie Lamport
  
  July 1984 | Rejected from the 1985 POPL Conference edition edition
  
  Rejected from the 1985 POPL Conference
  
  Publication
- Constraints: A Uniform Approach to Aliasing and Typing
  
  Leslie Lamport, Fred B. Schneider
  
  Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages, ACM SIGACT-SIGPLAN | July 1984
  
  Publication
- The Hoare Logic Of CSP, and All That
  
  Leslie Lamport
  
  ACM Transactions on Programming Languages and Systems | April 1984, pp. 281-296
  
  Publication
- Using Time Instead of Timeout for Fault-Tolerant Distributed Systems
  
  Leslie Lamport
  
  ACM Transactions on Programming Languages and Systems | April 1984, pp. 254-280
  
  Publication
- The Weak Byzantine Generals Problem
  
  Leslie Lamport
  
  Journal of the Association for Computing Machinery | June 1983, Vol 30(3): pp. 668-676
  
  Publication
- What Good Is Temporal Logic?
  
  Leslie Lamport
  
  Information Processing 83, R. E. A. Mason, ed., Elsevier Publishers | May 1983, Vol 83: pp. 657-668
  
  Publication
- Specifying Concurrent Program Modules
  
  Leslie Lamport
  
  ACM Transactions on Programming Languages and Systems | April 1983, pp. 190-222
  
  Publication
- Reasoning About Nonatomic Operations
  
  Leslie Lamport
  
  Proceedings of the Tenth ACM Symposium on Principles of Programming Languages, ACM SIGACT-SIGPLAN | January 1983
  
  Publication
- An Assertional Correctness Proof of a Distributed Program
  
  Leslie Lamport
  
  Science of Computer Programming | December 1982, pp. 175-206
  
  Publication
- The Byzantine Generals Problem
  
  Leslie Lamport, Robert Shostak, Marshall Pease
  
  ACM Transactions on Programming Languages and Systems | July 1982, pp. 382-401
  
  Publication
- Proving Liveness Properties of Concurrent Programs
  
  Leslie Lamport, Susan Owicki
  
  ACM Transactions on Programming Languages and Systems | July 1982, Vol 4(3): pp. 455-495
  
  Publication
- Byzantine Generals and Transaction Commit Protocols
  
  Leslie Lamport, Michael Fischer
  
  April 1982
  
  Publication
- Password Authentication with Insecure Communication
  
  Leslie Lamport
  
  Communications of the ACM 24 | November 1981, pp. 770-772
  
  Publication
- Reaching Agreement in the Presence of Faults
  
  Marshall Pease, Robert Shostak, Leslie Lamport
  
  Journal of the Association for Computing Machinery 27 | April 1980, Vol 2
  
  2005 Edsger W. Dijkstra Prize in Distributed Computing
  
  Publication
- Sometime’ is Sometimes ‘Not Never’
  
  Leslie Lamport
  
  Proceedings of the Seventh ACM Symposium on Principles of Programming Languages, ACM SIGACT-SIGPLAN | January 1980
  
  Publication
- Letter to the Editor
  
  Leslie Lamport
  
  Communications of the ACM 22 | November 1979, Vol 11: pp. 624
  
  Publication
- Constructing Digital Signatures from a One Way Function
  
  Leslie Lamport
  
  CSL-98 | October 1979
  
  This paper was published by IEEE in the Proceedings of HICSS-43 in January, 2010.
  
  Publication
- On the Proof of Correctness of a Calendar Program
  
  Leslie Lamport
  
  Communications of the ACM 22 | October 1979, Vol 10: pp. 554-556
  
  Publication
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
  
  Leslie Lamport
  
  IEEE Transactions on Computers C-28 | September 1979, Vol 9: pp. 690-691
  
  Publication
- How to Present a Paper
  
  Leslie Lamport
  
  August 1979
  
  Publication
- A New Approach to Proving the Correctness of Multiprocess Programs
  
  Leslie Lamport
  
  ACM Transactions on Programming Languages and Systems 1 | July 1979, Vol 1: pp. 84-97
  
  Publication Publication
- On-the-fly Garbage Collection: an Exercise in Cooperation
  
  Edsger W. Dijkstra, Leslie Lamport, A. J. Martin, C. S. Scholten, E. F. M. Steffens
  
  Communications of the ACM 21 | November 1978, Vol 11: pp. 966-975
  
  Publication
- SIFT: Design and Analysis of a Fault-Tolerant Computer for Aircraft Control
  
  John H. Wensley, Leslie Lamport, Jack Goldberg, Milton W. Green, Karl N. Levitt, P. M. Melliar-Smith, Robert E. Shostak, Charles B. Weinstock
  
  Proceedings of the IEEE 66 | October 1978
  
  Publication
- The Implementation of Reliable Distributed Multiprocess Systems
  
  Leslie Lamport
  
  Computer Networks | August 1978, Vol 2: pp. 95-114
  
  Publication
- Time, Clocks and the Ordering of Events in a Distributed System
  
  Leslie Lamport
  
  Communications of the ACM 21, 7 (July 1978), 558-565. Reprinted in several collections, including Distributed Computing: Concepts and Implementations, McEntire et al., ed. IEEE Press, 1984. | July 1978, pp. 558-565
  
  2000 PODC Influential Paper Award (later renamed the Edsger W. Dijkstra Prize in Distributed Computing). Also awarded an ACM SIGOPS Hall of Fame Award in 2007.
  
  Publication
- State the Problem Before Describing the Solution
  
  Leslie Lamport
  
  ACM SIGSOFT Software Engineering Notes | January 1978, pp. 26
  
  Publication
- On Concurrent Reading and Writing
  
  Leslie Lamport
  
  Communications of the ACM 20 | November 1977, Vol 11: pp. 806-811
  
  Publication
- Proving the Correctness of Multiprocess Programs
  
  Leslie Lamport
  
  IEEE Transactions on Software Engineering SE-3 | March 1977, Vol 2: pp. 125-143
  
  Publication
- How to Tell a Program from an Automobile
  
  Leslie Lamport
  
  In A Dynamic and Quick Intellect, John Tromp editor (1996)--a Liber Amicorum issued by the CWI in honor of Paul Vitanyi's 25-year jubilee. | January 1977
  
  Publication
- Comment on Bell’s Quadratic Quotient Algorithm
  
  Leslie Lamport
  
  Communications of the ACM | September 1970, Vol 13(9)
  
  Publication
- On the Glitch Phenomenon
  
  Leslie Lamport, Richard Palais
  
  November 1976 | Rejected by IEEE Transactions on Computers (November 1976). edition edition
  
  Rejected by IEEE Transactions on Computers (November 1976).
  
  Publication
- Multiple Byte Processing with Full-Word Instructions
  
  Leslie Lamport
  
  Communications of the ACM | August 1975, Vol 18(8): pp. 471-475
  
  Publication
- On Self-stabilizing Systems
  
  Leslie Lamport
  
  CA 7412-0511 | December 1974
  
  Publication
- A New Solution of Dijkstra’s Concurrent Programming Problem
  
  Leslie Lamport
  
  Communications of the ACM 17 | August 1974
  
  Publication
- Who Builds a House without Drawing Blueprints?
  
  Leslie Lamport
  
  Communications of the ACM | April 2015, Vol 58(4): pp. 38-41
  
  Publication Publication
- Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
  
  Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz
  
  Proceedings of the Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARNL 2014) | May 2014
  
  Publication
- Adaptive Register Allocation with a Linear Number of Registers
  
  Carole Delporte-Gallet, Hugues Fauconnier, Eli Gafni, Leslie Lamport
  
  Proceedings of the 27th International Symposium on Distributed Computing (DISC 2013) | August 2013
  
  Publication
- Why We Should Build Software Like We Build Houses
  
  Leslie Lamport
  
  Wired | January 2013
  
  Publication
- TLA+ Proofs
  
  Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernan Vanzetto
  
  Proceedings of the 18th International Symposium on Formal Methods (FM 2012), Dimitra Giannakopoulou and Dominique Mery, editors. Springer-Verlag Lecture Notes in Computer Science | January 2012, Vol 7436: pp. 147-154
  
  Publication
- Leaderless Byzantine Paxos
  
  Leslie Lamport
  
  Distributed Computing: 25th International Symposium: DISC 2011, David Peleg, editor. | December 2011, pp. 141-142
  
  Publication
- How to Write a 21st Century Proof
  
  Leslie Lamport
  
  Journal of Fixed Point Theory and Applications | November 2011
  
  Publication Publication
- Byzantizing Paxos by Refinement
  
  Leslie Lamport
  
  Distributed Computing: 25th International Symposium: DISC 2011, David Peleg, editor. Springer-Verlag. | June 2011, pp. 211-224
  
  Publication
- Euclid Writes an Algorithm: A Fairytale
  
  Leslie Lamport
  
  International Journal of Software and Informatics 5, 1-2 (2011) | June 2011, Vol 1: pp. 7-20
  
  Publication
- Verifying Safety Properties With the TLA+ Proof System
  
  Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
  
  Fifth International Joint Conference on Automated Reasoning (IJCAR), Edinburgh, UK. | July 2010
  
  Publication
- Computer Science and State Machines
  
  Leslie Lamport
  
  Concurrency, Compositionality, and Correctness (Essays in Honor of Willem-Paul de Roever). Dennis Dams, Ulrich Hannemann, and Martin Steffen editors. Lecture Notes in Computer Science, number 5930 (2010), 60-65. | June 2010, pp. 60-65
  
  Publication
- Vertical Paxos and Primary-Backup Replication
  
  Leslie Lamport, Dahlia Malkhi, Lidong Zhou
  
  The ACM Symposium on Principles of Distributed Computing (PODC 2009) | February 2009
  
  Publication Publication
- Teaching Concurrency
  
  Leslie Lamport
  
  ACM SIGACT News | January 2009, Vol 40(1): pp. 58-62
  
  Publication
- The PlusCal Algorithm Language
  
  Leslie Lamport
  
  Theoretical Aspects of Computing-ICTAC 2009, Martin Leucker and Carroll Morgan editors. Lecture Notes in Computer Science, number 5684, 36-60. | January 2009
  
  Publication
- The Mailbox Problem
  
  Leslie Lamport, Eli Gafni, Marcos K. Aguilera
  
  Proceedings of the International Symposium on Distributed Computing | September 2008
  
  Publication Publication
- A TLA+ Proof System
  
  Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
  
  Proceedings of the LPAR Workshops, CEUR Workshop | August 2008
  
  Publication
- Leslie Lamport: The Specification Language TLA+
  
  Leslie Lamport
  
  In Logics of Specification Languages | 2008 | In Logics of Specification Languages, Dines Bjørner and Martin C. Henson, editors. edition
  
  Editor(s): Dines Bjarner and Martin C. Henson
  
  Publication Publication
- Computation and State Machines
  
  Leslie Lamport
  
  April 2008
  
  Publication
- Stoppable Paxos
  
  Dahlia Malkhi, Leslie Lamport, Lidong Zhou
  
  MSR-TR-2008-192 | April 2008
  
  Publication
- Implementing Dataflow With Threads
  
  Leslie Lamport
  
  MSR-TR-2006-181 | December 2006
  
  Publication
- Fast Paxos
  
  Leslie Lamport
  
  Distributed Computing | October 2006, Vol 19: pp. 79-103
  
  Publication
- Checking a Multithreaded Algorithm with +CAL
  
  Leslie Lamport
  
  International Symposium on Distributed Computing (DISC) | September 2006
  
  Publication
- How Fast Can Eventual Synchrony Lead to Consensus?
  
  Partha Dutta, Rachid Guerraoui, Leslie Lamport
  
  Proceedings of the International Conference on Dependable Systems and Networks (DSN 2005) | June 2005
  
  Publication
- Generalized Consensus and Paxos
  
  Leslie Lamport
  
  MSR-TR-2005-33 | March 2005
  
  Publication
- Implementing and Combining Specifications
  
  Leslie Lamport
  
  September 2004
  
  Publication
- Lower Bounds for Asynchronous Consensus
  
  Leslie Lamport
  
  MSR-TR-2004-72 | July 2004
  
  Publication Publication
- Cheap Paxos
  
  Leslie Lamport, Mike Massa
  
  International Conference on Dependable Systems and Networks (DSN 2004) | June 2004
  
  Publication
- Consensus on Transaction Commit
  
  Jim Gray, Leslie Lamport
  
  MSR-TR-2003-96 | January 2004
  
  Published by Microsoft
  
  ACM Transactions on Database Systems 31, 1 (2006), 133-160
  
  Publication
- The Future of Computing: Logic or Biology
  
  Leslie Lamport
  
  July 2003
  
  Publication
- Disk Paxos
  
  Eli Gafni, Leslie Lamport
  
  Distributed Computing: 14th International Conference, DISC 2000, Maurice Herlihy, editor. Lecture Notes in Computer Science number 1914, Springer-Verlag, (2000) 330-344. | May 2003
  
  Publication Publication
- A Discussion With Leslie Lamport
  
  Leslie Lamport, Dejan Milojicic
  
  August 2002
  
  An interview in IEEE Distributed Systems Online 3, 8
  
  Publication
- Paxos Made Simple
  
  Leslie Lamport
  
  ACM SIGACT News (Distributed Computing Column) 32, 4 (Whole Number 121, December 2001) | December 2001, pp. 51-58
  
  Publication
- What Process Algebra Proofs Use Instead of Invariance
  
  Leslie Lamport
  
  January 1995
  
  Publication
- The Analytic Cauchy Problem with Singular Data
  
  Leslie Lamport
  
  May 1972
  
  PhD Thesis: Brandeis University | May 1972
  
  Publication
- The Parallel Execution of DO Loops
  
  Leslie Lamport
  
  Communications of the ACM 17 | February 1974, Vol 2: pp. 83-93
  
  Publication
- An Extension of a Theorem of Hamada on the Cauchy Problem with Singular Data
  
  Leslie Lamport
  
  American Mathematical Society | July 1973, Vol 174(4): pp. 776
  
  Publication
- Arbiter-Free Synchronization
  
  Leslie Lamport
  
  Distributed Computing | March 2002, Vol 16(3): pp. 219-237
  
  Publication Publication
- Braid Theory
  
  Leslie Lamport, Jackson Wright, Neal Plotkin, Robert Teitel, Martin Wenglinsky
  
  November 1957
  
  Publication
- An Old-Fashioned Recipe for Real Time
  
  Martin Abadi, Leslie Lamport
  
  Proceedings of REX Workshop "Real-Time: Theory in Practice", Mook, The Netherlands, June 1991 | January 1992
  
  Publication
- A General Construction for Expressing Repetition
  
  Leslie Lamport
  
  ACM SIGPLAN Notices 14 | March 1979, Vol 3: pp. 38-42
  
  Publication
- Generalized Consensus and Paxos
  
  Leslie Lamport
  
  MSR-TR-2005-33 | March 2005
  
  Publication
- Formal Specification of a Web Services Protocol
  
  James E. Johnson, David Langworthy, Leslie Lamport, Friedrich H. Vogt
  
  First International Workshop on Web Services and Formal Methods (WS-FM 2004) | February 2004
  
  Publication
- High-Level Specifications: Lessons from Industry
  
  Brannon Batson, Leslie Lamport
  
  Formal Methods for Components and Objects | March 2003
  
  Publication Publication
- Specifying and verifying systems with TLA+
  
  Leslie Lamport, John Matthews, Mark Tuttle, Yuan Yu
  
  Proceedings of the Tenth ACM SIGOPS European Workshop | September 2002
  
  Publication Publication
- Summer Vision Programs
  
  Leslie Lamport
  
  October 1966
  
  Massachusetts Institute of Technology, Project MAC Memorandum MAC-M-332, Artificial Intelligence Project Memo Number Vision 111
  
  Publication
- The Temporal Logic of Actions
  
  Leslie Lamport
  
  79 | May 1994
  
  Published by Microsoft
  
  ACM Transactions on Programming Languages and Systems 16
  
  Publication
- The Existence of Refinement Mappings
  
  Martin Abadi, Leslie Lamport
  
  Proceedings of the 3rd Annual Symposium on Logic in Computer Science | July 1988
  
  LICS 1988 Test of Time Award
  
  Publication
- Vertical Paxos and Primary-Backup Replication
  
  Leslie Lamport, Dahlia Malkhi, Lidong Zhou
  
  MSR-TR-2009-63 | May 2009
  
  Publication
- Vertical Paxos and Primary-Backup Replication
  
  Leslie Lamport, Dahlia Malkhi, Lidong Zhou
  
  The ACM Symposium on Principles of Distributed Computing (PODC 2009) | February 2009
  
  Publication Publication
- Reconfiguring a State Machine
  
  Leslie Lamport, Dahlia Malkhi, Lidong Zhou
  
  MSR-TR-2008-193 | February 2008
  
  Publication
- Checking a Multithreaded Algorithm with +CAL
  
  Leslie Lamport
  
  International Symposium on Distributed Computing (DISC) | September 2006
  
  Publication
- Chapter in Software Specification Methods: An Overview Using a Case Study
  
  Leslie Lamport
  
  Software Specification Methods: An Overview Using a Case Study, TLA+ | Published by Hermes | 2006
  
  Publication
- Real-Time Model Checking is Really Simple
  
  Leslie Lamport
  
  13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods | June 2005
  
  Publication
- Real Time is Really Simple
  
  Leslie Lamport
  
  MSR-TR-2005-30 | March 2005
  
  Publication
- Cheap Paxos
  
  Leslie Lamport, Mike Massa
  
  International Conference on Dependable Systems and Networks (DSN 2004) | June 2004
  
  Publication
- Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers
  
  Leslie Lamport
  
  Published by Addison-Wesley | June 2002
  
  Publication
- Arbiter-Free Synchronization
  
  Leslie Lamport
  
  Distributed Computing | March 2002, Vol 16(3): pp. 219-237
  
  Publication Publication
- Measuring Celebrity
  
  Leslie Lamport
  
  Annals of Improbable Research | January 2006, Vol 12: pp. 14-15
  
  Publication
- On Hair Color in France
  
  Ellen Gilkerson, Leslie Lamport
  
  January 2004
  
  Publication
- On Hair Color in France
  
  Ellen Gilkerson, Leslie Lamport
  
  January 2004
  
  Publication
- Checking Cache-Coherence Protocols with TLA+
  
  Rajeev Joshi, Leslie Lamport, John Matthews, Serdar Tasiran, Mark Tuttle, Yuan Yu
  
  Journal of Formal Methods in System Design | March 2003, Vol 22: pp. 125-131
  
  Publication

- The Wildfire Challenge Problem
  
  Leslie Lamport, Madhu Sharma, Mark Tuttle, Yuan Yu
  
  January 2001
  
  Publication
- When Does a Correct Mutual Exclusion Algorithm Guarantee Mutual Exclusion
  
  Leslie Lamport, Sharon Perl, William Weihl
  
  Information Processing Letters | March 2000, Vol 76(3): pp. 131-134
  
  Publication
- How (La)TeX changed the face of Mathematics
  
  Leslie Lamport
  
  Mitteilungen der Deutschen Mathematiker-Vereinigung | January 2000, pp. 49-51
  
  Publication
- Should Your Specification Language Be Typed?
  
  Leslie Lamport, Lawrence C. Paulson
  
  ACM Transactions on Programming Languages and Systems. Also appeared as SRC Research Report 147. | May 1999, Vol 31(3): pp. 502-526
  
  Publication
- Specifying Concurrent Systems with TLA+
  
  Leslie Lamport
  
  Calculational System Design | April 1999, pp. 183-247
  
  Publication
- A Lazy Caching Proof in TLA
  
  Peter Ladkin, Leslie Lamport, Bryan Olivier, Denis Roegel
  
  Distributed Computing 12 | April 1999, Vol 2(3): pp. 151-174
  
  Publication
- TLA+ Verification of Cache-Coherence Protocols
  
  Homayoon Akhiani, Damien Doligez, Paul Harter, Leslie Lamport, Mark Tuttle, Yuan Yu, Joshua Scheid
  
  February 1999
  
  Publication
- The Part-Time Parliament
  
  Leslie Lamport
  
  ACM Transactions on Computer Systems 16, 2 (May 1998), 133-169. Also appeared as SRC Research Report 49. This paper was first submitted in 1990, setting a personal record for publication delay that has since been broken by [60]. | May 1998
  
  ACM SIGOPS Hall of Fame Award in 2012
  
  Publication
- Proving Possibility Properties
  
  Leslie Lamport
  
  Theoretical Computer Science. Also appeared as SRC Research Report 137. | March 1998, Vol 206(2): pp. 341-352
  
  Publication
- A TLA Solution to the RPC-Memory Specification Problem
  
  Martin Abadi, Leslie Lamport, Stephan Merz
  
  Formal Systems Specification: The RPC-Memory Specification Case Study, Manfred Broy, Stephan Merz, and Katharina Spies editors. Lecture Notes in Computer Science, number 1169, (1996), 21-66. | November 1996
  
  Publication
- The RPC-Memory Specification Problem: Problem Statement
  
  Manfred Broy, Leslie Lamport
  
  Formal Systems Specification: The RPC-Memory Specification Case Study, Manfred Broy, Stephan Merz, and Katharina Spies editors. Lecture Notes in Computer Science. | August 1996, Vol 1169: pp. 1-4
  
  Publication
- TLA in Pictures
  
  Leslie Lamport
  
  IEEE Transactions on Software Engineering | September 1995, Vol 21(9): pp. 768-775
  
  Publication
- How to Write a Proof
  
  Leslie Lamport
  
  American Mathematical Monthly. Also appeared in Global Analysis in Modern Mathematics, Karen Uhlenbeck, editor. Publish or Perish Press, Houston. Also appeared as SRC Research Report 94. | August 1995, Vol 102(7): pp. 600-608
  
  Publication
- Conjoining Specifications
  
  Martin Abadi, Leslie Lamport
  
  ACM Transactions on Programming Languages and Systems. Also appeared as SRC Research Report 118. | May 1995, Vol 17(3): pp. 507-534
  
  Publication
- Processes are in the Eye of the Beholder
  
  Leslie Lamport
  
  Theoretical Computer Science SRC Research Report 132 | December 1994, Vol 179: pp. 333-351
  
  Publication
- How to Write a Long Formula
  
  Leslie Lamport
  
  FACJ 6(5) (September/October 1994) 580-584. Also appeared as SRC Research Report 119. | September 1994
  
  Publication
- Composing Specifications
  
  Leslie Lamport, Martin Abadi
  
  ACM Transactions on Programming Languages and Systems 15, 1 (January 1993), 73-132. Also appeared as SRC Research Report 66. A preliminary version appeared in Stepwise Refinement of Distributed Systems, J. W. de Bakker, W.-P. de Roever, and G. Rozenberg editors, Springer-Verlag Lecture Notes in Computer Science Volume 430 (1989), 1-41. | July 1993
  
  Publication
- How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor
  
  Leslie Lamport
  
  IEEE Transactions on Computers SRC Research Report 96 | February 1993, Vol 46(7): pp. 779-782
  
  Publication
- Critique of the Lake Arrowhead Three
  
  Leslie Lamport
  
  Distributed Computing | August 1992, pp. 65-71
  
  Publication
- Preserving Liveness: Comments on “Safety and Liveness from a Methodological Point of View”
  
  Martin Abadi, Bowen Alpern, Krzysztof R. Apt, Nissim Francez, Shmuel Katz, Leslie Lamport, Fred B. Schneider
  
  Information Processing Letters | November 1991, Vol 40(3): pp. 141-142
  
  Publication
- The Concurrent Reading and Writing of Clocks
  
  Leslie Lamport
  
  ACM Transactions on Computer Systems. Also appeared as SRC Research Report 27. | November 1990, pp. 305-310
  
  Publication
- The Mutual Exclusion Problem Has Been Solved
  
  Leslie Lamport
  
  Communications of the ACM | September 1990, Vol 34(1): pp. 110
  
  Publication
- Distributed Computing: Models and Methods
  
  Leslie Lamport, Nancy Lynch
  
  Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, Jan van Leeuwen, editor, Elsevier | August 1990, pp. 1157-1199
  
  Publication
- A Theorem on Atomicity in Distributed Algorithms
  
  Leslie Lamport
  
  Distributed Computing. Also appeared as SRC Research Report 28. | August 1990, Vol 4(2): pp. 59-68
  
  Publication
- Realizable and Unrealizable Specifications of Reactive Systems
  
  Martin Abadi, Leslie Lamport, Pierre Wolper
  
  Automata, Languages and Programming, Springer-Verlag | July 1989, pp. 1-17
  
  Publication
- Pretending Atomicity
  
  Leslie Lamport, Fred B. Schneider
  
  SRC Research Report 44 | May 1989
  
  Publication
- Another Position Paper on Fairness
  
  Fred B. Schneider, Leslie Lamport
  
  Software Engineering Notes | July 1988, Vol 13(3): pp. 1-2
  
  Publication
- Control Predicates Are Better than Dummy Variables for Representing Program Control
  
  Leslie Lamport
  
  ACM Transactions on Programming Languages and Systems. Also appeared as SRC Research Report 11. | April 1988, pp. 267-281
  
  Publication
- The Byzantine Generals
  
  Danny Dolev, Leslie Lamport, Marshall Pease, Robert Shostak
  
  Concurrency Control and Reliability in Distributed Systems, Bharat K. Bhargava, editor, Van Nostrand Reinhold | July 1987, pp. 348-369
  
  Publication
- Document Production: Visual or Logical?
  
  Leslie Lamport
  
  Notices of the American Mathematical Society. | June 1987, pp. 621-624
  
  Publication
- A Formal Basis for the Specification of Concurrent Systems
  
  Leslie Lamport
  
  In Distributed Operating Systems: Theory and Practice, Paker, Banatre and Bozyigit, editors, Springer-Verlag | April 1987, pp. 1-46
  
  Publication
- Derivation of a Simple Synchronization Algorithm
  
  Leslie Lamport
  
  February 1987
  
  Publication
- The Mutual Exclusion Problem – Part I: A Theory of Interprocess Communication
  
  Leslie Lamport
  
  Journal of the Association for Computing Machinery | January 1986, Vol 33(2): pp. 313-348
  
  Publication
- The Mutual Exclusion Problem – Part II: Statements and Solutions
  
  Leslie Lamport
  
  Journal of the Association for Computing Machinery | January 1986, Vol 33(2): pp. 313-348
  
  Publication
- On Interprocess Communication-Part I: Basic Formalism, Part II: Algorithms
  
  Leslie Lamport
  
  Distributed Computing. Also appeared as SRC Research Report 8. | December 1985, pp. 77-101
  
  Publication Publication
- A Fast Mutual Exclusion Algorithm
  
  Leslie Lamport
  
  ACM Transactions on Computer Systems 5, 1 (February 1987), 1-11. Also appeared as SRC Research Report 7. | November 1985, pp. 1-11
  
  Publication
- An Axiomatic Semantics of Concurrent Programming Languages
  
  Leslie Lamport
  
  Logics and Models of Concurrent Systems, Krzysztof Apt, editor. Springer-Verlag, Berlin | August 1985, pp. 77-122
  
  Publication
- Distributed Snapshots: Determining Global States of a Distributed System
  
  K. Mani Chandy, Leslie Lamport
  
  ACM Transactions on Computer Systems | February 1985, pp. 63-75
  
  Publication
- Synchronizing Clocks in the Presence of Faults
  
  Leslie Lamport, P. M. Melliar-Smith
  
  Journal of the Association for Computing Machinery | January 1985, Vol 32(1): pp. 52-78
  
  Publication
- Buridan’s Principle
  
  Leslie Lamport
  
  Foundations of Physics | October 1984, Vol 42(8): pp. 1056-1066
  
  Publication
- The Hoare Logic Of CSP, and All That
  
  Leslie Lamport
  
  ACM Transactions on Programming Languages and Systems | April 1984, pp. 281-296
  
  Publication
- Using Time Instead of Timeout for Fault-Tolerant Distributed Systems
  
  Leslie Lamport
  
  ACM Transactions on Programming Languages and Systems | April 1984, pp. 254-280
  
  Publication
- The Weak Byzantine Generals Problem
  
  Leslie Lamport
  
  Journal of the Association for Computing Machinery | June 1983, Vol 30(3): pp. 668-676
  
  Publication
- What Good Is Temporal Logic?
  
  Leslie Lamport
  
  Information Processing 83, R. E. A. Mason, ed., Elsevier Publishers | May 1983, Vol 83: pp. 657-668
  
  Publication
- Specifying Concurrent Program Modules
  
  Leslie Lamport
  
  ACM Transactions on Programming Languages and Systems | April 1983, pp. 190-222
  
  Publication
- An Assertional Correctness Proof of a Distributed Program
  
  Leslie Lamport
  
  Science of Computer Programming | December 1982, pp. 175-206
  
  Publication
- The Byzantine Generals Problem
  
  Leslie Lamport, Robert Shostak, Marshall Pease
  
  ACM Transactions on Programming Languages and Systems | July 1982, pp. 382-401
  
  Publication
- Proving Liveness Properties of Concurrent Programs
  
  Leslie Lamport, Susan Owicki
  
  ACM Transactions on Programming Languages and Systems | July 1982, Vol 4(3): pp. 455-495
  
  Publication
- Password Authentication with Insecure Communication
  
  Leslie Lamport
  
  Communications of the ACM 24 | November 1981, pp. 770-772
  
  Publication
- Reaching Agreement in the Presence of Faults
  
  Marshall Pease, Robert Shostak, Leslie Lamport
  
  Journal of the Association for Computing Machinery 27 | April 1980, Vol 2
  
  2005 Edsger W. Dijkstra Prize in Distributed Computing
  
  Publication
- Letter to the Editor
  
  Leslie Lamport
  
  Communications of the ACM 22 | November 1979, Vol 11: pp. 624
  
  Publication
- On the Proof of Correctness of a Calendar Program
  
  Leslie Lamport
  
  Communications of the ACM 22 | October 1979, Vol 10: pp. 554-556
  
  Publication
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
  
  Leslie Lamport
  
  IEEE Transactions on Computers C-28 | September 1979, Vol 9: pp. 690-691
  
  Publication
- A New Approach to Proving the Correctness of Multiprocess Programs
  
  Leslie Lamport
  
  ACM Transactions on Programming Languages and Systems 1 | July 1979, Vol 1: pp. 84-97
  
  Publication Publication
- A General Construction for Expressing Repetition
  
  Leslie Lamport
  
  ACM SIGPLAN Notices 14 | March 1979, Vol 3: pp. 38-42
  
  Publication
- On-the-fly Garbage Collection: an Exercise in Cooperation
  
  Edsger W. Dijkstra, Leslie Lamport, A. J. Martin, C. S. Scholten, E. F. M. Steffens
  
  Communications of the ACM 21 | November 1978, Vol 11: pp. 966-975
  
  Publication
- The Implementation of Reliable Distributed Multiprocess Systems
  
  Leslie Lamport
  
  Computer Networks | August 1978, Vol 2: pp. 95-114
  
  Publication
- Time, Clocks and the Ordering of Events in a Distributed System
  
  Leslie Lamport
  
  Communications of the ACM 21, 7 (July 1978), 558-565. Reprinted in several collections, including Distributed Computing: Concepts and Implementations, McEntire et al., ed. IEEE Press, 1984. | July 1978, pp. 558-565
  
  2000 PODC Influential Paper Award (later renamed the Edsger W. Dijkstra Prize in Distributed Computing). Also awarded an ACM SIGOPS Hall of Fame Award in 2007.
  
  Publication
- State the Problem Before Describing the Solution
  
  Leslie Lamport
  
  ACM SIGSOFT Software Engineering Notes | January 1978, pp. 26
  
  Publication
- On Concurrent Reading and Writing
  
  Leslie Lamport
  
  Communications of the ACM 20 | November 1977, Vol 11: pp. 806-811
  
  Publication
- Proving the Correctness of Multiprocess Programs
  
  Leslie Lamport
  
  IEEE Transactions on Software Engineering SE-3 | March 1977, Vol 2: pp. 125-143
  
  Publication
- How to Tell a Program from an Automobile
  
  Leslie Lamport
  
  In A Dynamic and Quick Intellect, John Tromp editor (1996)--a Liber Amicorum issued by the CWI in honor of Paul Vitanyi's 25-year jubilee. | January 1977
  
  Publication
- Comment on Bell’s Quadratic Quotient Algorithm
  
  Leslie Lamport
  
  Communications of the ACM | September 1970, Vol 13(9)
  
  Publication
- Multiple Byte Processing with Full-Word Instructions
  
  Leslie Lamport
  
  Communications of the ACM | August 1975, Vol 18(8): pp. 471-475
  
  Publication
- Who Builds a House without Drawing Blueprints?
  
  Leslie Lamport
  
  Communications of the ACM | April 2015, Vol 58(4): pp. 38-41
  
  Publication Publication
- Why We Should Build Software Like We Build Houses
  
  Leslie Lamport
  
  Wired | January 2013
  
  Publication
- TLA+ Proofs
  
  Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernan Vanzetto
  
  Proceedings of the 18th International Symposium on Formal Methods (FM 2012), Dimitra Giannakopoulou and Dominique Mery, editors. Springer-Verlag Lecture Notes in Computer Science | January 2012, Vol 7436: pp. 147-154
  
  Publication
- Leaderless Byzantine Paxos
  
  Leslie Lamport
  
  Distributed Computing: 25th International Symposium: DISC 2011, David Peleg, editor. | December 2011, pp. 141-142
  
  Publication
- How to Write a 21st Century Proof
  
  Leslie Lamport
  
  Journal of Fixed Point Theory and Applications | November 2011
  
  Publication Publication
- Byzantizing Paxos by Refinement
  
  Leslie Lamport
  
  Distributed Computing: 25th International Symposium: DISC 2011, David Peleg, editor. Springer-Verlag. | June 2011, pp. 211-224
  
  Publication
- Euclid Writes an Algorithm: A Fairytale
  
  Leslie Lamport
  
  International Journal of Software and Informatics 5, 1-2 (2011) | June 2011, Vol 1: pp. 7-20
  
  Publication
- The Parallel Execution of DO Loops
  
  Leslie Lamport
  
  Communications of the ACM 17 | February 1974, Vol 2: pp. 83-93
  
  Publication
- Computer Science and State Machines
  
  Leslie Lamport
  
  Concurrency, Compositionality, and Correctness (Essays in Honor of Willem-Paul de Roever). Dennis Dams, Ulrich Hannemann, and Martin Steffen editors. Lecture Notes in Computer Science, number 5930 (2010), 60-65. | June 2010, pp. 60-65
  
  Publication
- Teaching Concurrency
  
  Leslie Lamport
  
  ACM SIGACT News | January 2009, Vol 40(1): pp. 58-62
  
  Publication
- The PlusCal Algorithm Language
  
  Leslie Lamport
  
  Theoretical Aspects of Computing-ICTAC 2009, Martin Leucker and Carroll Morgan editors. Lecture Notes in Computer Science, number 5684, 36-60. | January 2009
  
  Publication
- Fast Paxos
  
  Leslie Lamport
  
  Distributed Computing | October 2006, Vol 19: pp. 79-103
  
  Publication
- Measuring Celebrity
  
  Leslie Lamport
  
  Annals of Improbable Research | January 2006, Vol 12: pp. 14-15
  
  Publication
- An Extension of a Theorem of Hamada on the Cauchy Problem with Singular Data
  
  Leslie Lamport
  
  American Mathematical Society | July 1973, Vol 174(4): pp. 776
  
  Publication
- Implementing and Combining Specifications
  
  Leslie Lamport
  
  September 2004
  
  Publication
- Checking Cache-Coherence Protocols with TLA+
  
  Rajeev Joshi, Leslie Lamport, John Matthews, Serdar Tasiran, Mark Tuttle, Yuan Yu
  
  Journal of Formal Methods in System Design | March 2003, Vol 22: pp. 125-131
  
  Publication
- Arbiter-Free Synchronization
  
  Leslie Lamport
  
  Distributed Computing | March 2002, Vol 16(3): pp. 219-237
  
  Publication Publication
- Paxos Made Simple
  
  Leslie Lamport
  
  ACM SIGACT News (Distributed Computing Column) 32, 4 (Whole Number 121, December 2001) | December 2001, pp. 51-58
  
  Publication
- Braid Theory
  
  Leslie Lamport, Jackson Wright, Neal Plotkin, Robert Teitel, Martin Wenglinsky
  
  November 1957
  
  Publication
- Fairness and Hyperfairness
  
  Leslie Lamport
  
  Distributed Computing. Also appeared as SRC Research Report 152. A preliminary version of this paper was rejected by Concur 99. | May 2000
  
  Publication
- Archival References to Web Pages
  
  Leslie Lamport
  
  Ninth International World Wide Web Conference: Poster Proceedings | May 2000
  
  Publication
- Model Checking TLA+ Specifications
  
  Yuan Yu, Panagiotis Manolios, Leslie Lamport
  
  In Correct Hardware Design and Verification Methods (CHARME '99), Laurence Pierre and Thomas Kropf editors. Lecture Notes in Computer Science, Springer-Verlag. | June 1999
  
  Publication
- Reduction in TLA
  
  Leslie Lamport, Ernie Cohen
  
  CONCUR'98 Concurrency Theory, David Sangiorgi and Robert de Simone editors. Lecture Notes in Computer Science. | May 1998
  
  Publication Publication
- Composition: A Way to Make Proofs Harder
  
  Leslie Lamport
  
  Compositionality: The Significant Difference (Proceedings of the COMPOS'97 Symposium), Willem-Paul de Roever, Hans Langmaack, and Amir Pnueli editors. Lecture Notes in Computer Science. | December 1997
  
  Publication
- Open Systems in TLA
  
  Martin Abadi, Leslie Lamport
  
  Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing | August 1994
  
  Publication
- Decomposing Specifications of Concurrent Systems
  
  Leslie Lamport, Martin Abadi
  
  Programming Concepts, Methods and Calculi, Ernst-RÃ¼diger Olderog editor. (Proceedings of the IFIP TC2/WG2.1/WG2.2/WG2.3 Working Conference, Procomet '94, San Miniato, Italy.) North-Holland | August 1994
  
  Publication
- Specifying and Verifying Fault-Tolerant Systems
  
  Leslie Lamport
  
  Formal Techniques in Real-Time and Fault-Tolerant Systems, H. Langmaack, W.-P. de Roever, J. Vytopil editors. Lecture Notes in Computer Science, Springer-Verlag | July 1994
  
  Publication
- TLZ (Abstract)
  
  Leslie Lamport
  
  Z User's Workshop, Cambridge. J.P. Bowen and J.A. Hall (Eds.) | May 1994
  
  Publication
- Verification of a Multiplier: 64 Bits and Beyond
  
  Leslie Lamport
  
  Computer-Aided Verification, Costas Courcoubetis, editor. (Proceedings of the Fifth International Conference, CAV'93.) Lecture Notes in Computer Science, number 697, Springer-Verlag (June, 1993), 166-179. | July 1993
  
  Publication
- Verification and Specification of Concurrent Programs
  
  Leslie Lamport
  
  A Decade of Concurrency: Reflections and Perspectives, J. W. de Bakker, W.-P. de Roever, and G. Rozenberg editors. Lecture Notes in Computer Science, number 803, Springer-Verlag, (June, 1993) 347-374. | June 1993
  
  Publication
- Mechanical Verification of Concurrent Systems with TLA
  
  Urban Engberg, Peter Gronning, Leslie Lamport
  
  Computer-Aided Verification, G. v. Bochmann and D. K. Probst editors. (Proceedings of the Fourth International Conference, CAV'92.) Lecture Notes in Computer Science, number 663, Springer-Verlag, (June, 1992) 44-55. | June 1992
  
  Publication
- An Old-Fashioned Recipe for Real Time
  
  Martin Abadi, Leslie Lamport
  
  Proceedings of REX Workshop "Real-Time: Theory in Practice", Mook, The Netherlands, June 1991 | January 1992
  
  Publication
- win and sin: Predicate Transformers for Concurrency
  
  Leslie Lamport
  
  ACM Transactions on Programming Languages and Systems. Also appeared as SRC Research Report 17 (May 1987). | July 1990
  
  Publication
- A Simple Approach to Specifying Concurrent Systems
  
  Leslie Lamport
  
  Proc. of ACM SIGCOMM. Communications of the ACM 32. Also appeared as SRC Research Report 15. | January 1989
  
  Publication
- A Lattice-Structured Proof of a Minimum Spanning Tree Algorithm
  
  Jennifer Lundelius Welch, Leslie Lamport, Nancy Lynch
  
  Proceedings of the Seventh Annual ACM Symposium on Principles of Distributed Computing | August 1988
  
  Publication
- The Existence of Refinement Mappings
  
  Martin Abadi, Leslie Lamport
  
  Proceedings of the 3rd Annual Symposium on Logic in Computer Science | July 1988
  
  LICS 1988 Test of Time Award
  
  Publication
- What It Means for a Concurrent Program to Satisfy a Specification: Why No One Has Specified Priority
  
  Leslie Lamport
  
  Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages, ACM SIGACT-SIGPLAN | January 1985
  
  Publication
- Solved Problems, Unsolved Problems and NonProblems in Concurrency
  
  Leslie Lamport
  
  Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing | August 1984
  
  Publication
- Byzantine Clock Synchronization
  
  Leslie Lamport, Michael Melliar-Smith
  
  Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing | August 1984
  
  Publication
- Constraints: A Uniform Approach to Aliasing and Typing
  
  Leslie Lamport, Fred B. Schneider
  
  Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages, ACM SIGACT-SIGPLAN | July 1984
  
  Publication
- Reasoning About Nonatomic Operations
  
  Leslie Lamport
  
  Proceedings of the Tenth ACM Symposium on Principles of Programming Languages, ACM SIGACT-SIGPLAN | January 1983
  
  Publication
- Sometime’ is Sometimes ‘Not Never’
  
  Leslie Lamport
  
  Proceedings of the Seventh ACM Symposium on Principles of Programming Languages, ACM SIGACT-SIGPLAN | January 1980
  
  Publication
- SIFT: Design and Analysis of a Fault-Tolerant Computer for Aircraft Control
  
  John H. Wensley, Leslie Lamport, Jack Goldberg, Milton W. Green, Karl N. Levitt, P. M. Melliar-Smith, Robert E. Shostak, Charles B. Weinstock
  
  Proceedings of the IEEE 66 | October 1978
  
  Publication
- A New Solution of Dijkstra’s Concurrent Programming Problem
  
  Leslie Lamport
  
  Communications of the ACM 17 | August 1974
  
  Publication
- Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
  
  Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz
  
  Proceedings of the Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARNL 2014) | May 2014
  
  Publication
- Adaptive Register Allocation with a Linear Number of Registers
  
  Carole Delporte-Gallet, Hugues Fauconnier, Eli Gafni, Leslie Lamport
  
  Proceedings of the 27th International Symposium on Distributed Computing (DISC 2013) | August 2013
  
  Publication
- Verifying Safety Properties With the TLA+ Proof System
  
  Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
  
  Fifth International Joint Conference on Automated Reasoning (IJCAR), Edinburgh, UK. | July 2010
  
  Publication
- Vertical Paxos and Primary-Backup Replication
  
  Leslie Lamport, Dahlia Malkhi, Lidong Zhou
  
  The ACM Symposium on Principles of Distributed Computing (PODC 2009) | February 2009
  
  Publication Publication
- The Mailbox Problem
  
  Leslie Lamport, Eli Gafni, Marcos K. Aguilera
  
  Proceedings of the International Symposium on Distributed Computing | September 2008
  
  Publication Publication
- A TLA+ Proof System
  
  Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
  
  Proceedings of the LPAR Workshops, CEUR Workshop | August 2008
  
  Publication
- Checking a Multithreaded Algorithm with +CAL
  
  Leslie Lamport
  
  International Symposium on Distributed Computing (DISC) | September 2006
  
  Publication
- Real-Time Model Checking is Really Simple
  
  Leslie Lamport
  
  13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods | June 2005
  
  Publication
- How Fast Can Eventual Synchrony Lead to Consensus?
  
  Partha Dutta, Rachid Guerraoui, Leslie Lamport
  
  Proceedings of the International Conference on Dependable Systems and Networks (DSN 2005) | June 2005
  
  Publication
- Cheap Paxos
  
  Leslie Lamport, Mike Massa
  
  International Conference on Dependable Systems and Networks (DSN 2004) | June 2004
  
  Publication
- Formal Specification of a Web Services Protocol
  
  James E. Johnson, David Langworthy, Leslie Lamport, Friedrich H. Vogt
  
  First International Workshop on Web Services and Formal Methods (WS-FM 2004) | February 2004
  
  Publication
- On Hair Color in France
  
  Ellen Gilkerson, Leslie Lamport
  
  January 2004
  
  Publication
- Disk Paxos
  
  Eli Gafni, Leslie Lamport
  
  Distributed Computing: 14th International Conference, DISC 2000, Maurice Herlihy, editor. Lecture Notes in Computer Science number 1914, Springer-Verlag, (2000) 330-344. | May 2003
  
  Publication Publication
- High-Level Specifications: Lessons from Industry
  
  Brannon Batson, Leslie Lamport
  
  Formal Methods for Components and Objects | March 2003
  
  Publication Publication
- Specifying and verifying systems with TLA+
  
  Leslie Lamport, John Matthews, Mark Tuttle, Yuan Yu
  
  Proceedings of the Tenth ACM SIGOPS European Workshop | September 2002
  
  Publication Publication
- Lower Bounds on Consensus
  
  Leslie Lamport
  
  March 2000
  
  Publication
- Marching to Many Distant Drummers
  
  Leslie Lamport, Timothy Mann
  
  May 1997
  
  Publication
- What Process Algebra Proofs Use Instead of Invariance
  
  Leslie Lamport
  
  January 1995
  
  Publication
- Adding “Process Algebra” to TLA
  
  Leslie Lamport
  
  January 1995
  
  Publication
- The Reduction Theorem
  
  Leslie Lamport
  
  April 1992
  
  Publication
- A Completeness Theorem for TLA
  
  Leslie Lamport
  
  October 1990
  
  Publication
- “EWD 1013”
  
  Leslie Lamport
  
  April 1988
  
  Publication
- On a “Theorem” of Peterson
  
  Leslie Lamport
  
  October 1984
  
  Publication
- Recursive Compiling and Programming Environments (Summary)
  
  Leslie Lamport
  
  July 1984 | Rejected from the 1985 POPL Conference edition edition
  
  Rejected from the 1985 POPL Conference
  
  Publication
- Byzantine Generals and Transaction Commit Protocols
  
  Leslie Lamport, Michael Fischer
  
  April 1982
  
  Publication
- How to Present a Paper
  
  Leslie Lamport
  
  August 1979
  
  Publication
- On the Glitch Phenomenon
  
  Leslie Lamport, Richard Palais
  
  November 1976 | Rejected by IEEE Transactions on Computers (November 1976). edition edition
  
  Rejected by IEEE Transactions on Computers (November 1976).
  
  Publication
- Computation and State Machines
  
  Leslie Lamport
  
  April 2008
  
  Publication
- Hybrid Systems in TLA+
  
  Leslie Lamport
  
  Hybrid Systems, Robert L. Grossman, Anil Nerode, Hans Rischel, and Anders P. Ravn, editors. Lecture Notes in Computer Science, Springer-Verlag | 1993, Vol 736 | Hybrid Systems, Robert L. Grossman, Anil Nerode, Hans Rischel, and Anders P. Ravn, editors. Lecture Notes in Computer Science, Springer-Verlag edition
  
  Publication
- Leslie Lamport: The Specification Language TLA+
  
  Leslie Lamport
  
  In Logics of Specification Languages | 2008 | In Logics of Specification Languages, Dines Bjørner and Martin C. Henson, editors. edition
  
  Editor(s): Dines Bjarner and Martin C. Henson
  
  Publication Publication
- Chapter in Software Specification Methods: An Overview Using a Case Study
  
  Leslie Lamport
  
  Software Specification Methods: An Overview Using a Case Study, TLA+ | Published by Hermes | 2006
  
  Publication
- Distribution
  
  Leslie Lamport
  
  May 1987
  
  Email message sent to a DEC SRC bulletin board at 12:23:29 PDT on 28 May 87.
  
  Publication
- The Future of Computing: Logic or Biology
  
  Leslie Lamport
  
  July 2003
  
  Publication
- A Discussion With Leslie Lamport
  
  Leslie Lamport, Dejan Milojicic
  
  August 2002
  
  An interview in IEEE Distributed Systems Online 3, 8
  
  Publication
- Summer Vision Programs
  
  Leslie Lamport
  
  October 1966
  
  Massachusetts Institute of Technology, Project MAC Memorandum MAC-M-332, Artificial Intelligence Project Memo Number Vision 111
  
  Publication
- Substitution: Syntactic versus Semantic
  
  Leslie Lamport
  
  1998-004 | March 1998
  
  The Fifth Internatinal Conference on Theoretical and Methodological Issues in Machine Translation with special emphasis on: MT in the Next Generation
  
  Publication
- Refinement in State-Based Formalisms
  
  Leslie Lamport
  
  1996-001 | December 1996
  
  Publication
- Introduction to TLA
  
  Leslie Lamport
  
  1994-001 | December 1994
  
  The Annals of Statistics
  
  Publication
- The Temporal Logic of Actions
  
  Leslie Lamport
  
  79 | May 1994
  
  Published by Microsoft
  
  ACM Transactions on Programming Languages and Systems 16
  
  Publication
- Synchronizing Time Servers
  
  Leslie Lamport
  
  | August 1987
  
  The ACM Conference on Human Factors in Computing Systems Workshop on Sensemaking (CHI 2008)
  
  Publication
- Constructing Digital Signatures from a One Way Function
  
  Leslie Lamport
  
  CSL-98 | October 1979
  
  This paper was published by IEEE in the Proceedings of HICSS-43 in January, 2010.
  
  Publication
- On Self-stabilizing Systems
  
  Leslie Lamport
  
  CA 7412-0511 | December 1974
  
  Publication
- Vertical Paxos and Primary-Backup Replication
  
  Leslie Lamport, Dahlia Malkhi, Lidong Zhou
  
  MSR-TR-2009-63 | May 2009
  
  Publication
- Stoppable Paxos
  
  Dahlia Malkhi, Leslie Lamport, Lidong Zhou
  
  MSR-TR-2008-192 | April 2008
  
  Publication
- Reconfiguring a State Machine
  
  Leslie Lamport, Dahlia Malkhi, Lidong Zhou
  
  MSR-TR-2008-193 | February 2008
  
  Publication
- Implementing Dataflow With Threads
  
  Leslie Lamport
  
  MSR-TR-2006-181 | December 2006
  
  Publication
- Generalized Consensus and Paxos
  
  Leslie Lamport
  
  MSR-TR-2005-33 | March 2005
  
  Publication
- Real Time is Really Simple
  
  Leslie Lamport
  
  MSR-TR-2005-30 | March 2005
  
  Publication
- Lower Bounds for Asynchronous Consensus
  
  Leslie Lamport
  
  MSR-TR-2004-72 | July 2004
  
  Publication Publication
- Consensus on Transaction Commit
  
  Jim Gray, Leslie Lamport
  
  MSR-TR-2003-96 | January 2004
  
  Published by Microsoft
  
  ACM Transactions on Database Systems 31, 1 (2006), 133-160
  
  Publication
- The Analytic Cauchy Problem with Singular Data
  
  Leslie Lamport
  
  May 1972
  
  PhD Thesis: Brandeis University | May 1972
  
  Publication
- Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers
  
  Leslie Lamport
  
  Published by Addison-Wesley | June 2002
  
  Publication

Leslie Lamport

Publications

Who Builds a House without Drawing Blueprints?

Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics

Adaptive Register Allocation with a Linear Number of Registers

Why We Should Build Software Like We Build Houses

TLA+ Proofs

Leaderless Byzantine Paxos

How to Write a 21st Century Proof

Byzantizing Paxos by Refinement

Euclid Writes an Algorithm: A Fairytale

Verifying Safety Properties With the TLA+ Proof System

Computer Science and State Machines

Vertical Paxos and Primary-Backup Replication

Vertical Paxos and Primary-Backup Replication

Teaching Concurrency

The PlusCal Algorithm Language

The Mailbox Problem

A TLA+ Proof System

Leslie Lamport: The Specification Language TLA+

Computation and State Machines

Stoppable Paxos

Reconfiguring a State Machine

Implementing Dataflow With Threads

Fast Paxos

Checking a Multithreaded Algorithm with +CAL

Chapter in Software Specification Methods: An Overview Using a Case Study

Measuring Celebrity

Real-Time Model Checking is Really Simple

How Fast Can Eventual Synchrony Lead to Consensus?

Generalized Consensus and Paxos

Real Time is Really Simple

Implementing and Combining Specifications

Lower Bounds for Asynchronous Consensus

Cheap Paxos

Formal Specification of a Web Services Protocol

Consensus on Transaction Commit

On Hair Color in France

The Future of Computing: Logic or Biology

Disk Paxos

Checking Cache-Coherence Protocols with TLA+

High-Level Specifications: Lessons from Industry

Specifying and verifying systems with TLA+

A Discussion With Leslie Lamport

Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers

Arbiter-Free Synchronization

The Wildfire Challenge Problem

Paxos Made Simple

Fairness and Hyperfairness

Archival References to Web Pages

Lower Bounds on Consensus

When Does a Correct Mutual Exclusion Algorithm Guarantee Mutual Exclusion

How (La)TeX changed the face of Mathematics

Model Checking TLA+ Specifications

Should Your Specification Language Be Typed?

Specifying Concurrent Systems with TLA+

A Lazy Caching Proof in TLA

TLA+ Verification of Cache-Coherence Protocols

Reduction in TLA

The Part-Time Parliament

Substitution: Syntactic versus Semantic

Proving Possibility Properties

Composition: A Way to Make Proofs Harder

Marching to Many Distant Drummers

Refinement in State-Based Formalisms

A TLA Solution to the RPC-Memory Specification Problem

The RPC-Memory Specification Problem: Problem Statement

TLA in Pictures

How to Write a Proof

Conjoining Specifications

Adding “Process Algebra” to TLA

What Process Algebra Proofs Use Instead of Invariance

Processes are in the Eye of the Beholder

Introduction to TLA

How to Write a Long Formula

Decomposing Specifications of Concurrent Systems

Open Systems in TLA

Specifying and Verifying Fault-Tolerant Systems

TLZ (Abstract)

The Temporal Logic of Actions