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

where email abbreviates (λx. x@in.tum.de).

All project ideas

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 PDF-LaTeX, but this is hard to render directly in the JVM/Swing world of jEdit, while preserving the rich meta-data 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é Paris-Sud 11, LRI

back to top

Cross-platform 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 cross-platform Isabelle distribution. For example, direct JVM-based unpacking of files (as done in IzPack) would lose symlinks and file attributes, especially on Windows, but a piggy-backed 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

back to top

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:
  • basic functional programming in Scala, but other JVM languages are also accepted
  • some familiarity with distributed version control systems helps (e.g., Git, Bazaar, Mercurial)
Mentor:

Lars Noschinski, Technische Universität München

back to top

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, block-structured 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

back to top

Deriving class instances in Isabelle

Isabelle provides type classes, as in Haskell, to support ad-hoc 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

back to top

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 proof-rerun effort and time to insert them at correct position when they are created. Moving lemmas after the fact by hand again is time-consuming, 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 re-runs 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

back to top

Advanced parser for the Isabelle term language

The logical language of Isabelle is typed lambda calculus with arbitrary user-defined notation. At the bottom of it is an Earley parser written in ML, which is able to handle arbitrary context-free grammars. Here are some ideas to renovate this important component:

This could mean to re-implement 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é Paris-Sud 11, LRI

back to top

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

back to top

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

where email abbreviates (λx. x@in.tum.de).

back to top