[isabelle-dev] GSoC with Isabelle Project
jasmin.blanchette at gmail.com
Fri Mar 25 14:10:55 CET 2011
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.
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.
More information about the isabelle-dev