[isabelle-dev] GSoC with Isabelle Project

[Jasmin Blanchette]

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.

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.

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