This Web page describes my encoding of Lamport's Temporal Logic of Actions in the higher-order logic of the generic interactive proof assistant Isabelle.


Since Isabelle98, TLA has been included with the standard distribution of Isabelle. To avoid versioning problems, it is therefore no longer available for separate download.


Isabelle/TLA is based on a complete axiomatization of the "raw" (stuttering-sensitive) variant of TLA. Here are two notes on the design of the prover and on a completeness proof for the underlying axiom system.

You may also browse the HTML documentation for the various theories.

The distribution contains a few examples, including

Please let me know about any comments or suggestions.

Stephan Merz