Data structures that associate keys with values (for instance hash maps or balanced search trees) are usually referred to as collections. Collections are an integral component of programming languages, either provided with built-in syntax like in Python (dictionaries) or as core libraries like in Java, Scala or Haskell.
The Agda programming language, in version 2, has been developed at the Chalmers/GU Department of Computer Science and Engineering since 2006. It is a functional programming language with strong type system. Its dependent types allow the programmer to express strong data structure invariants and properties of programs, enabling a correct-by-construction programming style.
Correct-by-construction operations on collections deliver, beyond the desired result values, evidence of correct operation. For instance, a query to look up a key in a collection would not just return the value or an error message, it would also deliver evidence that the delivered value is actually present in the collection or evidence that the key is undefined. As of now (October 2018), the Agda language does not have a collection library that is correct-by-construction.
Design and implement efficient correct-by-construction collections to be integrated into the Agda standard library.
Suggested supervisor: Andreas Abel