[isabelle-dev] GSoC with Isabelle Project

[Kishanthan Thangarajah]

Hi Jasmin,

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 [1] 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 [4].
>
> In addition, I would suggest you take a look at a few other papers on Sledgehammer [5] and the Isar proof language [6]. Section 2.2 of [5] 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
regarding this.

> 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.

Thanks,
Kishanthan.
>
> Please let me know if you have further questions.
>
> Regards,
>
> Jasmin
>
> [1] http://www.cl.cam.ac.uk/~lp15/papers/Automation/reconstruction.pdf
> [2] http://www.ags.uni-sb.de/~omega/software/Tramp/index.html
> [3] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.43.2311
> [4] http://www.springerlink.com/content/y3506683h1433l73/
> [5] http://www4.in.tum.de/~blanchet/iwil2010-sledgehammer.pdf
> [6] http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.169.2504&rep=rep1&type=pdf
>
>