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

79 points by kalaracey 2y ago ↗ HN

2 comments

[ 76.5 ms ] story [ 406 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?