Producing a verified implementation of sequences using agda2hs

Purely functional languages are advantageous in that it is easy to reason about the correctness of functions. Dependently typed programming languages such as Agda enable us to prove properties in the language itself. However, dependently typed programming languages have a steep learning curve and are usable only by expert programmers. The agda2hs project identifies a common subset of Agda and Haskell and translates this subset from Agda to readable Haskell, which enables programmers to write and verify code in Agda, and use it in Haskell. This provides the guarantees of verification to the translated code in Haskell, a language that does not support verification. The objective of this paper is to investigate the possibility of producing a verified implementation of the Haskell library Data.Sequence using the common subset identified by agda2hs. A description of the implementation and verification of Data.Sequence in Agda is provided. A proof technique using arbitrarily nested types is examined in detail. Possible reductions to the cost of the verification process are discussed.CSE3000 Research ProjectComputer Science and Engineerin