TLA+ in Isabelle/HOL (davecturner.github.io)

79 points by kalaracey 2y ago ↗ HN

2 comments

[ 4.1 ms ] story [ 16.2 ms ] thread

smitty1e 2y ago ↗

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

iamwil 2y ago ↗

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