<html><head><style>body{font-family:Helvetica,Arial;font-size:13px}</style></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div id="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;">These programs may be a little too simple, but my TyDe paper last year did embed a GCL/Promela-style language in Agda and proved some properties of Peterson’s algorithm using a heavily restricted subset of CTL and a tiny model checker running in the type system.</div><div id="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;"><br></div><div id="bloop_customfont" style="font-family:Helvetica,Arial;font-size:13px; color: rgba(0,0,0,1.0); margin: 0px; line-height: auto;"><a href="http://dl.acm.org/citation.cfm?id=2976030">http://dl.acm.org/citation.cfm?id=2976030</a></div> <br> <div id="bloop_sign_1487269155871794944" class="bloop_sign">I can supply a preprint if you can’t get the paper from the DL.</div><div id="bloop_sign_1487269155871794944" class="bloop_sign"><br></div><div id="bloop_sign_1487269155871794944" class="bloop_sign">Liam</div> <br><p class="airmail_on">On 17 February 2017 at 12:37:42 am, K V S Prasad (<a href="mailto:prasad@chalmers.se">prasad@chalmers.se</a>) wrote:</p> <blockquote type="cite" class="clean_bq"><span><div><div></div><div>Hello,
<br>
<br>Following Andreas’ suggestion, I am forwarding my mail below.
<br>
<br>I am looking for proofs about simple programs, where the programming language is an object language explicitly represented in Agda (the metalanguage). The proof can be carried out in Agda, or better, in a logic which again is explicitly represented in Agda. Our plan is to modify such work for a student project aiming to prove facts about programs in a subset of Promela (a modelling language for concurrent programs), using LTL (linear temporal logic). We are happy to swap Promela or LTL for more tractable languages.
<br>
<br> And advertising our own 20-year old development, I should point out that
<br>
<br>http://ojs.statsbiblioteket.dk/index.php/brics/article/view/19967
<br>
<br>not only partially fulfils the requirements above, it was also the first (as far as we know) proof of an executable concurrent program with data-dependent behavior. (That requires either that you regard an Agda program as executable or that you accept the indeed running Haskell program as “the same” as that represented in Agda). So I am also looking for other such examples.
<br>
<br>I would be grateful for any pointers.
<br>
<br>Thanks!
<br>
<br>Kind Regards,
<br>Prasad
<br>
<br>On 13/Feb/17 18:24, "Andreas Abel" <andreas.abel@cse.gu.se> wrote:
<br>
<br> Hi Prasad,
<br>
<br> I am sure there must be case studies out there like you suggested. This
<br> is a perfect question for the Agda mailing list.
<br>
<br> https://lists.chalmers.se/mailman/listinfo/agda
<br>
<br> Usually people are quite happy to advertise their developments on
<br> request. :)
<br>
<br> Best,
<br> Andreas
<br>
<br> On 13.02.2017 17:54, K V S Prasad wrote:
<br> > Hi Andreas,
<br> >
<br> >
<br> >
<br> > Are there examples in the Agda library which represent a (small)
<br> > programming language, small programs in it, and do proofs about these?
<br> > Even better if the logic used for the proofs is itself explicitly
<br> > encoded and used (i.e. use Agda as the meta language, and both the
<br> > programming language and the logic as object languages).
<br> >
<br> >
<br> >
<br> > Mvh
<br> >
<br> > Prasad
<br> >
<br>
<br> --
<br> Andreas Abel <>< Du bist der geliebte Mensch.
<br>
<br> Department of Computer Science and Engineering
<br> Chalmers and Gothenburg University, Sweden
<br>
<br> andreas.abel@gu.se
<br> http://www.cse.chalmers.se/~abela/
<br>
<br>
<br>_______________________________________________<br>Agda mailing list<br>Agda@lists.chalmers.se<br>https://lists.chalmers.se/mailman/listinfo/agda<br></div></div></span></blockquote></body></html>