Master thesis

Isabelle is a proof assistant with a built-in functional programming language. To compile and execute these programs, Isabelle offers code generation to the four target languages ML, OCaml, Haskell and Scala. The thesis is concerned with adding a fifth target language: Go.

Since Go differs widely from the existing targets, there are a few key areas that require special attention, for example generics and algebraic datatypes. With a background in compilers, you should work on finding a suitable mapping of these functional programming constructs to Go features.

    You have experience in, or taken a course on compiler construction.
    Experience with Isabelle is an advantage but not absolutely necessary

Advisor: Lars Hupel

Supervisor: Prof. Tobias Nipkow

Material to read: