[isabelle-dev] GSoC with Isabelle Project
kshanth2101 at gmail.com
Sat Mar 26 00:13:30 CET 2011
On Fri, Mar 25, 2011 at 6:40 PM, Jasmin Blanchette
<jasmin.blanchette at gmail.com> wrote:
> Hi Kishanthan,
> Thanks for your interest!
>> I'm interested in working with isabelle for this google summer of code.
>> I have gone through the ideas list of Isabelle and i'm interested in
>> working on "A general proof representation framework".
>> To be honest i'm fairly new to isabelle. So i would like to take this
>> project as a challenge and do it. I'm confident that ill get to know
>> much more in the due coarse.
> This sounds good. :)
>> Can someone guide me on where to begin and to resources relating the
>> above idea to get a better understanding?
> Here are a few references I know of. First, the paper "Source-level proofs reconstruction for interactive theorem proving" by Paulson and Susanto  lays the foundation for the current implementation in Isabelle, so that would give you a good idea of what we have and what we're trying to achieve.
> Other efforts from other research groups include TRAMP [2,3] and work by Xiaorong Huang .
> In addition, I would suggest you take a look at a few other papers on Sledgehammer  and the Isar proof language . Section 2.2 of  is especially relevant.
Thanks for directing me to some resources.
I'm currently reading these documents and trying to get a better
understanding. I will write back to you whenever i get any questions
> One last tip: One student already contacted me regarding this project and might also apply. Hence, to increase your chances, I would suggest that you also apply for another project from the Isabelle group in addition to this one.
Ok, i will look into other project ideas as well.
> Please let me know if you have further questions.
>  http://www.cl.cam.ac.uk/~lp15/papers/Automation/reconstruction.pdf
>  http://www.ags.uni-sb.de/~omega/software/Tramp/index.html
>  http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.43.2311
>  http://www.springerlink.com/content/y3506683h1433l73/
>  http://www4.in.tum.de/~blanchet/iwil2010-sledgehammer.pdf
>  http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.169.2504&rep=rep1&type=pdf
More information about the isabelle-dev