Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDLeslie Lamport
Person information
- affiliation: Microsoft Research, Mountain View
- award (2013): Turing Award
- award (2008): IEEE John von Neumann Medal
- award (2004): IEEE Emanuel R. Piore Award
- award (2000, 2005, 2014): Dijkstra Prize
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2022
[j75]Leslie Lamport:
Deconstructing the bakery to build a distributed state machine. Commun. ACM 65(9): 58-66 (2022)- [j74]Leslie Lamport, Stephan Merz
:
Prophecy Made Simple. ACM Trans. Program. Lang. Syst. 44(2): 6:1-6:27 (2022) - [p11]Leslie Lamport:
Concurrent Algorithms. Edsger Wybe Dijkstra 2022: 47-80 - [p10]Edsger W. Dijkstra, Leslie Lamport, Alain J. Martin, Carel S. Scholten, Elisabeth F. M. Steffens:
On-the-Fly Garbage Collection: An Exercise in Cooperation. Edsger Wybe Dijkstra 2022: 339-358 - [i8]Jonas Bayer, Christoph Benzmüller, Kevin Buzzard, Marco David, Leslie Lamport, Yuri V. Matiyasevich, Lawrence C. Paulson, Dierk Schleicher, Benedikt Stock, Efim I. Zelmanov:
Mathematical Proof Between Generations. CoRR abs/2207.04779 (2022) - 2021
- [c74]Leslie Lamport, Fred B. Schneider:
Verifying Hyperproperties With TLA. CSF 2021: 1-16
2010 – 2019
- 2019
- [c73]Markus Alexander Kuppe, Leslie Lamport, Daniel Ricketts:
The TLA+ Toolbox. F-IDE@FM 2019: 50-62 - [p9]Leslie Lamport:
The computer science of concurrency: the early years. Concurrency: the Works of Leslie Lamport 2019: 13-26 - [p8]Leslie Lamport:
A new solution of Dijkstra's concurrent programming problem. Concurrency: the Works of Leslie Lamport 2019: 171-178 - [p7]Leslie Lamport:
Time, clocks, and the ordering of events in a distributed system. Concurrency: the Works of Leslie Lamport 2019: 179-196 - [p6]Leslie Lamport:
How to make a multiprocessor computer that correctly executes multiprocess programs. Concurrency: the Works of Leslie Lamport 2019: 197-201 - [p5]Leslie Lamport, Robert E. Shostak, Marshall C. Pease:
The Byzantine generals problem. Concurrency: the Works of Leslie Lamport 2019: 203-226 - [p4]Leslie Lamport:
The mutual exclusion problem: part I - A theory of interprocess communication. Concurrency: the Works of Leslie Lamport 2019: 227-245 - [p3]Leslie Lamport:
The mutual exclusion problem: part II - Statement and solutions. Concurrency: the Works of Leslie Lamport 2019: 247-276 - [p2]Leslie Lamport:
The part-time parliament. Concurrency: the Works of Leslie Lamport 2019: 277-317 - 2018
- [j73]Leslie Lamport:
If You're Not Writing a Program, Don't Use a Programming Language. Bull. EATCS 125 (2018) - 2017
- [i7]Leslie Lamport, Stephan Merz:
Auxiliary Variables in TLA+. CoRR abs/1703.05121 (2017) - [i6]Leslie Lamport, Richard Palais:
On the Glitch Phenomenon. CoRR abs/1704.01154 (2017) - 2015
- [j72]Leslie Lamport:
Who builds a house without drawing blueprints? Commun. ACM 58(4): 38-41 (2015) - [j71]Leslie Lamport:
Turing lecture: The computer science of concurrency: the early years. Commun. ACM 58(6): 71-76 (2015) - 2014
- [c72]Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz:
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics. ARQNL@IJCAR 2014: 1-16 - [c71]Leslie Lamport:
An incomplete history of concurrency chapter 1. 1965-1977. PODC 2014: 291 - [i5]Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz:
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics. CoRR abs/1409.3819 (2014) - 2013
- [c70]Carole Delporte-Gallet, Hugues Fauconnier, Eli Gafni, Leslie Lamport:
Adaptive Register Allocation with a Linear Number of Registers. DISC 2013: 269-283 - 2012
- [c69]Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto:
TLA + Proofs. FM 2012: 147-154 - [i4]Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto:
TLA+ Proofs. CoRR abs/1208.5933 (2012) - 2011
- [j70]Leslie Lamport:
Euclid Writes an Algorithm: A Fairytale. Int. J. Softw. Informatics 5(1-2): 7-20 (2011) - [c68]Leslie Lamport:
Brief Announcement: Leaderless Byzantine Paxos. DISC 2011: 141-142 - [c67]Leslie Lamport:
Byzantizing Paxos by Refinement. DISC 2011: 211-224 - 2010
- [j69]Marcos Kawazoe Aguilera, Eli Gafni, Leslie Lamport:
The mailbox problem. Distributed Comput. 23(2): 113-134 (2010) - [j68]Leslie Lamport, Dahlia Malkhi, Lidong Zhou:
Reconfiguring a state machine. SIGACT News 41(1): 63-73 (2010) - [c66]Leslie Lamport:
Computer Science and State Machines. Concurrency, Compositionality, and Correctness 2010: 60-65 - [c65]Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz:
Verifying Safety Properties with the TLA+ Proof System. IJCAR 2010: 142-148 - [c64]Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz:
The TLA+ Proof System: Building a Heterogeneous Verification Platform. ICTAC 2010: 44 - [i3]Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz:
Verifying Safety Properties With the TLA+ Proof System. CoRR abs/1011.2560 (2010)
2000 – 2009
- 2009
- [j67]Leslie Lamport:
Teaching concurrency. SIGACT News 40(1): 58-62 (2009) - [c63]Leslie Lamport:
The PlusCal Algorithm Language. ICTAC 2009: 36-60 - [c62]Leslie Lamport:
TLA+: Whence, Wherefore, and Whither. NASA Formal Methods 2009: 3 - [c61]Leslie Lamport, Dahlia Malkhi, Lidong Zhou:
Vertical paxos and primary-backup replication. PODC 2009: 312-313 - 2008
- [j66]Leslie Lamport:
Implementing dataflow with threads. Distributed Comput. 21(3): 163-181 (2008) - [c60]Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz:
A TLA+ Proof System. LPAR Workshops 2008 - [c59]Marcos Kawazoe Aguilera, Eli Gafni, Leslie Lamport:
The Mailbox Problem. DISC 2008: 1-15 - [i2]Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz:
A TLA+ Proof System. CoRR abs/0811.1914 (2008) - 2007
- [j65]James E. Johnson, David E. Langworthy, Leslie Lamport, Friedrich H. Vogt:
Formal specification of a Web services protocol. J. Log. Algebraic Methods Program. 70(1): 34-52 (2007) - [c58]Leslie Lamport:
DISC 20th Anniversary: Invited Talk Time, Clocks, and the Ordering of My Ideas About Distributed Systems. DISC 2007: 504 - 2006
- [j64]Leslie Lamport:
Fast Paxos. Distributed Comput. 19(2): 79-103 (2006) - [j63]Leslie Lamport:
Lower bounds for asynchronous consensus. Distributed Comput. 19(2): 104-125 (2006) - [j62]Jim Gray, Leslie Lamport:
Consensus on transaction commit. ACM Trans. Database Syst. 31(1): 133-160 (2006) - [c57]Leslie Lamport:
The +CAL Algorithm Language. FORTE 2006: 23 - [c56]Leslie Lamport:
The +CAL Algorithm Language. NCA 2006: 5 - [c55]Leslie Lamport:
Checking a Multithreaded Algorithm with +CAL. DISC 2006: 151-163 - 2005
- [c54]Leslie Lamport:
Real-Time Model Checking Is Really Simple. CHARME 2005: 162-175 - [c53]Partha Dutta, Rachid Guerraoui, Leslie Lamport:
How Fast Can Eventual Synchrony Lead to Consensus?. DSN 2005: 22-27 - 2004
- [c52]Leslie Lamport:
Recent Discoveries from Paxos. DSN 2004: 3 - [c51]Leslie Lamport, Mike Massa:
Cheap Paxos. DSN 2004: 307-314 - [c50]James E. Johnson, David E. Langworthy, Leslie Lamport, Friedrich H. Vogt:
Formal Specification of a Web Services Protocol. WSFM 2004: 147-158 - [i1]Jim Gray, Leslie Lamport:
Consensus on Transaction Commit. CoRR cs.DC/0408036 (2004) - 2003
- [j61]Eli Gafni, Leslie Lamport:
Disk Paxos. Distributed Comput. 16(1): 1-20 (2003) - [j60]Leslie Lamport:
Arbitration-free synchronization. Distributed Comput. 16(2-3): 219-237 (2003) - [j59]Rajeev Joshi, Leslie Lamport, John Matthews, Serdar Tasiran, Mark R. Tuttle, Yuan Yu:
Checking Cache-Coherence Protocols with TLA+. Formal Methods Syst. Des. 22(2): 125-131 (2003) - [c49]Leslie Lamport:
Lower Bounds for Asynchronous Consensus. Future Directions in Distributed Computing 2003: 22-23 - 2002
- [b4]Leslie Lamport:
Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley 2002, ISBN 0-3211-4306-X - [c48]Brannon Batson, Leslie Lamport:
High-Level Specifications: Lessons from Industry. FMCO 2002: 242-261 - [c47]Leslie Lamport:
Paxos Made Simple, Fast, and Byzantine. OPODIS 2002: 7-9 - [c46]Leslie Lamport, John Matthews, Mark R. Tuttle, Yuan Yu:
Specifying and verifying systems with TLA+. ACM SIGOPS European Workshop 2002: 45-48 - 2000
- [j58]Leslie Lamport:
Fairness and hyperfairness. Distributed Comput. 13(4): 239-245 (2000) - [j57]Leslie Lamport, Sharon E. Perl, William E. Weihl:
When does a correct mutual exclusion algorithm guarantee mutual exclusion? Inf. Process. Lett. 76(3): 131-134 (2000) - [c45]Leslie Lamport:
Distributed algorithms in TLA (abstract). PODC 2000: 3 - [c44]Eli Gafni, Leslie Lamport:
Disk Paxos. DISC 2000: 330-344
1990 – 1999
- 1999
- [j56]Peter B. Ladkin, Leslie Lamport, Bryan Olivier, Denis Roegel:
Lazy Caching in TLA. Distributed Comput. 12(2-3): 151-174 (1999) - [j55]Leslie Lamport, Lawrence C. Paulson:
Should your specification language be typed. ACM Trans. Program. Lang. Syst. 21(3): 502-526 (1999) - [c43]Yuan Yu, Panagiotis Manolios, Leslie Lamport:
Model Checking TLA+ Specifications. CHARME 1999: 54-66 - [c42]Homayoon Akhiani, Damien Doligez, Paul Harter, Leslie Lamport, Joshua Scheid, Mark R. Tuttle, Yuan Yu:
Cache Coherence Verification with TLA+. World Congress on Formal Methods 1999: 1871-1872 - 1998
- [j54]Leslie Lamport:
Proving Possibility Properties. Theor. Comput. Sci. 206(1-2): 341-352 (1998) - [j53]Leslie Lamport:
The Part-Time Parliament. ACM Trans. Comput. Syst. 16(2): 133-169 (1998) - [c41]Ernie Cohen, Leslie Lamport:
Reduction in TLA. CONCUR 1998: 317-331 - 1997
- [j52]Leslie Lamport:
How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor. IEEE Trans. Computers 46(7): 779-782 (1997) - [j51]Leslie Lamport:
Processes are in the Eye of the Beholder. Theor. Comput. Sci. 179(1-2): 333-351 (1997) - [c40]Leslie Lamport:
Composition: A Way to Make Proofs Harder. COMPOS 1997: 402-423 - 1996
- [c39]Leslie Lamport:
Managing Proofs (Abstract). TACAS 1996: 34 - 1995
- [b3]Leslie Lamport:
Das LaTeX-Handbuch. Addison-Wesley 1995, ISBN 978-3-89319-826-9, pp. I-XVIII, 1-325 - [j50]Martín Abadi, Leslie Lamport:
Conjoining Specifications. ACM Trans. Program. Lang. Syst. 17(3): 507-534 (1995) - [j49]Leslie Lamport:
TLA in Pictures. IEEE Trans. Software Eng. 21(9): 768-775 (1995) - 1994
- [b2]Leslie Lamport:
LaTeX - A Document Preparation System: User's Guide and Reference Manual, Second Edition. Pearson / Prentice Hall 1994, ISBN 978-0-201-52983-8, pp. I-XVI, 1-272 - [j48]Leslie Lamport:
How to Write a Long Formula (Short Communication). Formal Aspects Comput. 6(5): 580-584 (1994) - [j47]Leslie Lamport:
The Temporal Logic of Actions. ACM Trans. Program. Lang. Syst. 16(3): 872-923 (1994) - [j46]Martín Abadi, Leslie Lamport:
An Old-Fashined Recipe for Real-Time. ACM Trans. Program. Lang. Syst. 16(5): 1543-1571 (1994) - [c38]Manfred Broy, Leslie Lamport:
The RPC-Memory Specification Problem - Problem Statement. Formal Systems Specification 1994: 1-4 - [c37]Martín Abadi, Leslie Lamport, Stephan Merz:
A TLA Solution to the RPC-Memory Specification Problem. Formal Systems Specification 1994: 21-66 - [c36]Leslie Lamport:
TLA in Pictures. Specification of Parallel Algorithms 1994: 293-307 - [c35]Leslie Lamport:
How good is your specification method? FORTE 1994: 289 - [c34]Leslie Lamport, Stephan Merz:
Specifying and Verifying Fault-Tolerant Systems. FTRTFT 1994: 41-76 - [c33]Martín Abadi, Leslie Lamport:
Open Systems in TLA. PODC 1994: 81-90 - [c32]Martín Abadi, Leslie Lamport:
Decomposing Specifications of Concurrent Systems. PROCOMET 1994: 327-340 - [c31]Leslie Lamport:
TLZ. Z User Workshop 1994: 267-268 - 1993
- [j45]Martín Abadi, Leslie Lamport:
Composing Specifications. ACM Trans. Program. Lang. Syst. 15(1): 73-132 (1993) - [c30]Robert P. Kurshan, Leslie Lamport:
Verification of a Multiplier: 64 Bits and Beyond. CAV 1993: 166-179 - [c29]Leslie Lamport:
Verification and Specifications of Concurrent Programs. REX School/Symposium 1993: 347-374 - 1992
- [j44]Leslie Lamport:
Critique of the Lake Arrowhead Three. Distributed Comput. 6(1): 65-71 (1992) - [c28]Leslie Lamport:
Computer-Hindered Verification (Humans Can Do It Too). CAV 1992: 1 - [c27]Urban Engberg, Peter Grønning, Leslie Lamport:
Mechanical Verification of Concurrent Systems with TLA. CAV 1992: 44-55 - [c26]Leslie Lamport:
Hybrid Systems in TLA+. Hybrid Systems 1992: 77-102 - [c25]Urban Engberg, Peter Grønning, Leslie Lamport:
Mechanical Verification of Concurrent Systems with TLA. Larch 1992: 86-97 - 1991
- [j43]Martín Abadi, Bowen Alpern, Krzysztof R. Apt, Nissim Francez, Shmuel Katz, Leslie Lamport, Fred B. Schneider:
Preserving Liveness: Comments on "Safety and Liveness from a Methodological Point of View". Inf. Process. Lett. 40(3): 141-142 (1991) - [j42]Martín Abadi, Leslie Lamport:
The Existence of Refinement Mappings. Theor. Comput. Sci. 82(2): 253-284 (1991) - [c24]Martín Abadi, Leslie Lamport:
An Old-Fashioned Recipe for Real Time. REX Workshop 1991: 1-27 - 1990
- [j41]Leslie Lamport:
A Theorem on Atomicity in Distributed Algorithms. Distributed Comput. 4: 59-68 (1990) - [j40]Leslie Lamport:
Concurrent Reading and Writing of Clocks. ACM Trans. Comput. Syst. 8(4): 305-310 (1990) - [j39]Leslie Lamport:
win and sin: Predicate Transformers for Concurrency. ACM Trans. Program. Lang. Syst. 12(3): 396-428 (1990) - [p1]Leslie Lamport, Nancy A. Lynch:
Distributed Computing: Models and Methods. Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B) 1990: 1157-1199
1980 – 1989
- 1989
- [j38]Leslie Lamport:
A Simple Approach to Specifying Concurrent Systems. Commun. ACM 32(1): 32-45 (1989) - [c23]Martín Abadi, Leslie Lamport, Pierre Wolper:
Realizable and Unrealizable Specifications of Reactive Systems. ICALP 1989: 1-17 - [c22]Martín Abadi, Leslie Lamport:
Composing Specifications. REX Workshop 1989: 1-41 - 1988
- [j37]Fred B. Schneider, Leslie Lamport:
On E. W. Dijkstra's position paper on "fairness: ". ACM SIGSOFT Softw. Eng. Notes 13(3): 18-19 (1988) - [j36]Leslie Lamport:
Control Predicates are Better than Dummy Variables for Reasoning about Program Control. ACM Trans. Program. Lang. Syst. 10(2): 267-281 (1988) - [c21]Leslie Lamport:
While Waiting for the Millennium: Formal Specification and Verficiation of Concurrent Systems Now (Abstract). Concurrency 1988: 3 - [c20]Martín Abadi, Leslie Lamport:
The Existence of Refinement Mappings. LICS 1988: 165-175 - [c19]Jennifer L. Welch, Leslie Lamport, Nancy A. Lynch:
A Lattice-Structured Proof of a Minimum Spanning. PODC 1988: 28-43 - 1987
- [j35]Leslie Lamport:
A Fast Mutual Exclusion Algorithm. ACM Trans. Comput. Syst. 5(1): 1-11 (1987) - 1986
- [b1]Leslie Lamport:
LaTeX: User's Guide & Reference Manual. Addison-Wesley 1986, ISBN 0-201-15790-X - [j34]Leslie Lamport:
On Interprocess Communication. Part I: Basic Formalism. Distributed Comput. 1(2): 77-85 (1986) - [j33]Leslie Lamport:
On Interprocess Communication. Part II: Algorithms. Distributed Comput. 1(2): 86-101 (1986) - [j32]Leslie Lamport:
The mutual exclusion problem: part I - a theory of interprocess communication. J. ACM 33(2): 313-326 (1986) - [j31]Leslie Lamport:
The mutual exclusion problem: partII - statement and solutions. J. ACM 33(2): 327-348 (1986) - [j30]Leslie Lamport, P. M. Melliar-Smith:
Byzantine Clock Synchronization. ACM SIGOPS Oper. Syst. Rev. 20(3): 10-16 (1986) - 1985
- [j29]Leslie Lamport, P. M. Melliar-Smith:
Synchronizing Clocks in the Presence of Faults. J. ACM 32(1): 52-78 (1985) - [j28]Leslie Lamport:
Solved Problems, Unsolved Problems and Non-Problems in Concurrency. ACM SIGOPS Oper. Syst. Rev. 19(4): 34-44 (1985) - [j27]