Producing a verified implementation of sequences using agda2hs
S. Anand (TU Delft - Electrical Engineering, Mathematics and Computer Science)
J.G.H. Cockx – Mentor (TU Delft - Programming Languages)
L.F.B. Escot – Mentor (TU Delft - Programming Languages)
Valentin Robu – Graduation committee member (TU Delft - Algorithmics)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
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.