Leslie Lamport

173 papers A* 16A 13B 4C 4Journal 83Unranked 37
YearRankTypeTitle / Venue / Authors
2025 J jnl
A Retrospective of Proving the Correctness of Multiprocess Programs.
IEEE Trans. Software Eng.
Leslie Lamport
2022 — ch.
Concurrent Algorithms.
Edsger Wybe Dijkstra
Leslie Lamport
2022 J jnl
Deconstructing the bakery to build a distributed state machine.
Commun. ACM
Leslie Lamport
2022 J jnl
Mathematical Proof Between Generations.
CoRR
Jonas Bayer, Christoph Benzmüller, Kevin Buzzard, Marco David, Leslie Lamport, Yuri V. Matiyasevich, Lawrence C. Paulson, Dierk Schleicher, Benedikt Stock, Efim I. Zelmanov
2022 — ch.
On-the-Fly Garbage Collection: An Exercise in Cooperation.
Edsger Wybe Dijkstra
Edsger W. Dijkstra, Leslie Lamport, Alain J. Martin, Carel S. Scholten, Elisabeth F. M. Steffens
2022 J jnl
Prophecy Made Simple.
ACM Trans. Program. Lang. Syst.
Leslie Lamport, Stephan Merz
2021 A conf
Verifying Hyperproperties With TLA.
CSF
Leslie Lamport, Fred B. Schneider
2019 — ch.
A new solution of Dijkstra's concurrent programming problem.
Concurrency: the Works of Leslie Lamport
Leslie Lamport
2019 — ch.
How to make a multiprocessor computer that correctly executes multiprocess programs.
Concurrency: the Works of Leslie Lamport
Leslie Lamport
2019 — ch.
The Byzantine generals problem.
Concurrency: the Works of Leslie Lamport
Leslie Lamport, Robert E. Shostak, Marshall C. Pease
2019 — conf
The TLA+ Toolbox.
F-IDE@FM
Markus Alexander Kuppe, Leslie Lamport, Daniel Ricketts
2019 — ch.
The computer science of concurrency: the early years.
Concurrency: the Works of Leslie Lamport
Leslie Lamport
2019 — ch.
The mutual exclusion problem: part I - A theory of interprocess communication.
Concurrency: the Works of Leslie Lamport
Leslie Lamport
2019 — ch.
The mutual exclusion problem: part II - Statement and solutions.
Concurrency: the Works of Leslie Lamport
Leslie Lamport
2019 — ch.
The part-time parliament.
Concurrency: the Works of Leslie Lamport
Leslie Lamport
2019 — ch.
Time, clocks, and the ordering of events in a distributed system.
Concurrency: the Works of Leslie Lamport
Leslie Lamport
2018 J jnl
If You're Not Writing a Program, Don't Use a Programming Language.
Bull. EATCS
Leslie Lamport
2017 J jnl
Auxiliary Variables in TLA+.
CoRR
Leslie Lamport, Stephan Merz
2017 J jnl
On the Glitch Phenomenon.
CoRR
Leslie Lamport, Richard Palais
2015 J jnl
Turing lecture: The computer science of concurrency: the early years.
Commun. ACM
Leslie Lamport
2015 J jnl
Who builds a house without drawing blueprints?
Commun. ACM
Leslie Lamport
2014 A* conf
An incomplete history of concurrency chapter 1. 1965-1977.
PODC
Leslie Lamport
2014 — conf
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics.
ARQNL@IJCAR
Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz
2014 J jnl
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics.
CoRR
Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz
2013 A conf
Adaptive Register Allocation with a Linear Number of Registers.
DISC
Carole Delporte-Gallet, Hugues Fauconnier, Eli Gafni, Leslie Lamport
2012 B conf
TLA + Proofs.
FM
Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto
2012 J jnl
TLA+ Proofs
CoRR
Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto
2011 A conf
Brief Announcement: Leaderless Byzantine Paxos.
DISC
Leslie Lamport
2011 A conf
Byzantizing Paxos by Refinement.
DISC
Leslie Lamport
2011 J jnl
Euclid Writes an Algorithm: A Fairytale.
Int. J. Softw. Informatics
Leslie Lamport
2010 — conf
Computer Science and State Machines.
Concurrency, Compositionality, and Correctness
Leslie Lamport
2010 J jnl
Reconfiguring a state machine.
SIGACT News
Leslie Lamport, Dahlia Malkhi, Lidong Zhou
2010 C conf
The TLA
ICTAC
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
2010 J jnl
The mailbox problem.
Distributed Comput.
Marcos Kawazoe Aguilera, Eli Gafni, Leslie Lamport
2010 J jnl
Verifying Safety Properties With the TLA+ Proof System
CoRR
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
2010 A conf
Verifying Safety Properties with the TLA+ Proof System.
IJCAR
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
2009 — conf
TLA+: Whence, Wherefore, and Whither.
NASA Formal Methods
Leslie Lamport
2009 J jnl
Teaching concurrency.
SIGACT News
Leslie Lamport
2009 C conf
The PlusCal Algorithm Language.
ICTAC
Leslie Lamport
2009 A* conf
Vertical paxos and primary-backup replication.
PODC
Leslie Lamport, Dahlia Malkhi, Lidong Zhou
2008 J jnl
A TLA+ Proof System
CoRR
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
2008 — conf
A TLA+ Proof System.
LPAR Workshops
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
2008 J jnl
Implementing dataflow with threads.
Distributed Comput.
Leslie Lamport
2008 A conf
The Mailbox Problem.
DISC
Marcos Kawazoe Aguilera, Eli Gafni, Leslie Lamport
2007 A conf
DISC 20th Anniversary: Invited Talk Time, Clocks, and the Ordering of My Ideas About Distributed Systems.
DISC
Leslie Lamport
2007 J jnl
Formal specification of a Web services protocol.
J. Log. Algebraic Methods Program.
James E. Johnson, David E. Langworthy, Leslie Lamport, Friedrich H. Vogt
2006 A conf
Checking a Multithreaded Algorithm with
DISC
Leslie Lamport
2006 J jnl
Consensus on transaction commit.
ACM Trans. Database Syst.
Jim Gray, Leslie Lamport
2006 J jnl
Fast Paxos.
Distributed Comput.
Leslie Lamport
2006 J jnl
Lower bounds for asynchronous consensus.
Distributed Comput.
Leslie Lamport
2006 C conf
The
FORTE
Leslie Lamport
2006 B conf
The +CAL Algorithm Language.
NCA
Leslie Lamport
2005 A conf
How Fast Can Eventual Synchrony Lead to Consensus?.
DSN
Partha Dutta, Rachid Guerraoui, Leslie Lamport
2005 — conf
Real-Time Model Checking Is Really Simple.
CHARME
Leslie Lamport
2004 A conf
Cheap Paxos.
DSN
Leslie Lamport, Mike Massa
2004 J jnl
Consensus on Transaction Commit
CoRR
Jim Gray, Leslie Lamport
2004 — conf
Formal Specification of a Web Services Protocol.
WSFM
James E. Johnson, David E. Langworthy, Leslie Lamport, Friedrich H. Vogt
2004 A conf
Recent Discoveries from Paxos.
DSN
Leslie Lamport
2003 J jnl
Arbitration-free synchronization.
Distributed Comput.
Leslie Lamport
2003 J jnl
Checking Cache-Coherence Protocols with TLA
Formal Methods Syst. Des.
Rajeev Joshi, Leslie Lamport, John Matthews, Serdar Tasiran, Mark R. Tuttle, Yuan Yu
2003 J jnl
Disk Paxos.
Distributed Comput.
Eli Gafni, Leslie Lamport
2003 — conf
Lower Bounds for Asynchronous Consensus.
Future Directions in Distributed Computing
Leslie Lamport
2002 — conf
High-Level Specifications: Lessons from Industry.
FMCO
Brannon Batson, Leslie Lamport
2002 B conf
Paxos Made Simple, Fast, and Byzantine.
OPODIS
Leslie Lamport
2002 — book
Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers
Leslie Lamport
2002 — conf
Specifying and verifying systems with TLA+.
ACM SIGOPS European Workshop
Leslie Lamport, John Matthews, Mark R. Tuttle, Yuan Yu
2000 A conf
Disk Paxos.
DISC
Eli Gafni, Leslie Lamport
2000 A* conf
Distributed algorithms in TLA (abstract).
PODC
Leslie Lamport
2000 J jnl
Fairness and hyperfairness.
Distributed Comput.
Leslie Lamport
2000 J jnl
When does a correct mutual exclusion algorithm guarantee mutual exclusion?
Inf. Process. Lett.
Leslie Lamport, Sharon E. Perl, William E. Weihl
1999 — conf
Cache Coherence Verification with TLA+.
World Congress on Formal Methods
Homayoon Akhiani, Damien Doligez, Paul Harter, Leslie Lamport, Joshua Scheid, Mark R. Tuttle, Yuan Yu
1999 J jnl
Lazy Caching in TLA.
Distributed Comput.
Peter B. Ladkin, Leslie Lamport, Bryan Olivier, Denis Roegel
1999 — conf
Model Checking TLA
CHARME
Yuan Yu, Panagiotis Manolios, Leslie Lamport
1999 J jnl
Should your specification language be typed.
ACM Trans. Program. Lang. Syst.
Leslie Lamport, Lawrence C. Paulson
1998 J jnl
Proving Possibility Properties.
Theor. Comput. Sci.
Leslie Lamport
1998 B conf
Reduction in TLA.
CONCUR
Ernie Cohen, Leslie Lamport
1998 J jnl
The Part-Time Parliament.
ACM Trans. Comput. Syst.
Leslie Lamport
1997 — conf
Composition: A Way to Make Proofs Harder.
COMPOS
Leslie Lamport
1997 J jnl
How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor.
IEEE Trans. Computers
Leslie Lamport
1997 J jnl
Processes are in the Eye of the Beholder.
Theor. Comput. Sci.
Leslie Lamport
1996 A conf
Managing Proofs (Abstract).
TACAS
Leslie Lamport
1995 J jnl
Conjoining Specifications.
ACM Trans. Program. Lang. Syst.
Martín Abadi, Leslie Lamport
1995 — book
Das LaTeX-Handbuch.
Leslie Lamport
1995 J jnl
TLA in Pictures.
IEEE Trans. Software Eng.
Leslie Lamport
1994 — conf
A TLA Solution to the RPC-Memory Specification Problem.
Formal Systems Specification
Martín Abadi, Leslie Lamport, Stephan Merz
1994 J jnl
An Old-Fashined Recipe for Real-Time.
ACM Trans. Program. Lang. Syst.
Martín Abadi, Leslie Lamport
1994 — conf
Decomposing Specifications of Concurrent Systems.
PROCOMET
Martín Abadi, Leslie Lamport
1994 C conf
How good is your specification method?
FORTE
Leslie Lamport
1994 J jnl
How to Write a Long Formula (Short Communication).
Formal Aspects Comput.
Leslie Lamport
1994 — book
LaTeX - A Document Preparation System: User's Guide and Reference Manual, Second Edition.
Leslie Lamport
1994 A* conf
Open Systems in TLA.
PODC
Martín Abadi, Leslie Lamport
1994 — conf
Specifying and Verifying Fault-Tolerant Systems.
FTRTFT
Leslie Lamport, Stephan Merz
1994 — conf
TLA in Pictures.
Specification of Parallel Algorithms
Leslie Lamport
1994 — conf
TLZ.
Z User Workshop
Leslie Lamport
1994 — conf
The RPC-Memory Specification Problem - Problem Statement.
Formal Systems Specification
Manfred Broy, Leslie Lamport
1994 J jnl
The Temporal Logic of Actions.
ACM Trans. Program. Lang. Syst.
Leslie Lamport
1993 J jnl
Composing Specifications.
ACM Trans. Program. Lang. Syst.
Martín Abadi, Leslie Lamport
1993 — conf
Verification and Specifications of Concurrent Programs.
REX School/Symposium
Leslie Lamport
1993 A* conf
Verification of a Multiplier: 64 Bits and Beyond.
CAV
Robert P. Kurshan, Leslie Lamport
1992 A* conf
Computer-Hindered Verification (Humans Can Do It Too).
CAV
Leslie Lamport
1992 J jnl
Critique of the Lake Arrowhead Three.
Distributed Comput.
Leslie Lamport
1992 — conf
Hybrid Systems in TLA
Hybrid Systems
Leslie Lamport
1992 A* conf
Mechanical Verification of Concurrent Systems with TLA.
CAV
Urban Engberg, Peter Grønning, Leslie Lamport
1992 — conf
Mechanical Verification of Concurrent Systems with TLA.
Larch
Urban Engberg, Peter Grønning, Leslie Lamport
1991 — conf
An Old-Fashioned Recipe for Real Time.
REX Workshop
Martín Abadi, Leslie Lamport
1991 J jnl
Preserving Liveness: Comments on "Safety and Liveness from a Methodological Point of View".
Inf. Process. Lett.
Martín Abadi, Bowen Alpern, Krzysztof R. Apt, Nissim Francez, Shmuel Katz, Leslie Lamport, Fred B. Schneider
1991 J jnl
The Existence of Refinement Mappings.
Theor. Comput. Sci.
Martín Abadi, Leslie Lamport
1990 J jnl
A Theorem on Atomicity in Distributed Algorithms.
Distributed Comput.
Leslie Lamport
1990 J jnl
Concurrent Reading and Writing of Clocks.
ACM Trans. Comput. Syst.
Leslie Lamport
1990 — ch.
Distributed Computing: Models and Methods.
Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B)
Leslie Lamport, Nancy A. Lynch
1989 J jnl
A Simple Approach to Specifying Concurrent Systems.
Commun. ACM
Leslie Lamport
1989 — conf
Composing Specifications.
REX Workshop
Martín Abadi, Leslie Lamport
1989 A* conf
Realizable and Unrealizable Specifications of Reactive Systems.
ICALP
Martín Abadi, Leslie Lamport, Pierre Wolper
1988 A* conf
A Lattice-Structured Proof of a Minimum Spanning.
PODC
Jennifer L. Welch, Leslie Lamport, Nancy A. Lynch
1988 J jnl
Control Predicates are Better than Dummy Variables for Reasoning about Program Control.
ACM Trans. Program. Lang. Syst.
Leslie Lamport
1988 J jnl
On E. W. Dijkstra's position paper on "fairness: ".
ACM SIGSOFT Softw. Eng. Notes
Fred B. Schneider, Leslie Lamport
1988 A* conf
The Existence of Refinement Mappings
LICS
Martín Abadi, Leslie Lamport
1988 — conf
While Waiting for the Millennium: Formal Specification and Verficiation of Concurrent Systems Now (Abstract).
Concurrency
Leslie Lamport
1987 J jnl
A Fast Mutual Exclusion Algorithm.
ACM Trans. Comput. Syst.
Leslie Lamport
1986 J jnl
Byzantine Clock Synchronization.
ACM SIGOPS Oper. Syst. Rev.
Leslie Lamport, P. M. Melliar-Smith
1986 — book
LaTeX: User's Guide & Reference Manual
Leslie Lamport
1986 J jnl
On Interprocess Communication. Part I: Basic Formalism.
Distributed Comput.
Leslie Lamport
1986 J jnl
On Interprocess Communication. Part II: Algorithms.
Distributed Comput.
Leslie Lamport
1986 J jnl
The mutual exclusion problem: part I - a theory of interprocess communication.
J. ACM
Leslie Lamport
1986 J jnl
The mutual exclusion problem: partII - statement and solutions.
J. ACM
Leslie Lamport
1985 A* conf
Constraints: A Uniform Approach to Aliasing and Typing.
POPL
Leslie Lamport, Fred B. Schneider
1985 J jnl
Distributed Snapshots: Determining Global States of Distributed Systems
ACM Trans. Comput. Syst.
K. Mani Chandy, Leslie Lamport
1985 — ed.
Distributed Systems: Methods and Tools for Specification, An Advanced Course, April 3-12, 1984 and April 16-25, 1985, Munich, Germany
Advanced Course: Distributed Systems
Mack W. Alford, Jean-Pierre Ansart, Günter Hommel, Leslie Lamport, Barbara Liskov, Geoff P. Mullery, Fred B. Schneider
1985 J jnl
Solved Problems, Unsolved Problems and Non-Problems in Concurrency.
ACM SIGOPS Oper. Syst. Rev.
Leslie Lamport
1985 J jnl
Synchronizing Clocks in the Presence of Faults
J. ACM
Leslie Lamport, P. M. Melliar-Smith
1985 A* conf
What It Means for a Concurrent Program to Satisfy a Specification: Why No One Has Specified Priority.
POPL
Leslie Lamport
1984 — conf
An Axiomatic Semantics of Concurrent Programming Languages.
Logics and Models of Concurrent Systems
Leslie Lamport
1984 — conf
Basic Concepts.
Advanced Course: Distributed Systems
Mack W. Alford, Leslie Lamport, Geoff P. Mullery
1984 A* conf
Byzantine Clock Synchronization.
PODC
Leslie Lamport, P. M. Melliar-Smith
1984 — conf
Formal Foundation for Specification and Verification.
Advanced Course: Distributed Systems
Leslie Lamport, Fred B. Schneider
1984 — conf
Paradigms for Distributed Programs.
Advanced Course: Distributed Systems
Fred B. Schneider, Leslie Lamport
1984 A* conf
Solved Problems, Unsolved Problems and Non-Problems in Concurrency (Invited Address).
PODC
Leslie Lamport
1984 J jnl
The "Hoare Logic" of CSP, and All That.
ACM Trans. Program. Lang. Syst.
Leslie Lamport, Fred B. Schneider
1984 J jnl
Using Time Instead of Timeout for Fault-Tolerant Distributed Systems.
ACM Trans. Program. Lang. Syst.
Leslie Lamport
1983 — conf
Problems from the Workshop on the Analysis of Concurrent Systems.
The Analysis of Concurrent Systems
Leslie Lamport
1983 A* conf
Reasoning About Nonatomic Operations.
POPL
Leslie Lamport
1983 J jnl
Specifying Concurrent Program Modules.
ACM Trans. Program. Lang. Syst.
Leslie Lamport
1983 J jnl
The Weak Byzantine Generals Problem
J. ACM
Leslie Lamport
1983 — conf
What Good is Temporal Logic?
IFIP Congress
Leslie Lamport
1982 J jnl
An Assertional Correctness Proof of a Distributed Algorithm.
Sci. Comput. Program.
Leslie Lamport
1982 J jnl
Proving Liveness Properties of Concurrent Programs.
ACM Trans. Program. Lang. Syst.
Susan S. Owicki, Leslie Lamport
1982 J jnl
The Byzantine Generals Problem.
ACM Trans. Program. Lang. Syst.
Leslie Lamport, Robert E. Shostak, Marshall C. Pease
1981 J jnl
Password Authentification with Insecure Communication.
Commun. ACM
Leslie Lamport
1981 — conf
Program Logics and Program Verification (position paper).
Logic of Programs
Leslie Lamport, Susan S. Owicki
1981 — conf
TIMESETS -- A New Method for Temporal Reasoning about Programs.
Logic of Programs
Leslie Lamport
1980 A* conf
"Sometime" is Sometimes "Not Never" - On the Temporal Logic of Programs.
POPL
Leslie Lamport
1980 J jnl
Reaching Agreement in the Presence of Faults.
J. ACM
Marshall C. Pease, Robert E. Shostak, Leslie Lamport
1980 J jnl
The 'Hoare Logic' of Concurrent Programs.
Acta Informatica
Leslie Lamport
1979 J jnl
A New Approach to Proving the Correctness of Multiprocess Programs.
ACM Trans. Program. Lang. Syst.
Leslie Lamport
1979 J jnl
A general construction for expressing repetition.
ACM SIGPLAN Notices
Leslie Lamport
1979 J jnl
How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs.
IEEE Trans. Computers
Leslie Lamport
1979 J jnl
On the Proof of Correctness of a Calendar Program.
Commun. ACM
Leslie Lamport
1978 J jnl
On-the-Fly Garbage Collection: An Exercise in Cooperation.
Commun. ACM
Edsger W. Dijkstra, Leslie Lamport, Alain J. Martin, Carel S. Scholten, Elisabeth F. M. Steffens
1978 J jnl
State the problem before describing the solution.
ACM SIGSOFT Softw. Eng. Notes
Leslie Lamport
1978 J jnl
The Implementation of Reliable Distributed Multiprocess Systems.
Comput. Networks
Leslie Lamport
1978 — conf
The specification and proof of correctness of interactive programs.
Mathematical Studies of Information Processing
Leslie Lamport
1978 J jnl
Time, Clocks, and the Ordering of Events in a Distributed System.
Commun. ACM
Leslie Lamport
1977 J jnl
Concurrent Reading and Writing.
Commun. ACM
Leslie Lamport
1977 J jnl
Proving the Correctness of Multiprocess Programs.
IEEE Trans. Software Eng.
Leslie Lamport
1976 J jnl
Comments on "A Synchronization Anomaly".
Inf. Process. Lett.
Leslie Lamport
1976 J jnl
The Synchronization of Independent Processes.
Acta Informatica
Leslie Lamport
1975 J jnl
Multiple Byte Processing with Full-Word Instructions.
Commun. ACM
Leslie Lamport
1975 — conf
On programming parallel computers.
Programming Languages and Compilers for Parallel and Vector Machines
Leslie Lamport
1975 — conf
On-the-fly garbage collection: an exercise in cooperation.
Language Hierarchies and Interfaces
Edsger W. Dijkstra, Leslie Lamport, Alain J. Martin, Carel S. Scholten, Elisabeth F. M. Steffens
1974 J jnl
A New Solution of Dijkstra's Concurrent Programming Problem.
Commun. ACM
Leslie Lamport
1974 — conf
The Hyperplane Method for an Array Computer.
Sagamore Computer Conference
Leslie Lamport
1974 J jnl
The Parallel Execution of DO Loops.
Commun. ACM
Leslie Lamport
1970 J jnl
Comment on Bell's quadratic quotient method for hash coded searching.
Commun. ACM
Leslie Lamport