Abstract

Higher-order features are increasingly popular in modern day programming languages (e.g. Java and C++ recently support lambda expressions). You will study the applicability and adaptation of current verification techniques to the analysis of Haskell code and devise improvements to these algorithms and implementations to meet the new challenges introduced.

Objectives

The compilation process of Haskell programs by the GHC compiler goes via two intermediate steps. First the code is translated into a small functional language called Haskell Core. This code is then compiled into C or LLVM code which is in turn compiled to a binary.

Many verification approaches and techniques have already been successfully applied to the analysis of C programs (e.g. CBMC and Klee amongst others). The initial goal of the project will be to evaluate the performance of these tools on code derived from higher-order Haskell programs.

Due to the specialised and unusual nature of the code produced by the GHC compilation process, it is likely that existing tools will struggle to return meaningful results. However, since the code produced will also follow a uniform and predictable structure it will be amenable to new heuristics which will improve the performance of the analysis tools. The second objective of the project will be to identify, implement, and evaluate these heuristics.

Expected ability of student

The student should have an interest in both theoretical and practical aspects of computer science. They should be comfortable with logical proofs, the basics of higher-order programming, and programming in C. The position is particular suited to a student wishing to continue study to a PhD. level. Candidates may also apply for a fully-funded Microsoft sponsored PhD. project to be supervised by Matthew Hague.