Isabelle/TLA

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.

Downloading

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.

Documentation

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

the increment example from Lamport's TLA paper
the proof of the RPC-Memory case study, which is described in a paper by Abadi, Lamport, and Merz.

Please let me know about any comments or suggestions.

Stephan Merz