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.
Prerequisites:
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