Practical Verification of the Haskell Ranged-sets Library

Bachelor thesis (2021)

Authors

A.I. Savu Electrical Engineering, Mathematics and Computer Science

Contributors

L.F.B. Escot Programming Languages - EEMCS (mentor)
J.G.H. Cockx Programming Languages - EEMCS (mentor)
Valentin Robu Algorithmics - EEMCS (coach)
Faculty
Electrical Engineering, Mathematics and Computer Science, Electrical Engineering, Mathematics and Computer Science
Copyright: © 2021 Ioana Savu
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

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.