[Agda] Proofs about programs explicitly represented in Agda.

[Liam O'Connor]

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.

http://dl.acm.org/citation.cfm?id=2976030

I can supply a preprint if you can’t get the paper from the DL.

Liam

On 17 February 2017 at 12:37:42 am, K V S Prasad (prasad at chalmers.se) wrote:

Hello,  

Following Andreas’ suggestion, I am forwarding my mail below.  

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.  

And advertising our own 20-year old development, I should point out that  

http://ojs.statsbiblioteket.dk/index.php/brics/article/view/19967  

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.  

I would be grateful for any pointers.  

Thanks!  

Kind Regards,  
Prasad  

On 13/Feb/17 18:24, "Andreas Abel" <andreas.abel at cse.gu.se> wrote:  

Hi Prasad,  

I am sure there must be case studies out there like you suggested. This  
is a perfect question for the Agda mailing list.  

https://lists.chalmers.se/mailman/listinfo/agda  

Usually people are quite happy to advertise their developments on  
request. :)  

Best,  
Andreas  

On 13.02.2017 17:54, K V S Prasad wrote:  
> Hi Andreas,  
>  
>  
>  
> Are there examples in the Agda library which represent a (small)  
> programming language, small programs in it, and do proofs about these?  
> Even better if the logic used for the proofs is itself explicitly  
> encoded and used (i.e. use Agda as the meta language, and both the  
> programming language and the logic as object languages).  
>  
>  
>  
> Mvh  
>  
> Prasad  
>  

--  
Andreas Abel <>< Du bist der geliebte Mensch.  

Department of Computer Science and Engineering  
Chalmers and Gothenburg University, Sweden  

andreas.abel at gu.se  
http://www.cse.chalmers.se/~abela/  


_______________________________________________
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/20170217/bccae2ea/attachment.html>