[isabelle-dev] Google Summer of Code: accepted students

Sascha Boehme boehmes at in.tum.de
Tue Apr 26 18:09:54 CEST 2011

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


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

More information about the isabelle-dev mailing list