Isabelle

Web Page: http://isabelle.in.tum.de/gsoc-ideas.html

Mailing List: mailto:isabelle-users@cl.cam.ac.uk

Isabelle is an open source interactive theorem prover to author formal texts ranging from pure mathematics to software where proofs are checked by the machine and 100% logical correctness is guaranteed. Isabelle is mainly developed in Standard ML but incorporates modules written in Perl, Python, and increasingly Scala. We are working on modernizing Isabelle by implementing a new-style non-linear interaction model in Scala/JVM. In the past, we have already successfully adopted efficient multi-core programming. For the future, we intend to integrate further tools (e.g., provers) and enhance the interface and on-line documentation of the system.

Projects

• SML Library for Proof Representation and Manipulation 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