Leslie Lamport

Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto: TLA + Proofs. FM 2012: 147-154

Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto: TLA+ Proofs. CoRR abs/1208.5933 (2012)

Leslie Lamport: Euclid Writes an Algorithm: A Fairytale. Int. J. Software and Informatics 5(1-2): 7-20 (2011)

Leslie Lamport: Brief Announcement: Leaderless Byzantine Paxos. DISC 2011: 141-142

Leslie Lamport: Byzantizing Paxos by Refinement. DISC 2011: 211-224

Marcos Kawazoe Aguilera, Eli Gafni, Leslie Lamport: The mailbox problem. Distributed Computing 23(2): 113-134 (2010)

Leslie Lamport, Dahlia Malkhi, Lidong Zhou: Reconfiguring a state machine. SIGACT News 41(1): 63-73 (2010)

Leslie Lamport: Computer Science and State Machines. Concurrency, Compositionality, and Correctness 2010: 60-65

Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz: Verifying Safety Properties with the TLA+ Proof System. IJCAR 2010: 142-148

Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz: The TLA⁺ Proof System: Building a Heterogeneous Verification Platform. ICTAC 2010: 44

Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz: Verifying Safety Properties With the TLA+ Proof System. CoRR abs/1011.2560 (2010)

Leslie Lamport: Teaching concurrency. SIGACT News 40(1): 58-62 (2009)

Leslie Lamport: The PlusCal Algorithm Language. ICTAC 2009: 36-60

Leslie Lamport: TLA+: Whence, Wherefore, and Whither. NASA Formal Methods 2009: 3

Leslie Lamport, Dahlia Malkhi, Lidong Zhou: Vertical paxos and primary-backup replication. PODC 2009: 312-313

Leslie Lamport: Implementing dataflow with threads. Distributed Computing 21(3): 163-181 (2008)

Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz: A TLA+ Proof System. LPAR Workshops 2008

Marcos Kawazoe Aguilera, Eli Gafni, Leslie Lamport: The Mailbox Problem. DISC 2008: 1-15

Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz: A TLA+ Proof System. CoRR abs/0811.1914 (2008)

James E. Johnson, David E. Langworthy, Leslie Lamport, Friedrich H. Vogt: Formal specification of a Web services protocol. J. Log. Algebr. Program. 70(1): 34-52 (2007)

Leslie Lamport: DISC 20th Anniversary: Invited Talk Time, Clocks, and the Ordering of My Ideas About Distributed Systems. DISC 2007: 504

Leslie Lamport: Fast Paxos. Distributed Computing 19(2): 79-103 (2006)

Leslie Lamport: Lower bounds for asynchronous consensus. Distributed Computing 19(2): 104-125 (2006)

Jim Gray, Leslie Lamport: Consensus on transaction commit. ACM Trans. Database Syst. 31(1): 133-160 (2006)

Leslie Lamport: The ⁺CAL Algorithm Language. FORTE 2006: 23

Leslie Lamport: The +CAL Algorithm Language. NCA 2006: 5

Leslie Lamport: Checking a Multithreaded Algorithm with ⁺CAL. DISC 2006: 151-163

Leslie Lamport: Real-Time Model Checking Is Really Simple. CHARME 2005: 162-175

Partha Dutta, Rachid Guerraoui, Leslie Lamport: How Fast Can Eventual Synchrony Lead to Consensus?. DSN 2005: 22-27

James E. Johnson, David E. Langworthy, Leslie Lamport, Friedrich H. Vogt: Formal Specification of a Web Services Protocol. Electr. Notes Theor. Comput. Sci. 105: 147-158 (2004)

Leslie Lamport: Recent Discoveries from Paxos. DSN 2004: 3

Leslie Lamport, Mike Massa: Cheap Paxos. DSN 2004: 307-314

Jim Gray, Leslie Lamport: Consensus on Transaction Commit. CoRR cs.DC/0408036 (2004)

Eli Gafni, Leslie Lamport: Disk Paxos. Distributed Computing 16(1): 1-20 (2003)

Leslie Lamport: Arbitration-free synchronization. Distributed Computing 16(2-3): 219-237 (2003)

Rajeev Joshi, Leslie Lamport, John Matthews, Serdar Tasiran, Mark R. Tuttle, Yuan Yu: Checking Cache-Coherence Protocols with TLA⁺. Formal Methods in System Design 22(2): 125-131 (2003)

Leslie Lamport: Lower Bounds for Asynchronous Consensus. Future Directions in Distributed Computing 2003: 22-23

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

Brannon Batson, Leslie Lamport: High-Level Specifications: Lessons from Industry. FMCO 2002: 242-261

Leslie Lamport: Paxos Made Simple, Fast, and Byzantine. OPODIS 2002: 7-9

Leslie Lamport, John Matthews, Mark R. Tuttle, Yuan Yu: Specifying and verifying systems with TLA+. ACM SIGOPS European Workshop 2002: 45-48

Leslie Lamport: Fairness and hyperfairness. Distributed Computing 13(4): 239-245 (2000)

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)

Leslie Lamport: Distributed algorithms in TLA (abstract). PODC 2000: 3

Eli Gafni, Leslie Lamport: Disk Paxos. DISC 2000: 330-344

Peter B. Ladkin, Leslie Lamport, Bryan Olivier, Denis Roegel: Lazy Caching in TLA. Distributed Computing 12(2-3): 151-174 (1999)

Leslie Lamport, Lawrence C. Paulson: Should your specification language be typed. ACM Trans. Program. Lang. Syst. 21(3): 502-526 (1999)

Yuan Yu, Panagiotis Manolios, Leslie Lamport: Model Checking TLA⁺ Specifications. CHARME 1999: 54-66

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

Leslie Lamport: Proving Possibility Properties. Theor. Comput. Sci. 206(1-2): 341-352 (1998)

Leslie Lamport: The Part-Time Parliament. ACM Trans. Comput. Syst. 16(2): 133-169 (1998)

Ernie Cohen, Leslie Lamport: Reduction in TLA. CONCUR 1998: 317-331

Leslie Lamport: How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor. IEEE Trans. Computers 46(7): 779-782 (1997)

Leslie Lamport: Processes are in the Eye of the Beholder. Theor. Comput. Sci. 179(1-2): 333-351 (1997)

Leslie Lamport: Composition: A Way to Make Proofs Harder. COMPOS 1997: 402-423

Leslie Lamport: Managing Proofs (Abstract). TACAS 1996: 34

Leslie Lamport: Das LaTeX-Handbuch. Addison-Wesley 1995, isbn 978-3-89319-826-9, pp. I-XVIII, 1-325

Martín Abadi, Leslie Lamport: Conjoining Specifications. ACM Trans. Program. Lang. Syst. 17(3): 507-534 (1995)

Leslie Lamport: TLA in Pictures. IEEE Trans. Software Eng. 21(9): 768-775 (1995)

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

Leslie Lamport: How to Write a Long Formula (Short Communication). Formal Asp. Comput. 6(5): 580-584 (1994)

Leslie Lamport: The Temporal Logic of Actions. ACM Trans. Program. Lang. Syst. 16(3): 872-923 (1994)

Martín Abadi, Leslie Lamport: An Old-Fashined Recipe for Real-Time. ACM Trans. Program. Lang. Syst. 16(5): 1543-1571 (1994)

Manfred Broy, Leslie Lamport: The RPC-Memory Specification Problem - Problem Statement. Formal Systems Specification 1994: 1-4

Martín Abadi, Leslie Lamport, Stephan Merz: A TLA Solution to the RPC-Memory Specification Problem. Formal Systems Specification 1994: 21-66

Leslie Lamport: How good is your specification method? FORTE 1994: 289

Leslie Lamport, Stephan Merz: Specifying and Verifying Fault-Tolerant Systems. FTRTFT 1994: 41-76

Martín Abadi, Leslie Lamport: Open Systems in TLA. PODC 1994: 81-90

Martín Abadi, Leslie Lamport: Decomposing Specifications of Concurrent Systems. PROCOMET 1994: 327-340

Leslie Lamport: TLZ. Z User Workshop 1994: 267-268

Martín Abadi, Leslie Lamport: Composing Specifications. ACM Trans. Program. Lang. Syst. 15(1): 73-132 (1993)

Robert P. Kurshan, Leslie Lamport: Verification of a Multiplier: 64 Bits and Beyond. CAV 1993: 166-179

Leslie Lamport: Verification and Specifications of Concurrent Programs. REX School/Symposium 1993: 347-374

Leslie Lamport: Critique of the Lake Arrowhead Three. Distributed Computing 6(1): 65-71 (1992)

Leslie Lamport: Computer-Hindered Verification (Humans Can Do It Too). CAV 1992: 1

Urban Engberg, Peter Grønning, Leslie Lamport: Mechanical Verification of Concurrent Systems with TLA. CAV 1992: 44-55

Leslie Lamport: Hybrid Systems in TLA⁺. Hybrid Systems 1992: 77-102

Urban Engberg, Peter Grønning, Leslie Lamport: Mechanical Verification of Concurrent Systems with TLA. Larch 1992: 86-97

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)

Martín Abadi, Leslie Lamport: The Existence of Refinement Mappings. Theor. Comput. Sci. 82(2): 253-284 (1991)

Martín Abadi, Leslie Lamport: An Old-Fashioned Recipe for Real Time. REX Workshop 1991: 1-27

Leslie Lamport: A Theorem on Atomicity in Distributed Algorithms. Distributed Computing 4: 59-68 (1990)

Leslie Lamport: Concurrent Reading and Writing of Clocks. ACM Trans. Comput. Syst. 8(4): 305-310 (1990)

Leslie Lamport: win and sin: Predicate Transformers for Concurrency. ACM Trans. Program. Lang. Syst. 12(3): 396-428 (1990)

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

Leslie Lamport: A Simple Approach to Specifying Concurrent Systems. Commun. ACM 32(1): 32-45 (1989)

Martín Abadi, Leslie Lamport, Pierre Wolper: Realizable and Unrealizable Specifications of Reactive Systems. ICALP 1989: 1-17

Martín Abadi, Leslie Lamport: Composing Specifications. REX Workshop 1989: 1-41

Leslie Lamport: Control Predicates are Better than Dummy Variables for Reasoning about Program Control. ACM Trans. Program. Lang. Syst. 10(2): 267-281 (1988)

Leslie Lamport: While Waiting for the Millennium: Formal Specification and Verficiation of Concurrent Systems Now (Abstract). Concurrency 1988: 3

Martín Abadi, Leslie Lamport: The Existence of Refinement Mappings. LICS 1988: 165-175

Jennifer L. Welch, Leslie Lamport, Nancy A. Lynch: A Lattice-Structured Proof of a Minimum Spanning. PODC 1988: 28-43

Leslie Lamport: A Fast Mutual Exclusion Algorithm. ACM Trans. Comput. Syst. 5(1): 1-11 (1987)

Leslie Lamport: LaTeX: User's Guide & Reference Manual. Addison-Wesley 1986, isbn 0-201-15790-X

Leslie Lamport: On Interprocess Communication. Part I: Basic Formalism. Distributed Computing 1(2): 77-85 (1986)

Leslie Lamport: On Interprocess Communication. Part II: Algorithms. Distributed Computing 1(2): 86-101 (1986)

Leslie Lamport: The mutual exclusion problem: part I - a theory of interprocess communication. J. ACM 33(2): 313-326 (1986)

Leslie Lamport: The mutual exclusion problem: partII - statement and solutions. J. ACM 33(2): 327-348 (1986)

Leslie Lamport, P. M. Melliar-Smith: Byzantine Clock Synchronization. Operating Systems Review 20(3): 10-16 (1986)

Leslie Lamport, P. M. Melliar-Smith: Synchronizing Clocks in the Presence of Faults. J. ACM 32(1): 52-78 (1985)

Leslie Lamport: Solved Problems, Unsolved Problems and Non-Problems in Concurrency. Operating Systems Review 19(4): 34-44 (1985)

K. Mani Chandy, Leslie Lamport: Distributed Snapshots: Determining Global States of Distributed Systems. ACM Trans. Comput. Syst. 3(1): 63-75 (1985)

Leslie Lamport: What It Means for a Concurrent Program to Satisfy a Specification: Why No One Has Specified Priority. POPL 1985: 78-83

Leslie Lamport, Fred B. Schneider: Constraints: A Uniform Approach to Aliasing and Typing. POPL 1985: 205-216

Mack W. Alford, Jean-Pierre Ansart, Günter Hommel, Leslie Lamport, Barbara Liskov, Geoff P. Mullery, Fred B. Schneider (Eds.): Distributed Systems: Methods and Tools for Specification, An Advanced Course, April 3-12, 1984 and April 16-25, 1985 Munich. Lecture Notes in Computer Science 190, Springer 1985, isbn 3-540-15216-4

Leslie Lamport: Using Time Instead of Timeout for Fault-Tolerant Distributed Systems. ACM Trans. Program. Lang. Syst. 6(2): 254-280 (1984)

Leslie Lamport, Fred B. Schneider: The ``Hoare Logic'' of CSP, and All That. ACM Trans. Program. Lang. Syst. 6(2): 281-296 (1984)

Mack W. Alford, Leslie Lamport, Geoff P. Mullery: Basic Concepts. Advanced Course: Distributed Systems 1984: 7-43

Leslie Lamport, Fred B. Schneider: Formal Foundation for Specification and Verification. Advanced Course: Distributed Systems 1984: 203-285

Fred B. Schneider, Leslie Lamport: Paradigms for Distributed Programs. Advanced Course: Distributed Systems 1984: 431-480

Leslie Lamport: Solved Problems, Unsolved Problems and Non-Problems in Concurrency (Invited Address). PODC 1984: 1-11

Leslie Lamport, P. M. Melliar-Smith: Byzantine Clock Synchronization. PODC 1984: 68-74

Leslie Lamport: The Weak Byzantine Generals Problem. J. ACM 30(3): 668-676 (1983)

Leslie Lamport: Specifying Concurrent Program Modules. ACM Trans. Program. Lang. Syst. 5(2): 190-222 (1983)

Leslie Lamport: Problems from the Workshop on the Analysis of Concurrent Systems. The Analysis of Concurrent Systems 1983: 252-270

Leslie Lamport: What Good is Temporal Logic? IFIP Congress 1983: 657-668

Leslie Lamport: Reasoning About Nonatomic Operations. POPL 1983: 28-37

Leslie Lamport: An Assertional Correctness Proof of a Distributed Algorithm. Sci. Comput. Program. 2(3): 175-206 (1982)

Leslie Lamport, Robert E. Shostak, Marshall C. Pease: The Byzantine Generals Problem. ACM Trans. Program. Lang. Syst. 4(3): 382-401 (1982)

Susan S. Owicki, Leslie Lamport: Proving Liveness Properties of Concurrent Programs. ACM Trans. Program. Lang. Syst. 4(3): 455-495 (1982)

Leslie Lamport: Password Authentification with Insecure Communication. Commun. ACM 24(11): 770-772 (1981)

Leslie Lamport: TIMESETS -- A New Method for Temporal Reasoning about Programs. Logic of Programs 1981: 177-196

Leslie Lamport, Susan S. Owicki: Program Logics and Program Verification (position paper). Logic of Programs 1981: 197-199

Leslie Lamport: The `Hoare Logic' of Concurrent Programs. Acta Inf. 14: 21-37 (1980)

Marshall C. Pease, Robert E. Shostak, Leslie Lamport: Reaching Agreement in the Presence of Faults. J. ACM 27(2): 228-234 (1980)

Leslie Lamport: ``Sometime'' is Sometimes ``Not Never'' - On the Temporal Logic of Programs. POPL 1980: 174-185

Leslie Lamport: On the Proof of Correctness of a Calendar Program. Commun. ACM 22(10): 554-556 (1979)

Leslie Lamport: How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs. IEEE Trans. Computers 28(9): 690-691 (1979)

Leslie Lamport: A New Approach to Proving the Correctness of Multiprocess Programs. ACM Trans. Program. Lang. Syst. 1(1): 84-97 (1979)

Leslie Lamport: Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM 21(7): 558-565 (1978)

Edsger W. Dijkstra, Leslie Lamport, Alain J. Martin, Carel S. Scholten, Elisabeth F. M. Steffens: On-the-Fly Garbage Collection: An Exercise in Cooperation. Commun. ACM 21(11): 966-975 (1978)

Leslie Lamport: The Implementation of Reliable Distributed Multiprocess Systems. Computer Networks 2: 95-114 (1978)

Leslie Lamport: The specification and proof of correctness of interactive programs. Mathematical Studies of Information Processing 1978: 474-537

Leslie Lamport: Concurrent Reading and Writing. Commun. ACM 20(11): 806-811 (1977)

Leslie Lamport: Proving the Correctness of Multiprocess Programs. IEEE Trans. Software Eng. 3(2): 125-143 (1977)

Leslie Lamport: The Synchronization of Independent Processes. Acta Inf. 7: 15-34 (1976)

Leslie Lamport: Comments on "A Synchronization Anomaly". Inf. Process. Lett. 4(4): 88-89 (1976)

Leslie Lamport: Multiple Byte Processing with Full-Word Instructions. Commun. ACM 18(8): 471-475 (1975)

Edsger W. Dijkstra, Leslie Lamport, Alain J. Martin, Carel S. Scholten, Elisabeth F. M. Steffens: On-the-fly garbage collection: an exercise in cooperation. Language Hierarchies and Interfaces 1975: 43-56

Leslie Lamport: The Parallel Execution of DO Loops. Commun. ACM 17(2): 83-93 (1974)

Leslie Lamport: A New Solution of Dijkstra's Concurrent Programming Problem. Commun. ACM 17(8): 453-455 (1974)

Leslie Lamport: The Hyperplane Method for an Array Computer. Sagamore Computer Conference 1974: 113-131

Leslie Lamport: Comment on Bell's quadratic quotient method for hash coded searching. Commun. ACM 13(9): 573-574 (1970)