Tla Plus Resources Save

TLA+ Reading and Resource List

Last updated 13 January 2018. Beginner-friendly (hopefully!) resources for learning TLA+/personal reading list. This leans heavily on Leslie Lamport's TLA homepage.

Learning it:

• Hyperbook: Downloads as a .zip; last updated August 2015

  "This is the start of a hypertext "book" containing two tutorials: Principles of Concurrent Computing and Specification of Concurrent Systems. The tutorials are two tracks that share much text--especially at the beginning. Both tutorials are based on TLA+. The Principles track, which I hope will eventually be suitable for an undergraduate course on concurrent computing, will mainly use the PlusCal algorithm language rather than TLA+ for describing algorithms. There is also a TLA+ Proof track that explains how to use the TLAPS proof system."

• TLA video course: Video course that assumes basic programming knowledge and some math. Downloads and complete transcripts are available; last updated December 2017.
• Specifying Systems: By Leslie Lamport; link to order through publisher or download for personal use (license details at the download page).
• Learn TLA website
  • TLA+ Toolbox is the IDE that Learn TLA recommends
• Dr. TLA+: Lectures on algorithms and TLA+ implementation
• TLA+ in Practice and Theory: Four-part video lecture series on math and design principles/concepts used in TLA+

Papers/Examples

• AWS and TLA+
• Leslie Lamport papers
  • Euclid Writes a Fairytale
• Examples on GitHub

Community Resources

• Google usergroup
• TLAPlus on Twitter

Misc

• Leslie Lamport at Heidelberg

  "An algorithm is not a program, so why describe it with a programming language? PlusCal is a tiny toy-like language that is infinitely more expressive than any programming language because an expression can be any mathematical formula."

• Leslie Lamport at Microsoft: "Thinking Above the Code"
• Don Knuth: "The Analysis of Algorithms"
• Learning PlusCal