[POPLmark] The purpose of challenge problems?

[Jesper Bengtson]

Benjamin Pierce wrote:

>Continuing a previous discussion... :-)
>
>  
>
>>It's struck me that there's been a bit of a disconnect in the last
>>week's discussion of new challenge problems.  I think the issue is  
>>that
>>we are not in agreement as to their purpose.  So I'd like to ask the
>>question, what is the purpose to a new challenge problem?
>>    
>>
>
>For me, there are two main motivations for thinking about new  
>challenge problems:
>
>1) Several people (Randy Pollack, for example) have made the point  
>that, in some sense, the POPLMark challenge as it stands may be too  
>*easy*.  Although it's got non-trivial binding problems and some  
>slightly intricate inductive proofs, there may be other binding  
>situations (dependent records have been mentioned as an example,  
>IIRC) that will stress terms-with-binding representation strategies  
>significantly harder than Fsub does.  Since representation of binding  
>keeps appearing as a key issue in formalizing POPL-like proofs, this  
>would be nice to know more about.
>
>2) Looking beyond variable binding, one might wonder how various  
>proof assistants fare on a broad range of tasks that come up in POPL- 
>ish reasoning.  Inductive proofs are the bread and butter, which is  
>why the original POPLMark  Challenge focused there, but one also  
>wants to know that one's assistant will be good for co-induction,  
>logical relations arguments, combinatorial reasoning involving  
>significant numerical manipulations, algebra, etc., etc.
>
>Of the two, (1) is both more immediate and better delimited, so  
>perhaps it is good to focus there.  But it would be even nicer to  
>identify problems with aspects of both 1 and 2 -- this was the reason  
>for thinking about things like pi-calculus.
>
>  
>
I have just finished formalising the pi-calculus in Isabelle using 
nominal logic. I have proven so far that strong equivalence is a 
congruence and that it preserves the rules for structural congruence, 
i.e. if two processes are structurally congruent then they are also 
strongly equivalent (and strongly bisimilar). Similar work has been done 
in Coq and Isabelle/HOL.

Bisimulation is defined coinductively but the core of all bisimulation 
proofs is done on a simulation level. Once simulation in one direction 
is proven, a coinductive argument can be applied and the symetric 
version of the bisimulation proof can be inferred automatically.

The sources can be found at http://www.it.uu.se/katalog/jesperb/pi.html

It is a bit difficult to find small well contained challenge problems 
for the pi-calculus. My next challenge will be proving that weak 
equivalence is a congruence and see how well my theories for strong 
equivalence apply here. Another challenge is including support for 
defining processes recursively so that the theorem prover can be used 
for actual model checking. Modelling the polyadic pi-calculus where 
lists of bound names can be sent and received across channels could also 
be a challenge.

Best regards

/Jesper