[Agda] TLA+ or LTL in agda ?

Tue Jun 5 06:06:43 CEST 2018

Has anyone thought of implementing tla+ in Agda?

I found Alan Jeffrey's Linear Temporal Logic written in Agda but there is
no mention of concurrency, so I am unsure if LTL is sufficient for
concurrency.

I would like to express in LTL and agda , the Dining Philosophers' problem
or Paxos.

Apart from Alan , has anyone else worked on LTL in agda?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180605/e39b412e/attachment.html>