[Agda] TLA+ or LTL in agda ?

[Ulf Norell]

Liam O'Connor's Applications of Applicative Proof Search [1] might be
relevant.

/ Ulf

[1]
https://scholar.google.se/scholar?hl=en&as_sdt=0%2C5&q=Applications+of+applicative+proof+search&btnG=

On Tue, Jun 5, 2018 at 6:06 AM, Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:

> 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?
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180605/2472a173/attachment.html>