Agda implementation of collections

Potential supervisors: 
Description: 

Background

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.

Task

Design and implement efficient correct-by-construction collections to be integrated into the Agda standard library.

Prerequisites

* Strong interest in dependently-typed programming
* Strong interest in mathematical correctness proofs of programs
* Good functional programming skills
* DAT350/DIT232 Types for Proofs and Programs

Contact: Andreas Abel

References

* Agda on github.
* Agda standard library on github.
* Andreas Abel, Agda tutorial on binary search trees, 2016.
* Conor McBride, How to keep your neighbors in order, ICFP 2014.  (Paper is hard to understand; the basic idea is simple and explained in my tutorial code.)
 

 

Date range: 
October, 2018 to October, 2023