Verifying correctness of Haskell programs using the programming language Agda and framework agda2hs

Bachelor thesis (2021)

Authors

D. Sabharwal Electrical Engineering, Mathematics and Computer Science

Contributors

J.G.H. Cockx Programming Languages - EEMCS (supervisor 1)
L.F.B. Escot Programming Languages - EEMCS (supervisor 1)
Valentin Robu Algorithmics - EEMCS (coach)
Faculty
Electrical Engineering, Mathematics and Computer Science
Copyright: © 2021 Dixit Sabharwal
More Info
expand_more

Published Date

01-07-2021

Language

English

Reuse Rights

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.

Faculty

Electrical Engineering, Mathematics and Computer Science

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.