Practical Verification of Infinite Structures in agda2hs

Bachelor thesis (2022)

Authors

R. Schrijver 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)
Q. Wang Embedded Systems - EEMCS (supervisor 2)
Faculty
Electrical Engineering, Mathematics and Computer Science
Copyright: © 2022 Remco Schrijver
Functional Programming Agda Agda2hs Haskell Infinite structures Copatterns Coinduction
More Info
expand_more

Published Date

27-06-2022

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

Agda allows for writing code that can be mathematically proven and verified to be correct, this type of languages is generally known as a proof assistant. The agda2hs library makes an effort to translate Agda to readable Haskell, in a way the Haskell is still consistent. In previous work it is shown that with the current agda2hs implementation, rudimentary structures can be translated to Haskell from Agda with agda2hs. In this paper the translation and verification of infinite structures to readable Haskell code is researched. This allows for future work to be done on verification of more complex libraries because the concept of infinite structures is used often in Haskell. The results of the research were that translation of rudimentary infinite structures is possible, but functions creating infinite structures cannot be translated at this point in time.