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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
