Bachelor Thesis/Master Thesis

Isabelle/HOL is a theorem prover for higher order logic. It offers rich specification, programming and proof languages.

Leon is a verification and synthesis toolkit for Scala programs, developed at EPFL. In recent work, Hupel and Kuncak have implemented a connection between Leon and Isabelle, i.e., Isabelle can be used to prove correctness of Scala programs.

The goal of this thesis is to extend the Leon system with a mechanism to define inductive predicates and sets, and subsequently translate those to Isabelle.

Programming language:
Standard ML and Scala
Prerequisites:
Familiarity with functional programming (e.g., ML, OCaml, Haskell, Lisp); English
Advisor:
Lars Hupel, email {hupel} AT [in.tum.de]
Supervisor:
Prof. Tobias Nipkow, Raum MI 01.11.058, email {nipkow} AT [in.tum.de]