<div dir="ltr"><div>Liam O'Connor's Applications of Applicative Proof Search [1] might be relevant.<br></div><div><br></div><div>/ Ulf<br></div><div><br></div><div>[1] <a href="https://scholar.google.se/scholar?hl=en&as_sdt=0%2C5&q=Applications+of+applicative+proof+search&btnG=">https://scholar.google.se/scholar?hl=en&as_sdt=0%2C5&q=Applications+of+applicative+proof+search&btnG=</a></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Jun 5, 2018 at 6:06 AM, Apostolis Xekoukoulotakis <span dir="ltr"><<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>Has anyone thought of implementing tla+ in Agda?<br></div><div><br></div><div>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.<br></div><div><br></div><div><br></div><div>I would like to express in LTL and agda , the Dining Philosophers' problem or Paxos.</div><div><br></div><div>Apart from Alan , has anyone else worked on LTL in agda?<br></div></div>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>