Leslie Lamport

Affiliations:
  • Microsoft Research, Mountain View


According to our database1, Leslie Lamport authored at least 157 papers between 1970 and 2022.

Collaborative distances:
  • Dijkstra number2 of one.
  • Erdős number3 of three.

Awards

Turing Prize recipient

Turing Prize 2013, "For fundamental contributions to the theory and practice of distributed and concurrent systems, notably the invention of concepts such as causality and logical clocks, safety and liveness, replicated state machines, and sequential consistency.".

ACM Fellow

ACM Fellow 2014, "For contributions to the theory and practice of distributed and concurrent systems".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2022
Prophecy Made Simple.
ACM Trans. Program. Lang. Syst., 2022

Mathematical Proof Between Generations.
CoRR, 2022

Deconstructing the bakery to build a distributed state machine.
Commun. ACM, 2022

Concurrent Algorithms.
Proceedings of the Edsger Wybe Dijkstra: His Life, Work, and Legacy, 2022

On-the-Fly Garbage Collection: An Exercise in Cooperation.
Proceedings of the Edsger Wybe Dijkstra: His Life, Work, and Legacy, 2022

2021
Verifying Hyperproperties With TLA.
Proceedings of the 34th IEEE Computer Security Foundations Symposium, 2021

2019
The TLA+ Toolbox.
Proceedings of the Proceedings Fifth Workshop on Formal Integrated Development Environment, 2019

The Byzantine generals problem.
Proceedings of the Concurrency: the Works of Leslie Lamport, 2019

The part-time parliament.
Proceedings of the Concurrency: the Works of Leslie Lamport, 2019

The mutual exclusion problem: part II - Statement and solutions.
Proceedings of the Concurrency: the Works of Leslie Lamport, 2019

The mutual exclusion problem: part I - A theory of interprocess communication.
Proceedings of the Concurrency: the Works of Leslie Lamport, 2019

How to make a multiprocessor computer that correctly executes multiprocess programs.
Proceedings of the Concurrency: the Works of Leslie Lamport, 2019

Time, clocks, and the ordering of events in a distributed system.
Proceedings of the Concurrency: the Works of Leslie Lamport, 2019

A new solution of Dijkstra's concurrent programming problem.
Proceedings of the Concurrency: the Works of Leslie Lamport, 2019

The computer science of concurrency: the early years.
Proceedings of the Concurrency: the Works of Leslie Lamport, 2019

2018
If You're Not Writing a Program, Don't Use a Programming Language.
Bull. EATCS, 2018

2017
On the Glitch Phenomenon.
CoRR, 2017

Auxiliary Variables in TLA+.
CoRR, 2017

2015
Turing lecture: The computer science of concurrency: the early years.
Commun. ACM, 2015

Who builds a house without drawing blueprints?
Commun. ACM, 2015

2014
An incomplete history of concurrency chapter 1. 1965-1977.
Proceedings of the ACM Symposium on Principles of Distributed Computing, 2014

Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics.
Proceedings of the Automated Reasoning in Quantified Non-Classical Logics, 2014

2013
Adaptive Register Allocation with a Linear Number of Registers.
Proceedings of the Distributed Computing - 27th International Symposium, 2013

2012
TLA + Proofs.
Proceedings of the FM 2012: Formal Methods, 2012

2011
Euclid Writes an Algorithm: A Fairytale.
Int. J. Softw. Informatics, 2011

Byzantizing Paxos by Refinement.
Proceedings of the Distributed Computing - 25th International Symposium, 2011

Brief Announcement: Leaderless Byzantine Paxos.
Proceedings of the Distributed Computing - 25th International Symposium, 2011

2010
Reconfiguring a state machine.
SIGACT News, 2010

The mailbox problem.
Distributed Comput., 2010

The TLA<sup>+</sup> Proof System: Building a Heterogeneous Verification Platform.
Proceedings of the Theoretical Aspects of Computing, 2010

Verifying Safety Properties with the TLA+ Proof System.
Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

Computer Science and State Machines.
Proceedings of the Concurrency, 2010

2009
Teaching concurrency.
SIGACT News, 2009

Vertical paxos and primary-backup replication.
Proceedings of the 28th Annual ACM Symposium on Principles of Distributed Computing, 2009

TLA+: Whence, Wherefore, and Whither.
Proceedings of the First NASA Formal Methods Symposium, 2009

The PlusCal Algorithm Language.
Proceedings of the Theoretical Aspects of Computing, 2009

2008
Implementing dataflow with threads.
Distributed Comput., 2008

A TLA+ Proof System.
Proceedings of the LPAR 2008 Workshops, 2008

2007
Formal specification of a Web services protocol.
J. Log. Algebraic Methods Program., 2007

DISC 20th Anniversary: Invited Talk Time, Clocks, and the Ordering of My Ideas About Distributed Systems.
Proceedings of the Distributed Computing, 21st International Symposium, 2007

2006
Consensus on transaction commit.
ACM Trans. Database Syst., 2006

Lower bounds for asynchronous consensus.
Distributed Comput., 2006

Fast Paxos.
Distributed Comput., 2006

Checking a Multithreaded Algorithm with <sup>+</sup>CAL.
Proceedings of the Distributed Computing, 20th International Symposium, 2006

The +CAL Algorithm Language.
Proceedings of the Fifth IEEE International Symposium on Network Computing and Applications, 2006

The <sup>+</sup>CAL Algorithm Language.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2006

2005
How Fast Can Eventual Synchrony Lead to Consensus?.
Proceedings of the 2005 International Conference on Dependable Systems and Networks (DSN 2005), 28 June, 2005

Real-Time Model Checking Is Really Simple.
Proceedings of the Correct Hardware Design and Verification Methods, 2005

2004
Cheap Paxos.
Proceedings of the 2004 International Conference on Dependable Systems and Networks (DSN 2004), 28 June, 2004

Recent Discoveries from Paxos.
Proceedings of the 2004 International Conference on Dependable Systems and Networks (DSN 2004), 28 June, 2004

2003
Checking Cache-Coherence Protocols with TLA<sup>+</sup>.
Formal Methods Syst. Des., 2003

Arbitration-free synchronization.
Distributed Comput., 2003

Disk Paxos.
Distributed Comput., 2003

2002
Specifying and verifying systems with TLA+.
Proceedings of the 10th ACM SIGOPS European Workshop, Saint-Emilion, France, July 1, 2002, 2002

Paxos Made Simple, Fast, and Byzantine.
Proceedings of the Procedings of the 6th International Conference on Principles of Distributed Systems. OPODIS 2002, 2002

High-Level Specifications: Lessons from Industry.
Proceedings of the Formal Methods for Components and Objects, 2002

Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers
Addison-Wesley, ISBN: 0-3211-4306-X, 2002

2000
When does a correct mutual exclusion algorithm guarantee mutual exclusion?
Inf. Process. Lett., 2000

Fairness and hyperfairness.
Distributed Comput., 2000

Distributed algorithms in TLA (abstract).
Proceedings of the Nineteenth Annual ACM Symposium on Principles of Distributed Computing, 2000

1999
Should your specification language be typed.
ACM Trans. Program. Lang. Syst., 1999

Lazy Caching in TLA.
Distributed Comput., 1999

Cache Coherence Verification with TLA+.
Proceedings of the FM'99 - Formal Methods, 1999

Model Checking TLA<sup>+</sup> Specifications.
Proceedings of the Correct Hardware Design and Verification Methods, 1999

1998
The Part-Time Parliament.
ACM Trans. Comput. Syst., 1998

Proving Possibility Properties.
Theor. Comput. Sci., 1998

Reduction in TLA.
Proceedings of the CONCUR '98: Concurrency Theory, 1998

1997
Processes are in the Eye of the Beholder.
Theor. Comput. Sci., 1997

How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor.
IEEE Trans. Computers, 1997

Composition: A Way to Make Proofs Harder.
Proceedings of the Compositionality: The Significant Difference, International Symposium, 1997

1996
Managing Proofs (Abstract).
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1996

1995
TLA in Pictures.
IEEE Trans. Software Eng., 1995

Conjoining Specifications.
ACM Trans. Program. Lang. Syst., 1995

Das LaTeX-Handbuch.
Addison-Wesley, ISBN: 978-3-89319-826-9, 1995

1994
The Temporal Logic of Actions.
ACM Trans. Program. Lang. Syst., 1994

An Old-Fashined Recipe for Real-Time.
ACM Trans. Program. Lang. Syst., 1994

How to Write a Long Formula (Short Communication).
Formal Aspects Comput., 1994

Proceedings of the Z User Workshop, Cambridge, UK, 29-30 June 1994, Proceedings, 1994

Decomposing Specifications of Concurrent Systems.
Proceedings of the Programming Concepts, 1994

Open Systems in TLA.
Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing, 1994

Specifying and Verifying Fault-Tolerant Systems.
Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, Third International Symposium Organized Jointly with the Working Group Provably Correct Systems, 1994

How good is your specification method?
Proceedings of the Formal Description Techniques VII, 1994

The RPC-Memory Specification Problem - Problem Statement.
Proceedings of the Formal Systems Specification, 1994

A TLA Solution to the RPC-Memory Specification Problem.
Proceedings of the Formal Systems Specification, 1994

LaTeX - A Document Preparation System: User's Guide and Reference Manual, Second Edition.
Pearson / Prentice Hall, ISBN: 978-0-201-52983-8, 1994

1993
Composing Specifications.
ACM Trans. Program. Lang. Syst., 1993

Verification and Specifications of Concurrent Programs.
Proceedings of the A Decade of Concurrency, Reflections and Perspectives, 1993

Verification of a Multiplier: 64 Bits and Beyond.
Proceedings of the Computer Aided Verification, 5th International Conference, 1993

1992
Critique of the Lake Arrowhead Three.
Distributed Comput., 1992

Hybrid Systems in TLA<sup>+</sup>.
Proceedings of the Hybrid Systems, 1992

Computer-Hindered Verification (Humans Can Do It Too).
Proceedings of the Computer Aided Verification, Fourth International Workshop, 1992

Mechanical Verification of Concurrent Systems with TLA.
Proceedings of the Computer Aided Verification, Fourth International Workshop, 1992

1991
The Existence of Refinement Mappings.
Theor. Comput. Sci., 1991

Preserving Liveness: Comments on "Safety and Liveness from a Methodological Point of View".
Inf. Process. Lett., 1991

An Old-Fashioned Recipe for Real Time.
Proceedings of the Real-Time: Theory in Practice, 1991

1990
<i>win</i> and <i>sin</i>: Predicate Transformers for Concurrency.
ACM Trans. Program. Lang. Syst., 1990

Concurrent Reading and Writing of Clocks.
ACM Trans. Comput. Syst., 1990

A Theorem on Atomicity in Distributed Algorithms.
Distributed Comput., 1990

Distributed Computing: Models and Methods.
Proceedings of the Handbook of Theoretical Computer Science, 1990

1989
A Simple Approach to Specifying Concurrent Systems.
Commun. ACM, 1989

Realizable and Unrealizable Specifications of Reactive Systems.
Proceedings of the Automata, Languages and Programming, 16th International Colloquium, 1989

1988
Control Predicates are Better than Dummy Variables for Reasoning about Program Control.
ACM Trans. Program. Lang. Syst., 1988

On E. W. Dijkstra's position paper on "fairness: ".
ACM SIGSOFT Softw. Eng. Notes, 1988

A Lattice-Structured Proof of a Minimum Spanning.
Proceedings of the Seventh Annual ACM Symposium on Principles of Distributed Computing, 1988

While Waiting for the Millennium: Formal Specification and Verficiation of Concurrent Systems Now (Abstract).
Proceedings of the Concurrency 88: International Conference on Concurrency, 1988

1987
A Fast Mutual Exclusion Algorithm.
ACM Trans. Comput. Syst., 1987

1986
Byzantine Clock Synchronization.
ACM SIGOPS Oper. Syst. Rev., 1986

The mutual exclusion problem: partII - statement and solutions.
J. ACM, 1986

The mutual exclusion problem: part I - a theory of interprocess communication.
J. ACM, 1986

On Interprocess Communication. Part II: Algorithms.
Distributed Comput., 1986

On Interprocess Communication. Part I: Basic Formalism.
Distributed Comput., 1986

LaTeX: User's Guide & Reference Manual
Addison-Wesley, ISBN: 0-201-15790-X, 1986

1985
Synchronizing Clocks in the Presence of Faults
J. ACM, January, 1985

Distributed Snapshots: Determining Global States of Distributed Systems
ACM Trans. Comput. Syst., 1985

Solved Problems, Unsolved Problems and Non-Problems in Concurrency.
ACM SIGOPS Oper. Syst. Rev., 1985

Constraints: A Uniform Approach to Aliasing and Typing.
Proceedings of the Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, 1985

What It Means for a Concurrent Program to Satisfy a Specification: Why No One Has Specified Priority.
Proceedings of the Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, 1985

1984
The "Hoare Logic" of CSP, and All That.
ACM Trans. Program. Lang. Syst., 1984

Using Time Instead of Timeout for Fault-Tolerant Distributed Systems.
ACM Trans. Program. Lang. Syst., 1984

Solved Problems, Unsolved Problems and Non-Problems in Concurrency (Invited Address).
Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing, 1984

An Axiomatic Semantics of Concurrent Programming Languages.
Proceedings of the Logics and Models of Concurrent Systems, 1984

Paradigms for Distributed Programs.
Proceedings of the Distributed Systems: Methods and Tools for Specification, 1984

Formal Foundation for Specification and Verification.
Proceedings of the Distributed Systems: Methods and Tools for Specification, 1984

Basic Concepts.
Proceedings of the Distributed Systems: Methods and Tools for Specification, 1984

1983
The Weak Byzantine Generals Problem
J. ACM, July, 1983

Specifying Concurrent Program Modules.
ACM Trans. Program. Lang. Syst., 1983

Reasoning About Nonatomic Operations.
Proceedings of the Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, 1983

What Good is Temporal Logic?
Proceedings of the Information Processing 83, 1983

Problems from the Workshop on the Analysis of Concurrent Systems.
Proceedings of the Analysis of Concurrent Systems, 1983

1982
Proving Liveness Properties of Concurrent Programs.
ACM Trans. Program. Lang. Syst., 1982

The Byzantine Generals Problem.
ACM Trans. Program. Lang. Syst., 1982

An Assertional Correctness Proof of a Distributed Algorithm.
Sci. Comput. Program., 1982

1981
Password Authentification with Insecure Communication.
Commun. ACM, 1981

Program Logics and Program Verification (position paper).
Proceedings of the Logics of Programs, Workshop, Yorktown Heights, New York, USA, May 1981, 1981

TIMESETS -- A New Method for Temporal Reasoning about Programs.
Proceedings of the Logics of Programs, Workshop, Yorktown Heights, New York, USA, May 1981, 1981

1980
Reaching Agreement in the Presence of Faults.
J. ACM, 1980

The 'Hoare Logic' of Concurrent Programs.
Acta Informatica, 1980

"Sometime" is Sometimes "Not Never" - On the Temporal Logic of Programs.
Proceedings of the Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, 1980

1979
A New Approach to Proving the Correctness of Multiprocess Programs.
ACM Trans. Program. Lang. Syst., 1979

How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs.
IEEE Trans. Computers, 1979

A general construction for expressing repetition.
ACM SIGPLAN Notices, 1979

On the Proof of Correctness of a Calendar Program.
Commun. ACM, 1979

1978
State the problem before describing the solution.
ACM SIGSOFT Softw. Eng. Notes, 1978

The Implementation of Reliable Distributed Multiprocess Systems.
Comput. Networks, 1978

Time, Clocks, and the Ordering of Events in a Distributed System.
Commun. ACM, 1978

On-the-Fly Garbage Collection: An Exercise in Cooperation.
Commun. ACM, 1978

The specification and proof of correctness of interactive programs.
Proceedings of the Mathematical Studies of Information Processing, 1978

1977
Proving the Correctness of Multiprocess Programs.
IEEE Trans. Software Eng., 1977

Concurrent Reading and Writing.
Commun. ACM, 1977

1976
Comments on "A Synchronization Anomaly".
Inf. Process. Lett., 1976

The Synchronization of Independent Processes.
Acta Informatica, 1976

1975
Multiple Byte Processing with Full-Word Instructions.
Commun. ACM, 1975

On programming parallel computers.
Proceedings of the Conference on Programming Languages and Compilers for Parallel and Vector Machines 1975, 1975

1974
A New Solution of Dijkstra's Concurrent Programming Problem.
Commun. ACM, 1974

The Parallel Execution of DO Loops.
Commun. ACM, 1974

The Hyperplane Method for an Array Computer.
Proceedings of the Parallel Processing, Proceedings of the Sagamore Computer Conference, 1974

1970
Comment on Bell's quadratic quotient method for hash coded searching.
Commun. ACM, 1970


  Loading...