We are happy to announce that two students are participating in this year's Google Summer of Code for Isabelle:
Peter Skočovský, working on "Isabelle/jEdit document browser and various enhancements" and mentored by Makarius. Peter is studying in the European Master's program in Computational Logic with frequent changes of location. He spent the winter at TU Dresden, is now at Free University of Bozen-Bolzano and will continue at TU Wien. Here is a short description for his summer occupation in Peter's words: ------------------------------------------- I propose to integrate Isabelle's documentation and the document generation process into Isabelle/jEdit Prover IDE. It will be possible to display the documentation and the documents generated from a source in the IDE with their rich meta-data and links. Further, if there will be enough time, I plan to enhance Isabelle/jEdit Prover IDE with better prover content visualization, source file templates, code templates and completion, automatic indentation, ... ------------------------------------------- and Charles Francis, working on "SML Library for Proof Representation and Manipulation" and mentored by Jasmin. Charles has a BA in Mathematics from Reed College and is going to do his master at Carnegie Mellon under Jeremy Avigad. Here is what Charles proposed to do this summer: ------------------------------------------- The aim of my summer project is to create an SML library to aid in transitioning from machine generated proofs to legible proofs containing justifications at a higher level of abstraction. That is, I propose to develop a graph-based proof representation and manipulation library for the purpose of: 1) automatically improving the legibility of human and machine-generated proofs alike 2) improving the performance of bridges between interactive and automatic theorem provers such as Sledgehammer. ------------------------------------------- We welcome both "on board" and wish them success with their projects. Stay tuned, Jasmin & Sascha _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev