Isabelle Project Ideas
See below for current Isabelle project ideas for Google's Summer of Code 2011. If you have additional ideas, please contact us via
 Sascha Böhme: email boehmes
 Jasmin Christian Blanchette: email blanchette
where email abbreviates (λx. x@in.tum.de).
All project ideas
 Isabelle/jEdit document browser
 Crossplatform installer and package repository based on Scala/JVM
 Isabelle/jEdit repository and project management
 A general proof representation framework
 Deriving class instances in Isabelle
 Levity 2011
 Advanced parser for the Isabelle term language
 Visual tracing facility for the rewriting engine
Isabelle/jEdit document browser
The idea is to integrate Isabelle generated documents (e.g., Isabelle's main reference manuals) into the Isabelle/jEdit Prover IDE, based on formal content of the edited source text and indexes of items in the library. The classic Isabelle document preparation system targets PDFLaTeX, but this is hard to render directly in the JVM/Swing world of jEdit, while preserving the rich metadata and links. Since Isabelle document sources are based on stylized LaTeX with its own embedded language for formal items, it is easier to parse that directly in the manner of Hevea and generate XHTML/CSS, so that the result can be browsed directly in jEdit using the Lobo/Cobra browser (with some hooks implemented in Scala). It is also possible to extend this to include SVG graphics in these documents (for railroad syntax diagrams used in Isabelle manuals).
 Requirements:

 functional programming (e.g., in Scala, Standard ML or Haskell)
 some familiarity with Swing (in Java or Scala) helps
 some familiarity with XHTML/CSS helps
 Mentor:

Makarius Wenzel, Université ParisSud 11, LRI
Crossplatform installer and package repository based on Scala/JVM
Isabelle is deployed uniformly for Linux, Mac OS X, and Windows/Cygwin, pretending all these platforms are in fact some generic Isabelle/POSIX. The main tool for Isabelle system programming is Scala/JVM, together with creative Perl scripts to iron out physical platform differences.
The idea is to augment a generic installer framework like IzPack for the specific requirements of the crossplatform Isabelle distribution. For example, direct JVMbased unpacking of files (as done in IzPack) would lose symlinks and file attributes, especially on Windows, but a piggybacked copy of Cygwin "tar" can do the trick. Further creativity will be required. Some infrastructure for Isabelle package repositories (based on existing IzPack functionality) should be provided as well. Initial JVM launching on Windows (and maybe Mac OS X) will also require attention.
 Requirements:

 basic functional programming in Scala, but other JVM languages are also accepted
 some familiarity with POSIX system programming helps
 some familiarity with Cygwin (on Windows) helps
 Mentor:

Sascha Böhme, Technische Universität München
Isabelle/jEdit repository and project management
The idea is to integrate the Isabelle/jEdit Prover IDE with existing plugins for repository and project management of jEdit, with special focus on Mercurial. This means to get in touch with ongoing development of some jEdit plugins (e.g., HgPlugin and ProjectViewer), and see how they can be fit to the requirements of Isabelle source management. The ultimate goal is to support continuous building of versioned Isabelle theory libraries, but the beginnings will be more modest.
 Requirements:
 Mentor:

Lars Noschinski, Technische Universität München
A general proof representation framework
Automatic theorem provers (such as E, SPASS, Vampire, and Z3) are powerful tools that can sometimes find very long proofs for previously unproved conjectures, but the proofs are by contradiction and are notoriously unreadable.
In the interactive theorem proving world, proofs can be written using nice, blockstructured proof languages (e.g., Mizar and Isar). This project consists of developing a small generic framework to represent proofs as graphs and manipulate them. Typical operations on proof graphs are to recast a proof by contradiction to a direct proof, introduce block structure to cleanly separate independent subproofs, and remove uninteresting proof steps. Many of the pieces are described in the literature or have been done before by various groups, but they are tied to specific provers.
A generic framework would be beneficial to the automatic theorem proving community. It would also help our tool Sledgehammer, a bridge between Isabelle and automatic theorem provers.
 Requirements:

 knowledge of some programming language (e.g., Standard ML, Scala, C++, Java)
 basic familiarity with logic (logical connectives, quantifiers)
 Mentor:

Jasmin Christian Blanchette, Technische Universität München
Deriving class instances in Isabelle
Isabelle provides type classes, as in Haskell, to support adhoc polymorphism. For standard type classes (e.g., "order" and "finite") deriving instances for types is often a straightforward but tedious task. The idea is to automate the process of deriving instances for types, based on the "deriving" mechanism of Haskell.
 Requirements:

 good knowlegde in functional programming (e.g. Standard ML, OCaml or Haskell)
 knowledge of type classes and generic programming is helpful
 knowledge of interactive theorem proving is helpful
 Mentor:

Lukas Bulwahn, Technische Universität München
Levity 2011
In large sets of Isabelle theory files, lemmas, definitions and theorems often end up in the wrong file, because it takes too much proofrerun effort and time to insert them at correct position when they are created. Moving lemmas after the fact by hand again is timeconsuming, occasionally frustrating and mechanical work. The Levity tool automates this process. According to user annotation, it figures out the best position for a lemma or definition to be in, moves it from its source file to the correct destination, and reruns its proof to check if it still works in the changed context. A prototype of this tool exists for Isabelle 2009, but Isabelle's internal API has changed so much since then that a complete redesign and reimplementation is necessary. Moreover, the prototype does not deal correctly with all Isabelle proof contexts such as locales and it is only able to move lemmas, not definitions.
 Requirements:

 functional programming (e.g., Standard ML or Haskell)
 knowledge of interactive theorem proving is helpful
 Mentor:

Gerwin Klein, University of New South Wales
Advanced parser for the Isabelle term language
The logical language of Isabelle is typed lambda calculus with arbitrary userdefined notation. At the bottom of it is an Earley parser written in ML, which is able to handle arbitrary contextfree grammars. Here are some ideas to renovate this important component:
 Provide more information on successful and erroneous parse attempts, e.g. to give immediate feedback about expected syntactic categories.
 Adapt to the parallel Isabelle/ML programming runtime environment, to get the best out of current multicore hardware.
This could mean to reimplement the Earley parser afresh, using contemporary approaches (there are some recent papers on the web).
 Requirements:

 functional programming (e.g. Standard ML)
 some interest in concrete vs. abstract syntax of mathematical languages
 Mentor:

Makarius Wenzel, Université ParisSud 11, LRI
Visual tracing facility for the rewriting engine
The term rewriting engine (called the simplifier) is one of Isabelle's most important tools. Understanding it is quite important, not only for Isabelle beginners to reduce the steep learning curve, but also for regular users, as it is often not obvious how the simplifier reached the final result. At the moment, the simplifier is capable of producing a trace which contains every rewrite step tried, in an unstructured, sequential manner, and does not distinguish between failed and successful steps. A reimplementation should address these issues. Especially, we would like to see rewriting steps visualized in a modern GUI (based on Scala or Java and preferrably integrated with jEdit). The project can be extended in several directions to provide even more information, for example giving explanations why certain rewriting steps could not be performed or which parts of a conjecture are invalidated by a counterexample. There are close connections to debug traces for functional programming languages, e.g., with Hat in Haskell.
 Requirements:

 functional programming (e.g., Standard ML, Haskell or Scala)
 knowledge with GUI programming (especially jEdit) is helpful
 Mentor:

Lars Noschinski, Technische Universität München
Additional ideas
We invite student suggestions for further ideas related to Isabelle. Especially, we welcome ideas for verifying software or proving mathematical theorems within Isabelle. Please contact us via
 Sascha Böhme: email boehmes
 Jasmin Christian Blanchette: email blanchette
where email abbreviates (λx. x@in.tum.de).