TLA+ in Isabelle/HOL

davecturner.github.io

79 points by kalaracey 2 years ago · 2 comments

Reader

iamwil 2 years ago

Wait, is it a reimplementation of TLA+ in Isabelle?

smitty1e 2 years ago

"Temporal Logic of Actions", not "Three Letter Acronym".