Verifying correctness of Haskell programs using the programming language Agda and framework agda2hs
D. Sabharwal (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 – Coach (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
Equational reasoning based verification address some of the limitations of classical testing. The Curry-Howard correspondence shows a direct link between type systems and mathematical logic based proofs. Agda is a language with totality and dependent types which makes use of the CH isomorphism to support equational reasoning in its programs. ‘agda2hs’ attempts to bring this formal verification to the Haskell ecosystem, by providing a translation between Haskell and Agda programs. This project will serve to test the viability of this framework by re-writing the Haskell library ‘Data.Map’ in the subset of Agda defined by agda2hs and verifying properties of various functions in the library using Agda and dependent types.