4 ms·
It is be interesting to think of how a checker would work that detects monotonicity & deploys this theorem to check liveness properties. Maybe I'm just describi
by ahelwer 3y ago
It is be interesting to think of how a checker would work that detects monotonicity & deploys this theorem to check liveness properties. Maybe I'm just describing the TLA+ proof language! Also something to bring up at the next monthly TLA+ meeting.