TLA+ in Isabelle/HOL (opens in new tab)

(davecturner.github.io)

79 pointskalaracey2y ago2 comments

2 comments

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

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

j / k navigate · click thread line to collapse

(davecturner.github.io)

79 pointskalaracey2y ago2 comments

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

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

j / k navigate · click thread line to collapse