Who Builds a House without Drawing Blueprints?
Communications of the ACM | April 2015, 巻58(4): pp. 38-41
Leslie Lamport
Emeritus Researcher
出版物
-
-
-
-
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, 巻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, 巻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, 巻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
編集者: 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, 巻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+ | Hermes による投稿 | 2006
-
Measuring Celebrity
Annals of Improbable Research | January 2006, 巻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
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, 巻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, 巻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, 巻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, 巻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, 巻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, 巻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, 巻1169: pp. 1-4
-
-
-
TLA in Pictures
IEEE Transactions on Software Engineering | September 1995, 巻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, 巻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, 巻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, 巻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
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, 巻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, 巻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, 巻34(1): pp. 110
-
A Theorem on Atomicity in Distributed Algorithms
Distributed Computing. Also appeared as SRC Research Report 28. | August 1990, 巻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, 巻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, 巻33(2): pp. 313-348
-
The Mutual Exclusion Problem – Part II: Statements and Solutions
Journal of the Association for Computing Machinery | January 1986, 巻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, 巻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, 巻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 エディションエディション
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, 巻30(3): pp. 668-676
-
What Good Is Temporal Logic?
Information Processing 83, R. E. A. Mason, ed., Elsevier Publishers | May 1983, 巻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, 巻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, 巻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, 巻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, 巻10: pp. 554-556
-
How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
IEEE Transactions on Computers C-28 | September 1979, 巻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, 巻1: pp. 84-97
-
A General Construction for Expressing Repetition
ACM SIGPLAN Notices 14 | March 1979, 巻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, 巻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, 巻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, 巻11: pp. 806-811
-
Proving the Correctness of Multiprocess Programs
IEEE Transactions on Software Engineering SE-3 | March 1977, 巻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). エディションエディション
Rejected by IEEE Transactions on Computers (November 1976).
-
-
-
Multiple Byte Processing with Full-Word Instructions
Communications of the ACM | August 1975, 巻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, 巻2: pp. 83-93
-
-
-
An Extension of a Theorem of Hamada on the Cauchy Problem with Singular Data
American Mathematical Society | July 1973, 巻174(4): pp. 776
-
-
-
The Analytic Cauchy Problem with Singular Data
May 1972
博士論文:Brandeis University | May 1972
-
-
-
Comment on Bell’s Quadratic Quotient Algorithm
Communications of the ACM | September 1970, 巻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
-
-
-
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, 巻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, 巻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, 巻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, 巻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, 巻1169: pp. 1-4
-
TLA in Pictures
IEEE Transactions on Software Engineering | September 1995, 巻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, 巻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, 巻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, 巻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, 巻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, 巻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, 巻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, 巻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, 巻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, 巻33(2): pp. 313-348
-
The Mutual Exclusion Problem – Part II: Statements and Solutions
Journal of the Association for Computing Machinery | January 1986, 巻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, 巻32(1): pp. 52-78
-
Buridan’s Principle
Foundations of Physics | October 1984, 巻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 エディションエディション
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, 巻30(3): pp. 668-676
-
What Good Is Temporal Logic?
Information Processing 83, R. E. A. Mason, ed., Elsevier Publishers | May 1983, 巻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, 巻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, 巻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, 巻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, 巻10: pp. 554-556
-
How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
IEEE Transactions on Computers C-28 | September 1979, 巻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, 巻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, 巻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, 巻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, 巻11: pp. 806-811
-
Proving the Correctness of Multiprocess Programs
IEEE Transactions on Software Engineering SE-3 | March 1977, 巻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, 巻13(9)
-
On the Glitch Phenomenon
Leslie Lamport, Richard Palais
November 1976|Rejected by IEEE Transactions on Computers (November 1976). エディションエディション
Rejected by IEEE Transactions on Computers (November 1976).
-
Multiple Byte Processing with Full-Word Instructions
Communications of the ACM | August 1975, 巻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, 巻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, 巻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, 巻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, 巻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
編集者: 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, 巻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
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
博士論文:Brandeis University | May 1972
-
The Parallel Execution of DO Loops
Communications of the ACM 17 | February 1974, 巻2: pp. 83-93
-
An Extension of a Theorem of Hamada on the Cauchy Problem with Singular Data
American Mathematical Society | July 1973, 巻174(4): pp. 776
-
Arbiter-Free Synchronization
Distributed Computing | March 2002, 巻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, 巻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
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+ | 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, 巻16(3): pp. 219-237
-
-
-
Measuring Celebrity
Annals of Improbable Research | January 2006, 巻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, 巻22: pp. 125-131
-
-
-
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, 巻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, 巻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, 巻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, 巻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, 巻1169: pp. 1-4
-
TLA in Pictures
IEEE Transactions on Software Engineering | September 1995, 巻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, 巻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, 巻17(3): pp. 507-534
-
Processes are in the Eye of the Beholder
Theoretical Computer Science SRC Research Report 132 | December 1994, 巻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, 巻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, 巻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, 巻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, 巻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, 巻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, 巻33(2): pp. 313-348
-
The Mutual Exclusion Problem – Part II: Statements and Solutions
Journal of the Association for Computing Machinery | January 1986, 巻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, 巻32(1): pp. 52-78
-
Buridan’s Principle
Foundations of Physics | October 1984, 巻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, 巻30(3): pp. 668-676
-
What Good Is Temporal Logic?
Information Processing 83, R. E. A. Mason, ed., Elsevier Publishers | May 1983, 巻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, 巻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, 巻2
2005 Edsger W. Dijkstra Prize in Distributed Computing
-
Letter to the Editor
Communications of the ACM 22 | November 1979, 巻11: pp. 624
-
On the Proof of Correctness of a Calendar Program
Communications of the ACM 22 | October 1979, 巻10: pp. 554-556
-
How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
IEEE Transactions on Computers C-28 | September 1979, 巻9: pp. 690-691
-
A New Approach to Proving the Correctness of Multiprocess Programs
ACM Transactions on Programming Languages and Systems 1 | July 1979, 巻1: pp. 84-97
-
A General Construction for Expressing Repetition
ACM SIGPLAN Notices 14 | March 1979, 巻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, 巻11: pp. 966-975
-
The Implementation of Reliable Distributed Multiprocess Systems
Computer Networks | August 1978, 巻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, 巻11: pp. 806-811
-
Proving the Correctness of Multiprocess Programs
IEEE Transactions on Software Engineering SE-3 | March 1977, 巻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, 巻13(9)
-
Multiple Byte Processing with Full-Word Instructions
Communications of the ACM | August 1975, 巻18(8): pp. 471-475
-
Who Builds a House without Drawing Blueprints?
Communications of the ACM | April 2015, 巻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, 巻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, 巻1: pp. 7-20
-
The Parallel Execution of DO Loops
Communications of the ACM 17 | February 1974, 巻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, 巻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, 巻19: pp. 79-103
-
Measuring Celebrity
Annals of Improbable Research | January 2006, 巻12: pp. 14-15
-
An Extension of a Theorem of Hamada on the Cauchy Problem with Singular Data
American Mathematical Society | July 1973, 巻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, 巻22: pp. 125-131
-
Arbiter-Free Synchronization
Distributed Computing | March 2002, 巻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 エディションエディション
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). エディションエディション
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
編集者: 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+ | 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
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
Microsoft による投稿
ACM Transactions on Database Systems 31, 1 (2006), 133-160
-
-
-
The Analytic Cauchy Problem with Singular Data
May 1972
博士論文:Brandeis University | May 1972
-
-
-
Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers
Published by Addison-Wesley | June 2002
-