[Agda] Proofs about programs explicitly represented in Agda.

[K V S Prasad]

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/