Add a verified data structure to the CakeML basis library

Potential supervisors: 
Research groups/keywords: 
Description: 

CakeML

CakeML is an on-going research project that is building a verified implementation of a strict functional programming language, in the style of Standard ML and OCaml. The tools around the language include a verified compiler and tools for program verification in the CakeML language. The CakeML language comes with a standard basis library that contains modules for strings, arithmetic, file I/O etc. These library functions have been verified using the program verification tools mentioned earlier.

Project

This project is about developing the CakeML standard basis library further. Concretely, this project is about adding one or more new modules that contain some useful data structures, e.g. stateful hash maps, or functionality, e.g. search routines. The functions in the module would be verified using the existing program verification tools. Contact Magnus Myreen to discuss potential directions.

Research

Projects in this area will seek to answer research questions such as: What can be verified using the CakeML tools? How far can the CakeML basis library be developed? How can one make data strcture proofs as easy as possible to produce?  

Student

This project requires a solid background in functional programming and a keen interest in logic and data structures.

Suggested background courses:

  •  Functional programming
  •  Testing, Debugging and Verification
  •  Programming Language Technology

There are many modules that can be added to the CakeML basis library, i.e. several students can do projects in this area in parallel.