Provably Correct Key-Value Maps in Agda - Leveraging Membership to Reach Correctness

Abstract

This thesis describes the interface and implementation of a provably correct finite map in the Agda programming language. Finite maps are fundamental data structures in computer science, and existing finite maps in Agda can be improved in terms of correctness and some implementation details. We present an extension of ‘A Theory of Finite Maps’ (Collins & Syme, 1995) and an Agda formalisation of that extended theory. The formalisation is designed to be structure agnostic, allowing for many underlying implementations, and its flexibility is demonstrated through a proof-of-concept simply typed lambda calculus interpreter. The core of the formalisation is implemented and proven for AVL trees, extending the Agda standard library with additional proofs and operations. Among these are laws defining the behaviour of delete and unionWith as well as an alternative unionWith implementation. The implementation is also differentiated from the standard library by using erasure to remove, among other things, ordering proofs from the tree data type and operations. The performance of our implementation is compared to the standard library and the results show no meaningful performance gains for our implementation. Finally, we discuss the inclusion of correct-by-construction membership properties in the tree structure itself. Such properties have not been introduced in our implementation. This is due to the constant need to update each proof on every operation on the collection, since any operation that modifies the structure of the tree may cause a proof to become irrelevant for the new map.