Producing a verified implementation of sequences using agda2hs

Bachelor thesis (2021)

Authors

S. Anand 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 (supervisor 2)
Faculty
Electrical Engineering, Mathematics and Computer Science
Copyright: © 2021 Shashank Anand
Agda2hs Translation Dependent Types Verification
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

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.