Verified JSON Parsing in CakeML

Picture of Michael Norrish

22 May 2023

JSON parsing is a standard and important facility used in many programming languages. This project requires the student to implement verified JSON-parsing for the CakeML programming language.

This requires a great deal more than “simple” programming. In particular, a formal specification of the format is required, followed by the implementation of code that is proved to correctly parse the format. (One might also desire good error-reports if the data is malformed.) Finally, it is also important to be able to stream JSON values from input sources so that entire JSON values (e.g., lists of records) need not be parsed and stored in memory at one time. Instead, it should be possible to process JSON incrementally.

This project requires experience in functional programming (e.g. Haskell), and a strong interest in software verification (see COMP1600). This would suit an Honours project student, or (perhaps) a student doing COMP3770.

You are on Aboriginal land.

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.

arrow-left bars search times arrow-up