Who Builds a House without Drawing Blueprints?
Communications of the ACM | April 2015, Vol 58(4): pp. 38-41
Leslie Lamport
Distinguished Scientist
Publications
Publications by Year
-
-
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
-
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
Why We Should Build Software Like We Build Houses
Wired | January 2013
-
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
-
Leaderless Byzantine Paxos
Distributed Computing: 25th International Symposium: DISC 2011, David Peleg, editor. | December 2011, pp. 141-142
How to Write a 21st Century Proof
Journal of Fixed Point Theory and Applications | November 2011
Byzantizing Paxos by Refinement
Distributed Computing: 25th International Symposium: DISC 2011, David Peleg, editor. Springer-Verlag. | June 2011, pp. 211-224
Euclid Writes an Algorithm: A Fairytale
International Journal of Software and Informatics 5, 1-2 (2011) | June 2011, Vol 1: pp. 7-20
-
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
Computer Science and State Machines
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
-
Vertical Paxos and Primary-Backup Replication
Leslie Lamport, Dahlia Malkhi, Lidong Zhou
MSR-TR-2009-63 | May 2009
Vertical Paxos and Primary-Backup Replication
Leslie Lamport, Dahlia Malkhi, Lidong Zhou
The ACM Symposium on Principles of Distributed Computing (PODC 2009) | February 2009
Teaching Concurrency
ACM SIGACT News | January 2009, Vol 40(1): pp. 58-62
The PlusCal Algorithm Language
Theoretical Aspects of Computing-ICTAC 2009, Martin Leucker and Carroll Morgan editors. Lecture Notes in Computer Science, number 5684, 36-60. | January 2009
-
The Mailbox Problem
Leslie Lamport, Eli Gafni, Marcos K. Aguilera
Proceedings of the International Symposium on Distributed Computing | September 2008
A TLA+ Proof System
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
Proceedings of the LPAR Workshops, CEUR Workshop | August 2008
Leslie Lamport: The Specification Language TLA+
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
Computation and State Machines
April 2008
Stoppable Paxos
Dahlia Malkhi, Leslie Lamport, Lidong Zhou
MSR-TR-2008-192 | April 2008
Reconfiguring a State Machine
Leslie Lamport, Dahlia Malkhi, Lidong Zhou
MSR-TR-2008-193 | February 2008
-
Implementing Dataflow With Threads
MSR-TR-2006-181 | December 2006
Fast Paxos
Distributed Computing | October 2006, Vol 19: pp. 79-103
Checking a Multithreaded Algorithm with +CAL
International Symposium on Distributed Computing (DISC) | September 2006
Chapter in Software Specification Methods: An Overview Using a Case Study
Software Specification Methods: An Overview Using a Case Study, TLA+ | Published by Hermes | 2006
Measuring Celebrity
Annals of Improbable Research | January 2006, Vol 12: pp. 14-15
-
Real-Time Model Checking is Really Simple
13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods | June 2005
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
Generalized Consensus and Paxos
MSR-TR-2005-33 | March 2005
Real Time is Really Simple
MSR-TR-2005-30 | March 2005
-
Implementing and Combining Specifications
September 2004
Lower Bounds for Asynchronous Consensus
MSR-TR-2004-72 | July 2004
Cheap Paxos
Leslie Lamport, Mike Massa
International Conference on Dependable Systems and Networks (DSN 2004) | June 2004
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
Consensus on Transaction Commit
MSR-TR-2003-96 | January 2004
Published by Microsoft
ACM Transactions on Database Systems 31, 1 (2006), 133-160
On Hair Color in France
Ellen Gilkerson, Leslie Lamport
January 2004
-
The Future of Computing: Logic or Biology
July 2003
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
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
High-Level Specifications: Lessons from Industry
Brannon Batson, Leslie Lamport
Formal Methods for Components and Objects | March 2003
-
Specifying and verifying systems with TLA+
Leslie Lamport, John Matthews, Mark Tuttle, Yuan Yu
Proceedings of the Tenth ACM SIGOPS European Workshop | September 2002
A Discussion With Leslie Lamport
Leslie Lamport, Dejan Milojicic
August 2002
An interview in IEEE Distributed Systems Online 3, 8
Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers
Published by Addison-Wesley | June 2002
Arbiter-Free Synchronization
Distributed Computing | March 2002, Vol 16(3): pp. 219-237
-
The Wildfire Challenge Problem
Leslie Lamport, Madhu Sharma, Mark Tuttle, Yuan Yu
January 2001
Paxos Made Simple
ACM SIGACT News (Distributed Computing Column) 32, 4 (Whole Number 121, December 2001) | December 2001, pp. 51-58
-
Fairness and Hyperfairness
Distributed Computing. Also appeared as SRC Research Report 152. A preliminary version of this paper was rejected by Concur 99. | May 2000
Archival References to Web Pages
Ninth International World Wide Web Conference: Poster Proceedings | May 2000
Lower Bounds on Consensus
March 2000
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
How (La)TeX changed the face of Mathematics
Mitteilungen der Deutschen Mathematiker-Vereinigung | January 2000, pp. 49-51
-
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
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
Specifying Concurrent Systems with TLA+
Calculational System Design | April 1999, pp. 183-247
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
TLA+ Verification of Cache-Coherence Protocols
Homayoon Akhiani, Damien Doligez, Paul Harter, Leslie Lamport, Mark Tuttle, Yuan Yu, Joshua Scheid
February 1999
-
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
The Part-Time Parliament
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
Substitution: Syntactic versus Semantic
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
Proving Possibility Properties
Theoretical Computer Science. Also appeared as SRC Research Report 137. | March 1998, Vol 206(2): pp. 341-352
-
Composition: A Way to Make Proofs Harder
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
Marching to Many Distant Drummers
Leslie Lamport, Timothy Mann
May 1997
-
Refinement in State-Based Formalisms
1996-001 | December 1996
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
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
-
TLA in Pictures
IEEE Transactions on Software Engineering | September 1995, Vol 21(9): pp. 768-775
How to Write a Proof
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
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
Adding “Process Algebra” to TLA
January 1995
What Process Algebra Proofs Use Instead of Invariance
January 1995
-
Processes are in the Eye of the Beholder
Theoretical Computer Science SRC Research Report 132 | December 1994, Vol 179: pp. 333-351
Introduction to TLA
1994-001 | December 1994
The Annals of Statistics
How to Write a Long Formula
FACJ 6(5) (September/October 1994) 580-584. Also appeared as SRC Research Report 119. | September 1994
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
Open Systems in TLA
Martin Abadi, Leslie Lamport
Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing | August 1994
Specifying and Verifying Fault-Tolerant Systems
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
TLZ (Abstract)
Z User's Workshop, Cambridge. J.P. Bowen and J.A. Hall (Eds.) | May 1994
The Temporal Logic of Actions
79 | May 1994
Published by Microsoft
ACM Transactions on Programming Languages and Systems 16
-
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
Verification of a Multiplier: 64 Bits and Beyond
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
Verification and Specification of Concurrent Programs
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
Hybrid Systems in TLA+
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
How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor
IEEE Transactions on Computers SRC Research Report 96 | February 1993, Vol 46(7): pp. 779-782
-
Critique of the Lake Arrowhead Three
Distributed Computing | August 1992, pp. 65-71
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
The Reduction Theorem
April 1992
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
-
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
-
The Concurrent Reading and Writing of Clocks
ACM Transactions on Computer Systems. Also appeared as SRC Research Report 27. | November 1990, pp. 305-310
A Completeness Theorem for TLA
October 1990
The Mutual Exclusion Problem Has Been Solved
Communications of the ACM | September 1990, Vol 34(1): pp. 110
A Theorem on Atomicity in Distributed Algorithms
Distributed Computing. Also appeared as SRC Research Report 28. | August 1990, Vol 4(2): pp. 59-68
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
win and sin: Predicate Transformers for Concurrency
ACM Transactions on Programming Languages and Systems. Also appeared as SRC Research Report 17 (May 1987). | July 1990
-
Realizable and Unrealizable Specifications of Reactive Systems
Martin Abadi, Leslie Lamport, Pierre Wolper
Automata, Languages and Programming, Springer-Verlag | July 1989, pp. 1-17
Pretending Atomicity
Leslie Lamport, Fred B. Schneider
SRC Research Report 44 | May 1989
A Simple Approach to Specifying Concurrent Systems
Proc. of ACM SIGCOMM. Communications of the ACM 32. Also appeared as SRC Research Report 15. | January 1989
-
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
Another Position Paper on Fairness
Fred B. Schneider, Leslie Lamport
Software Engineering Notes | July 1988, Vol 13(3): pp. 1-2
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
“EWD 1013”
April 1988
Control Predicates Are Better than Dummy Variables for Representing Program Control
ACM Transactions on Programming Languages and Systems. Also appeared as SRC Research Report 11. | April 1988, pp. 267-281
-
Synchronizing Time Servers
| August 1987
The ACM Conference on Human Factors in Computing Systems Workshop on Sensemaking (CHI 2008)
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
Document Production: Visual or Logical?
Notices of the American Mathematical Society. | June 1987, pp. 621-624
Distribution
May 1987
Email message sent to a DEC SRC bulletin board at 12:23:29 PDT on 28 May 87.
A Formal Basis for the Specification of Concurrent Systems
In Distributed Operating Systems: Theory and Practice, Paker, Banatre and Bozyigit, editors, Springer-Verlag | April 1987, pp. 1-46
Derivation of a Simple Synchronization Algorithm
February 1987
-
The Mutual Exclusion Problem – Part I: A Theory of Interprocess Communication
Journal of the Association for Computing Machinery | January 1986, Vol 33(2): pp. 313-348
The Mutual Exclusion Problem – Part II: Statements and Solutions
Journal of the Association for Computing Machinery | January 1986, Vol 33(2): pp. 313-348
-
On Interprocess Communication-Part I: Basic Formalism, Part II: Algorithms
Distributed Computing. Also appeared as SRC Research Report 8. | December 1985, pp. 77-101
A Fast Mutual Exclusion Algorithm
ACM Transactions on Computer Systems 5, 1 (February 1987), 1-11. Also appeared as SRC Research Report 7. | November 1985, pp. 1-11
An Axiomatic Semantics of Concurrent Programming Languages
Logics and Models of Concurrent Systems, Krzysztof Apt, editor. Springer-Verlag, Berlin | August 1985, pp. 77-122
Distributed Snapshots: Determining Global States of a Distributed System
K. Mani Chandy, Leslie Lamport
ACM Transactions on Computer Systems | February 1985, pp. 63-75
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
What It Means for a Concurrent Program to Satisfy a Specification: Why No One Has Specified Priority
Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages, ACM SIGACT-SIGPLAN | January 1985
-
Buridan’s Principle
Foundations of Physics | October 1984, Vol 42(8): pp. 1056-1066
On a “Theorem” of Peterson
October 1984
Solved Problems, Unsolved Problems and NonProblems in Concurrency
Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing | August 1984
Byzantine Clock Synchronization
Leslie Lamport, Michael Melliar-Smith
Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing | August 1984
Recursive Compiling and Programming Environments (Summary)
July 1984 | Rejected from the 1985 POPL Conference edition edition
Rejected from the 1985 POPL Conference
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
The Hoare Logic Of CSP, and All That
ACM Transactions on Programming Languages and Systems | April 1984, pp. 281-296
Using Time Instead of Timeout for Fault-Tolerant Distributed Systems
ACM Transactions on Programming Languages and Systems | April 1984, pp. 254-280
-
The Weak Byzantine Generals Problem
Journal of the Association for Computing Machinery | June 1983, Vol 30(3): pp. 668-676
What Good Is Temporal Logic?
Information Processing 83, R. E. A. Mason, ed., Elsevier Publishers | May 1983, Vol 83: pp. 657-668
Specifying Concurrent Program Modules
ACM Transactions on Programming Languages and Systems | April 1983, pp. 190-222
Reasoning About Nonatomic Operations
Proceedings of the Tenth ACM Symposium on Principles of Programming Languages, ACM SIGACT-SIGPLAN | January 1983
-
An Assertional Correctness Proof of a Distributed Program
Science of Computer Programming | December 1982, pp. 175-206
The Byzantine Generals Problem
Leslie Lamport, Robert Shostak, Marshall Pease
ACM Transactions on Programming Languages and Systems | July 1982, pp. 382-401
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
Byzantine Generals and Transaction Commit Protocols
Leslie Lamport, Michael Fischer
April 1982
-
Password Authentication with Insecure Communication
Communications of the ACM 24 | November 1981, pp. 770-772
-
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
Sometime’ is Sometimes ‘Not Never’
Proceedings of the Seventh ACM Symposium on Principles of Programming Languages, ACM SIGACT-SIGPLAN | January 1980
-
Letter to the Editor
Communications of the ACM 22 | November 1979, Vol 11: pp. 624
Constructing Digital Signatures from a One Way Function
CSL-98 | October 1979
This paper was published by IEEE in the Proceedings of HICSS-43 in January, 2010.
On the Proof of Correctness of a Calendar Program
Communications of the ACM 22 | October 1979, Vol 10: pp. 554-556
How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
IEEE Transactions on Computers C-28 | September 1979, Vol 9: pp. 690-691
How to Present a Paper
August 1979
A New Approach to Proving the Correctness of Multiprocess Programs
ACM Transactions on Programming Languages and Systems 1 | July 1979, Vol 1: pp. 84-97
A General Construction for Expressing Repetition
ACM SIGPLAN Notices 14 | March 1979, Vol 3: pp. 38-42
-
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
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
The Implementation of Reliable Distributed Multiprocess Systems
Computer Networks | August 1978, Vol 2: pp. 95-114
Time, Clocks and the Ordering of Events in a Distributed System
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.
State the Problem Before Describing the Solution
ACM SIGSOFT Software Engineering Notes | January 1978, pp. 26
-
On Concurrent Reading and Writing
Communications of the ACM 20 | November 1977, Vol 11: pp. 806-811
Proving the Correctness of Multiprocess Programs
IEEE Transactions on Software Engineering SE-3 | March 1977, Vol 2: pp. 125-143
How to Tell a Program from an Automobile
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
-
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).
-
Multiple Byte Processing with Full-Word Instructions
Communications of the ACM | August 1975, Vol 18(8): pp. 471-475
-
On Self-stabilizing Systems
CA 7412-0511 | December 1974
A New Solution of Dijkstra’s Concurrent Programming Problem
Communications of the ACM 17 | August 1974
The Parallel Execution of DO Loops
Communications of the ACM 17 | February 1974, Vol 2: pp. 83-93
-
An Extension of a Theorem of Hamada on the Cauchy Problem with Singular Data
American Mathematical Society | July 1973, Vol 174(4): pp. 776
-
The Analytic Cauchy Problem with Singular Data
May 1972
PhD Thesis: Brandeis University | May 1972
-
Comment on Bell’s Quadratic Quotient Algorithm
Communications of the ACM | September 1970, Vol 13(9)
-
Summer Vision Programs
October 1966
Massachusetts Institute of Technology, Project MAC Memorandum MAC-M-332, Artificial Intelligence Project Memo Number Vision 111
-
Braid Theory
Leslie Lamport, Jackson Wright, Neal Plotkin, Robert Teitel, Martin Wenglinsky
November 1957
Publications by Research Area
-
The Wildfire Challenge Problem
Leslie Lamport, Madhu Sharma, Mark Tuttle, Yuan Yu
January 2001
Fairness and Hyperfairness
Distributed Computing. Also appeared as SRC Research Report 152. A preliminary version of this paper was rejected by Concur 99. | May 2000
Archival References to Web Pages
Ninth International World Wide Web Conference: Poster Proceedings | May 2000
Lower Bounds on Consensus
March 2000
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
How (La)TeX changed the face of Mathematics
Mitteilungen der Deutschen Mathematiker-Vereinigung | January 2000, pp. 49-51
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
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
Specifying Concurrent Systems with TLA+
Calculational System Design | April 1999, pp. 183-247
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
TLA+ Verification of Cache-Coherence Protocols
Homayoon Akhiani, Damien Doligez, Paul Harter, Leslie Lamport, Mark Tuttle, Yuan Yu, Joshua Scheid
February 1999
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
The Part-Time Parliament
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
Substitution: Syntactic versus Semantic
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
Proving Possibility Properties
Theoretical Computer Science. Also appeared as SRC Research Report 137. | March 1998, Vol 206(2): pp. 341-352
Composition: A Way to Make Proofs Harder
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
Marching to Many Distant Drummers
Leslie Lamport, Timothy Mann
May 1997
Refinement in State-Based Formalisms
1996-001 | December 1996
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
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
TLA in Pictures
IEEE Transactions on Software Engineering | September 1995, Vol 21(9): pp. 768-775
How to Write a Proof
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
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
Adding “Process Algebra” to TLA
January 1995
Processes are in the Eye of the Beholder
Theoretical Computer Science SRC Research Report 132 | December 1994, Vol 179: pp. 333-351
Introduction to TLA
1994-001 | December 1994
The Annals of Statistics
How to Write a Long Formula
FACJ 6(5) (September/October 1994) 580-584. Also appeared as SRC Research Report 119. | September 1994
Open Systems in TLA
Martin Abadi, Leslie Lamport
Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing | August 1994
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
Specifying and Verifying Fault-Tolerant Systems
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
TLZ (Abstract)
Z User's Workshop, Cambridge. J.P. Bowen and J.A. Hall (Eds.) | May 1994
Verification of a Multiplier: 64 Bits and Beyond
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
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
Verification and Specification of Concurrent Programs
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
Hybrid Systems in TLA+
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
How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor
IEEE Transactions on Computers SRC Research Report 96 | February 1993, Vol 46(7): pp. 779-782
Critique of the Lake Arrowhead Three
Distributed Computing | August 1992, pp. 65-71
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
The Reduction Theorem
April 1992
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
The Concurrent Reading and Writing of Clocks
ACM Transactions on Computer Systems. Also appeared as SRC Research Report 27. | November 1990, pp. 305-310
A Completeness Theorem for TLA
October 1990
The Mutual Exclusion Problem Has Been Solved
Communications of the ACM | September 1990, Vol 34(1): pp. 110
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
A Theorem on Atomicity in Distributed Algorithms
Distributed Computing. Also appeared as SRC Research Report 28. | August 1990, Vol 4(2): pp. 59-68
win and sin: Predicate Transformers for Concurrency
ACM Transactions on Programming Languages and Systems. Also appeared as SRC Research Report 17 (May 1987). | July 1990
Realizable and Unrealizable Specifications of Reactive Systems
Martin Abadi, Leslie Lamport, Pierre Wolper
Automata, Languages and Programming, Springer-Verlag | July 1989, pp. 1-17
Pretending Atomicity
Leslie Lamport, Fred B. Schneider
SRC Research Report 44 | May 1989
A Simple Approach to Specifying Concurrent Systems
Proc. of ACM SIGCOMM. Communications of the ACM 32. Also appeared as SRC Research Report 15. | January 1989
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
Another Position Paper on Fairness
Fred B. Schneider, Leslie Lamport
Software Engineering Notes | July 1988, Vol 13(3): pp. 1-2
“EWD 1013”
April 1988
Control Predicates Are Better than Dummy Variables for Representing Program Control
ACM Transactions on Programming Languages and Systems. Also appeared as SRC Research Report 11. | April 1988, pp. 267-281
Synchronizing Time Servers
| August 1987
The ACM Conference on Human Factors in Computing Systems Workshop on Sensemaking (CHI 2008)
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
Document Production: Visual or Logical?
Notices of the American Mathematical Society. | June 1987, pp. 621-624
Distribution
May 1987
Email message sent to a DEC SRC bulletin board at 12:23:29 PDT on 28 May 87.
A Formal Basis for the Specification of Concurrent Systems
In Distributed Operating Systems: Theory and Practice, Paker, Banatre and Bozyigit, editors, Springer-Verlag | April 1987, pp. 1-46
Derivation of a Simple Synchronization Algorithm
February 1987
The Mutual Exclusion Problem – Part I: A Theory of Interprocess Communication
Journal of the Association for Computing Machinery | January 1986, Vol 33(2): pp. 313-348
The Mutual Exclusion Problem – Part II: Statements and Solutions
Journal of the Association for Computing Machinery | January 1986, Vol 33(2): pp. 313-348
On Interprocess Communication-Part I: Basic Formalism, Part II: Algorithms
Distributed Computing. Also appeared as SRC Research Report 8. | December 1985, pp. 77-101
A Fast Mutual Exclusion Algorithm
ACM Transactions on Computer Systems 5, 1 (February 1987), 1-11. Also appeared as SRC Research Report 7. | November 1985, pp. 1-11
An Axiomatic Semantics of Concurrent Programming Languages
Logics and Models of Concurrent Systems, Krzysztof Apt, editor. Springer-Verlag, Berlin | August 1985, pp. 77-122
Distributed Snapshots: Determining Global States of a Distributed System
K. Mani Chandy, Leslie Lamport
ACM Transactions on Computer Systems | February 1985, pp. 63-75
What It Means for a Concurrent Program to Satisfy a Specification: Why No One Has Specified Priority
Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages, ACM SIGACT-SIGPLAN | January 1985
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
Buridan’s Principle
Foundations of Physics | October 1984, Vol 42(8): pp. 1056-1066
On a “Theorem” of Peterson
October 1984
Solved Problems, Unsolved Problems and NonProblems in Concurrency
Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing | August 1984
Byzantine Clock Synchronization
Leslie Lamport, Michael Melliar-Smith
Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing | August 1984
Recursive Compiling and Programming Environments (Summary)
July 1984 | Rejected from the 1985 POPL Conference edition edition
Rejected from the 1985 POPL Conference
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
The Hoare Logic Of CSP, and All That
ACM Transactions on Programming Languages and Systems | April 1984, pp. 281-296
Using Time Instead of Timeout for Fault-Tolerant Distributed Systems
ACM Transactions on Programming Languages and Systems | April 1984, pp. 254-280
The Weak Byzantine Generals Problem
Journal of the Association for Computing Machinery | June 1983, Vol 30(3): pp. 668-676
What Good Is Temporal Logic?
Information Processing 83, R. E. A. Mason, ed., Elsevier Publishers | May 1983, Vol 83: pp. 657-668
Specifying Concurrent Program Modules
ACM Transactions on Programming Languages and Systems | April 1983, pp. 190-222
Reasoning About Nonatomic Operations
Proceedings of the Tenth ACM Symposium on Principles of Programming Languages, ACM SIGACT-SIGPLAN | January 1983
An Assertional Correctness Proof of a Distributed Program
Science of Computer Programming | December 1982, pp. 175-206
The Byzantine Generals Problem
Leslie Lamport, Robert Shostak, Marshall Pease
ACM Transactions on Programming Languages and Systems | July 1982, pp. 382-401
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
Byzantine Generals and Transaction Commit Protocols
Leslie Lamport, Michael Fischer
April 1982
Password Authentication with Insecure Communication
Communications of the ACM 24 | November 1981, pp. 770-772
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
Sometime’ is Sometimes ‘Not Never’
Proceedings of the Seventh ACM Symposium on Principles of Programming Languages, ACM SIGACT-SIGPLAN | January 1980
Letter to the Editor
Communications of the ACM 22 | November 1979, Vol 11: pp. 624
Constructing Digital Signatures from a One Way Function
CSL-98 | October 1979
This paper was published by IEEE in the Proceedings of HICSS-43 in January, 2010.
On the Proof of Correctness of a Calendar Program
Communications of the ACM 22 | October 1979, Vol 10: pp. 554-556
How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
IEEE Transactions on Computers C-28 | September 1979, Vol 9: pp. 690-691
How to Present a Paper
August 1979
A New Approach to Proving the Correctness of Multiprocess Programs
ACM Transactions on Programming Languages and Systems 1 | July 1979, Vol 1: pp. 84-97
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
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
The Implementation of Reliable Distributed Multiprocess Systems
Computer Networks | August 1978, Vol 2: pp. 95-114
Time, Clocks and the Ordering of Events in a Distributed System
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.
State the Problem Before Describing the Solution
ACM SIGSOFT Software Engineering Notes | January 1978, pp. 26
On Concurrent Reading and Writing
Communications of the ACM 20 | November 1977, Vol 11: pp. 806-811
Proving the Correctness of Multiprocess Programs
IEEE Transactions on Software Engineering SE-3 | March 1977, Vol 2: pp. 125-143
How to Tell a Program from an Automobile
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
Comment on Bell’s Quadratic Quotient Algorithm
Communications of the ACM | September 1970, Vol 13(9)
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).
Multiple Byte Processing with Full-Word Instructions
Communications of the ACM | August 1975, Vol 18(8): pp. 471-475
On Self-stabilizing Systems
CA 7412-0511 | December 1974
A New Solution of Dijkstra’s Concurrent Programming Problem
Communications of the ACM 17 | August 1974
Who Builds a House without Drawing Blueprints?
Communications of the ACM | April 2015, Vol 58(4): pp. 38-41
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
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
Why We Should Build Software Like We Build Houses
Wired | January 2013
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
Leaderless Byzantine Paxos
Distributed Computing: 25th International Symposium: DISC 2011, David Peleg, editor. | December 2011, pp. 141-142
How to Write a 21st Century Proof
Journal of Fixed Point Theory and Applications | November 2011
Byzantizing Paxos by Refinement
Distributed Computing: 25th International Symposium: DISC 2011, David Peleg, editor. Springer-Verlag. | June 2011, pp. 211-224
Euclid Writes an Algorithm: A Fairytale
International Journal of Software and Informatics 5, 1-2 (2011) | June 2011, Vol 1: pp. 7-20
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
Computer Science and State Machines
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
Vertical Paxos and Primary-Backup Replication
Leslie Lamport, Dahlia Malkhi, Lidong Zhou
The ACM Symposium on Principles of Distributed Computing (PODC 2009) | February 2009
Teaching Concurrency
ACM SIGACT News | January 2009, Vol 40(1): pp. 58-62
The PlusCal Algorithm Language
Theoretical Aspects of Computing-ICTAC 2009, Martin Leucker and Carroll Morgan editors. Lecture Notes in Computer Science, number 5684, 36-60. | January 2009
The Mailbox Problem
Leslie Lamport, Eli Gafni, Marcos K. Aguilera
Proceedings of the International Symposium on Distributed Computing | September 2008
A TLA+ Proof System
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
Proceedings of the LPAR Workshops, CEUR Workshop | August 2008
Leslie Lamport: The Specification Language TLA+
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
Computation and State Machines
April 2008
Stoppable Paxos
Dahlia Malkhi, Leslie Lamport, Lidong Zhou
MSR-TR-2008-192 | April 2008
Implementing Dataflow With Threads
MSR-TR-2006-181 | December 2006
Fast Paxos
Distributed Computing | October 2006, Vol 19: pp. 79-103
Checking a Multithreaded Algorithm with +CAL
International Symposium on Distributed Computing (DISC) | September 2006
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
Generalized Consensus and Paxos
MSR-TR-2005-33 | March 2005
Implementing and Combining Specifications
September 2004
Lower Bounds for Asynchronous Consensus
MSR-TR-2004-72 | July 2004
Cheap Paxos
Leslie Lamport, Mike Massa
International Conference on Dependable Systems and Networks (DSN 2004) | June 2004
Consensus on Transaction Commit
MSR-TR-2003-96 | January 2004
Published by Microsoft
ACM Transactions on Database Systems 31, 1 (2006), 133-160
The Future of Computing: Logic or Biology
July 2003
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
A Discussion With Leslie Lamport
Leslie Lamport, Dejan Milojicic
August 2002
An interview in IEEE Distributed Systems Online 3, 8
Paxos Made Simple
ACM SIGACT News (Distributed Computing Column) 32, 4 (Whole Number 121, December 2001) | December 2001, pp. 51-58
-
What Process Algebra Proofs Use Instead of Invariance
January 1995
The Analytic Cauchy Problem with Singular Data
May 1972
PhD Thesis: Brandeis University | May 1972
The Parallel Execution of DO Loops
Communications of the ACM 17 | February 1974, Vol 2: pp. 83-93
An Extension of a Theorem of Hamada on the Cauchy Problem with Singular Data
American Mathematical Society | July 1973, Vol 174(4): pp. 776
Arbiter-Free Synchronization
Distributed Computing | March 2002, Vol 16(3): pp. 219-237
Braid Theory
Leslie Lamport, Jackson Wright, Neal Plotkin, Robert Teitel, Martin Wenglinsky
November 1957
-
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
A General Construction for Expressing Repetition
ACM SIGPLAN Notices 14 | March 1979, Vol 3: pp. 38-42
Generalized Consensus and Paxos
MSR-TR-2005-33 | March 2005
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
High-Level Specifications: Lessons from Industry
Brannon Batson, Leslie Lamport
Formal Methods for Components and Objects | March 2003
Specifying and verifying systems with TLA+
Leslie Lamport, John Matthews, Mark Tuttle, Yuan Yu
Proceedings of the Tenth ACM SIGOPS European Workshop | September 2002
-
Summer Vision Programs
October 1966
Massachusetts Institute of Technology, Project MAC Memorandum MAC-M-332, Artificial Intelligence Project Memo Number Vision 111
-
The Temporal Logic of Actions
79 | May 1994
Published by Microsoft
ACM Transactions on Programming Languages and Systems 16
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
Vertical Paxos and Primary-Backup Replication
Leslie Lamport, Dahlia Malkhi, Lidong Zhou
MSR-TR-2009-63 | May 2009
Vertical Paxos and Primary-Backup Replication
Leslie Lamport, Dahlia Malkhi, Lidong Zhou
The ACM Symposium on Principles of Distributed Computing (PODC 2009) | February 2009
Reconfiguring a State Machine
Leslie Lamport, Dahlia Malkhi, Lidong Zhou
MSR-TR-2008-193 | February 2008
Checking a Multithreaded Algorithm with +CAL
International Symposium on Distributed Computing (DISC) | September 2006
Chapter in Software Specification Methods: An Overview Using a Case Study
Software Specification Methods: An Overview Using a Case Study, TLA+ | Published by Hermes | 2006
Real-Time Model Checking is Really Simple
13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods | June 2005
Real Time is Really Simple
MSR-TR-2005-30 | March 2005
Cheap Paxos
Leslie Lamport, Mike Massa
International Conference on Dependable Systems and Networks (DSN 2004) | June 2004
Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers
Published by Addison-Wesley | June 2002
Arbiter-Free Synchronization
Distributed Computing | March 2002, Vol 16(3): pp. 219-237
-
Measuring Celebrity
Annals of Improbable Research | January 2006, Vol 12: pp. 14-15
On Hair Color in France
Ellen Gilkerson, Leslie Lamport
January 2004
-
On Hair Color in France
Ellen Gilkerson, Leslie Lamport
January 2004
-
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
Publications by Type
-
The Wildfire Challenge Problem
Leslie Lamport, Madhu Sharma, Mark Tuttle, Yuan Yu
January 2001
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
How (La)TeX changed the face of Mathematics
Mitteilungen der Deutschen Mathematiker-Vereinigung | January 2000, pp. 49-51
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
Specifying Concurrent Systems with TLA+
Calculational System Design | April 1999, pp. 183-247
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
TLA+ Verification of Cache-Coherence Protocols
Homayoon Akhiani, Damien Doligez, Paul Harter, Leslie Lamport, Mark Tuttle, Yuan Yu, Joshua Scheid
February 1999
The Part-Time Parliament
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
Proving Possibility Properties
Theoretical Computer Science. Also appeared as SRC Research Report 137. | March 1998, Vol 206(2): pp. 341-352
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
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
TLA in Pictures
IEEE Transactions on Software Engineering | September 1995, Vol 21(9): pp. 768-775
How to Write a Proof
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
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
Processes are in the Eye of the Beholder
Theoretical Computer Science SRC Research Report 132 | December 1994, Vol 179: pp. 333-351
How to Write a Long Formula
FACJ 6(5) (September/October 1994) 580-584. Also appeared as SRC Research Report 119. | September 1994
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
How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor
IEEE Transactions on Computers SRC Research Report 96 | February 1993, Vol 46(7): pp. 779-782
Critique of the Lake Arrowhead Three
Distributed Computing | August 1992, pp. 65-71
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
The Concurrent Reading and Writing of Clocks
ACM Transactions on Computer Systems. Also appeared as SRC Research Report 27. | November 1990, pp. 305-310
The Mutual Exclusion Problem Has Been Solved
Communications of the ACM | September 1990, Vol 34(1): pp. 110
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
A Theorem on Atomicity in Distributed Algorithms
Distributed Computing. Also appeared as SRC Research Report 28. | August 1990, Vol 4(2): pp. 59-68
Realizable and Unrealizable Specifications of Reactive Systems
Martin Abadi, Leslie Lamport, Pierre Wolper
Automata, Languages and Programming, Springer-Verlag | July 1989, pp. 1-17
Pretending Atomicity
Leslie Lamport, Fred B. Schneider
SRC Research Report 44 | May 1989
Another Position Paper on Fairness
Fred B. Schneider, Leslie Lamport
Software Engineering Notes | July 1988, Vol 13(3): pp. 1-2
Control Predicates Are Better than Dummy Variables for Representing Program Control
ACM Transactions on Programming Languages and Systems. Also appeared as SRC Research Report 11. | April 1988, pp. 267-281
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
Document Production: Visual or Logical?
Notices of the American Mathematical Society. | June 1987, pp. 621-624
A Formal Basis for the Specification of Concurrent Systems
In Distributed Operating Systems: Theory and Practice, Paker, Banatre and Bozyigit, editors, Springer-Verlag | April 1987, pp. 1-46
Derivation of a Simple Synchronization Algorithm
February 1987
The Mutual Exclusion Problem – Part I: A Theory of Interprocess Communication
Journal of the Association for Computing Machinery | January 1986, Vol 33(2): pp. 313-348
The Mutual Exclusion Problem – Part II: Statements and Solutions
Journal of the Association for Computing Machinery | January 1986, Vol 33(2): pp. 313-348
On Interprocess Communication-Part I: Basic Formalism, Part II: Algorithms
Distributed Computing. Also appeared as SRC Research Report 8. | December 1985, pp. 77-101
A Fast Mutual Exclusion Algorithm
ACM Transactions on Computer Systems 5, 1 (February 1987), 1-11. Also appeared as SRC Research Report 7. | November 1985, pp. 1-11
An Axiomatic Semantics of Concurrent Programming Languages
Logics and Models of Concurrent Systems, Krzysztof Apt, editor. Springer-Verlag, Berlin | August 1985, pp. 77-122
Distributed Snapshots: Determining Global States of a Distributed System
K. Mani Chandy, Leslie Lamport
ACM Transactions on Computer Systems | February 1985, pp. 63-75
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
Buridan’s Principle
Foundations of Physics | October 1984, Vol 42(8): pp. 1056-1066
The Hoare Logic Of CSP, and All That
ACM Transactions on Programming Languages and Systems | April 1984, pp. 281-296
Using Time Instead of Timeout for Fault-Tolerant Distributed Systems
ACM Transactions on Programming Languages and Systems | April 1984, pp. 254-280
The Weak Byzantine Generals Problem
Journal of the Association for Computing Machinery | June 1983, Vol 30(3): pp. 668-676
What Good Is Temporal Logic?
Information Processing 83, R. E. A. Mason, ed., Elsevier Publishers | May 1983, Vol 83: pp. 657-668
Specifying Concurrent Program Modules
ACM Transactions on Programming Languages and Systems | April 1983, pp. 190-222
An Assertional Correctness Proof of a Distributed Program
Science of Computer Programming | December 1982, pp. 175-206
The Byzantine Generals Problem
Leslie Lamport, Robert Shostak, Marshall Pease
ACM Transactions on Programming Languages and Systems | July 1982, pp. 382-401
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
Password Authentication with Insecure Communication
Communications of the ACM 24 | November 1981, pp. 770-772
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
Letter to the Editor
Communications of the ACM 22 | November 1979, Vol 11: pp. 624
On the Proof of Correctness of a Calendar Program
Communications of the ACM 22 | October 1979, Vol 10: pp. 554-556
How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
IEEE Transactions on Computers C-28 | September 1979, Vol 9: pp. 690-691
A New Approach to Proving the Correctness of Multiprocess Programs
ACM Transactions on Programming Languages and Systems 1 | July 1979, Vol 1: pp. 84-97
A General Construction for Expressing Repetition
ACM SIGPLAN Notices 14 | March 1979, Vol 3: pp. 38-42
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
The Implementation of Reliable Distributed Multiprocess Systems
Computer Networks | August 1978, Vol 2: pp. 95-114
Time, Clocks and the Ordering of Events in a Distributed System
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.
State the Problem Before Describing the Solution
ACM SIGSOFT Software Engineering Notes | January 1978, pp. 26
On Concurrent Reading and Writing
Communications of the ACM 20 | November 1977, Vol 11: pp. 806-811
Proving the Correctness of Multiprocess Programs
IEEE Transactions on Software Engineering SE-3 | March 1977, Vol 2: pp. 125-143
How to Tell a Program from an Automobile
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
Comment on Bell’s Quadratic Quotient Algorithm
Communications of the ACM | September 1970, Vol 13(9)
Multiple Byte Processing with Full-Word Instructions
Communications of the ACM | August 1975, Vol 18(8): pp. 471-475
Who Builds a House without Drawing Blueprints?
Communications of the ACM | April 2015, Vol 58(4): pp. 38-41
Why We Should Build Software Like We Build Houses
Wired | January 2013
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
Leaderless Byzantine Paxos
Distributed Computing: 25th International Symposium: DISC 2011, David Peleg, editor. | December 2011, pp. 141-142
How to Write a 21st Century Proof
Journal of Fixed Point Theory and Applications | November 2011
Byzantizing Paxos by Refinement
Distributed Computing: 25th International Symposium: DISC 2011, David Peleg, editor. Springer-Verlag. | June 2011, pp. 211-224
Euclid Writes an Algorithm: A Fairytale
International Journal of Software and Informatics 5, 1-2 (2011) | June 2011, Vol 1: pp. 7-20
The Parallel Execution of DO Loops
Communications of the ACM 17 | February 1974, Vol 2: pp. 83-93
Computer Science and State Machines
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
Teaching Concurrency
ACM SIGACT News | January 2009, Vol 40(1): pp. 58-62
The PlusCal Algorithm Language
Theoretical Aspects of Computing-ICTAC 2009, Martin Leucker and Carroll Morgan editors. Lecture Notes in Computer Science, number 5684, 36-60. | January 2009
Fast Paxos
Distributed Computing | October 2006, Vol 19: pp. 79-103
Measuring Celebrity
Annals of Improbable Research | January 2006, Vol 12: pp. 14-15
An Extension of a Theorem of Hamada on the Cauchy Problem with Singular Data
American Mathematical Society | July 1973, Vol 174(4): pp. 776
Implementing and Combining Specifications
September 2004
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
Arbiter-Free Synchronization
Distributed Computing | March 2002, Vol 16(3): pp. 219-237
Paxos Made Simple
ACM SIGACT News (Distributed Computing Column) 32, 4 (Whole Number 121, December 2001) | December 2001, pp. 51-58
Braid Theory
Leslie Lamport, Jackson Wright, Neal Plotkin, Robert Teitel, Martin Wenglinsky
November 1957
-
Fairness and Hyperfairness
Distributed Computing. Also appeared as SRC Research Report 152. A preliminary version of this paper was rejected by Concur 99. | May 2000
Archival References to Web Pages
Ninth International World Wide Web Conference: Poster Proceedings | May 2000
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
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
Composition: A Way to Make Proofs Harder
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
Open Systems in TLA
Martin Abadi, Leslie Lamport
Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing | August 1994
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
Specifying and Verifying Fault-Tolerant Systems
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
TLZ (Abstract)
Z User's Workshop, Cambridge. J.P. Bowen and J.A. Hall (Eds.) | May 1994
Verification of a Multiplier: 64 Bits and Beyond
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
Verification and Specification of Concurrent Programs
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
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
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
win and sin: Predicate Transformers for Concurrency
ACM Transactions on Programming Languages and Systems. Also appeared as SRC Research Report 17 (May 1987). | July 1990
A Simple Approach to Specifying Concurrent Systems
Proc. of ACM SIGCOMM. Communications of the ACM 32. Also appeared as SRC Research Report 15. | January 1989
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
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
What It Means for a Concurrent Program to Satisfy a Specification: Why No One Has Specified Priority
Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages, ACM SIGACT-SIGPLAN | January 1985
Solved Problems, Unsolved Problems and NonProblems in Concurrency
Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing | August 1984
Byzantine Clock Synchronization
Leslie Lamport, Michael Melliar-Smith
Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing | August 1984
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
Reasoning About Nonatomic Operations
Proceedings of the Tenth ACM Symposium on Principles of Programming Languages, ACM SIGACT-SIGPLAN | January 1983
Sometime’ is Sometimes ‘Not Never’
Proceedings of the Seventh ACM Symposium on Principles of Programming Languages, ACM SIGACT-SIGPLAN | January 1980
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
A New Solution of Dijkstra’s Concurrent Programming Problem
Communications of the ACM 17 | August 1974
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
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
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
Vertical Paxos and Primary-Backup Replication
Leslie Lamport, Dahlia Malkhi, Lidong Zhou
The ACM Symposium on Principles of Distributed Computing (PODC 2009) | February 2009
The Mailbox Problem
Leslie Lamport, Eli Gafni, Marcos K. Aguilera
Proceedings of the International Symposium on Distributed Computing | September 2008
A TLA+ Proof System
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
Proceedings of the LPAR Workshops, CEUR Workshop | August 2008
Checking a Multithreaded Algorithm with +CAL
International Symposium on Distributed Computing (DISC) | September 2006
Real-Time Model Checking is Really Simple
13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods | June 2005
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
Cheap Paxos
Leslie Lamport, Mike Massa
International Conference on Dependable Systems and Networks (DSN 2004) | June 2004
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
On Hair Color in France
Ellen Gilkerson, Leslie Lamport
January 2004
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
High-Level Specifications: Lessons from Industry
Brannon Batson, Leslie Lamport
Formal Methods for Components and Objects | March 2003
Specifying and verifying systems with TLA+
Leslie Lamport, John Matthews, Mark Tuttle, Yuan Yu
Proceedings of the Tenth ACM SIGOPS European Workshop | September 2002
-
Lower Bounds on Consensus
March 2000
Marching to Many Distant Drummers
Leslie Lamport, Timothy Mann
May 1997
What Process Algebra Proofs Use Instead of Invariance
January 1995
Adding “Process Algebra” to TLA
January 1995
The Reduction Theorem
April 1992
A Completeness Theorem for TLA
October 1990
“EWD 1013”
April 1988
On a “Theorem” of Peterson
October 1984
Recursive Compiling and Programming Environments (Summary)
July 1984 | Rejected from the 1985 POPL Conference edition edition
Rejected from the 1985 POPL Conference
Byzantine Generals and Transaction Commit Protocols
Leslie Lamport, Michael Fischer
April 1982
How to Present a Paper
August 1979
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).
Computation and State Machines
April 2008
-
Hybrid Systems in TLA+
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
Leslie Lamport: The Specification Language TLA+
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
Chapter in Software Specification Methods: An Overview Using a Case Study
Software Specification Methods: An Overview Using a Case Study, TLA+ | Published by Hermes | 2006
-
Distribution
May 1987
Email message sent to a DEC SRC bulletin board at 12:23:29 PDT on 28 May 87.
The Future of Computing: Logic or Biology
July 2003
A Discussion With Leslie Lamport
Leslie Lamport, Dejan Milojicic
August 2002
An interview in IEEE Distributed Systems Online 3, 8
Summer Vision Programs
October 1966
Massachusetts Institute of Technology, Project MAC Memorandum MAC-M-332, Artificial Intelligence Project Memo Number Vision 111
-
Substitution: Syntactic versus Semantic
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
Refinement in State-Based Formalisms
1996-001 | December 1996
Introduction to TLA
1994-001 | December 1994
The Annals of Statistics
The Temporal Logic of Actions
79 | May 1994
Published by Microsoft
ACM Transactions on Programming Languages and Systems 16
Synchronizing Time Servers
| August 1987
The ACM Conference on Human Factors in Computing Systems Workshop on Sensemaking (CHI 2008)
Constructing Digital Signatures from a One Way Function
CSL-98 | October 1979
This paper was published by IEEE in the Proceedings of HICSS-43 in January, 2010.
On Self-stabilizing Systems
CA 7412-0511 | December 1974
Vertical Paxos and Primary-Backup Replication
Leslie Lamport, Dahlia Malkhi, Lidong Zhou
MSR-TR-2009-63 | May 2009
Stoppable Paxos
Dahlia Malkhi, Leslie Lamport, Lidong Zhou
MSR-TR-2008-192 | April 2008
Reconfiguring a State Machine
Leslie Lamport, Dahlia Malkhi, Lidong Zhou
MSR-TR-2008-193 | February 2008
Implementing Dataflow With Threads
MSR-TR-2006-181 | December 2006
Generalized Consensus and Paxos
MSR-TR-2005-33 | March 2005
Real Time is Really Simple
MSR-TR-2005-30 | March 2005
Lower Bounds for Asynchronous Consensus
MSR-TR-2004-72 | July 2004
Consensus on Transaction Commit
MSR-TR-2003-96 | January 2004
Published by Microsoft
ACM Transactions on Database Systems 31, 1 (2006), 133-160
-
The Analytic Cauchy Problem with Singular Data
May 1972
PhD Thesis: Brandeis University | May 1972
-
Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers
Published by Addison-Wesley | June 2002