Practical Verification of the Haskell Ranged-sets Library
A.I. Savu (TU Delft - Electrical Engineering, Mathematics and Computer Science)
L.F.B. Escot – Mentor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
J.G.H. Cockx – Mentor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
V. Robu – Coach (TU Delft - Electrical Engineering, Mathematics and Computer Science)
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
agda2hs is a project that aims to combine the best parts of Haskell and Agda by providing a common subset between them. It allows programmers to im- plement libraries in Agda, verify their correctness and then translate the result to Haskell so they can be used by Haskell programmers. In this paper, a verified Agda implementation of the Ranged-sets Haskell library is provided, using agda2hs. In or- der to produce a verified implementation of this li- brary, we proved its preconditions, invariants and properties.