Practical Verification of Infinite Structures in agda2hs

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.https://github.com/RemcoSchrijver/verification-of-infinite-structures/tree/paper_reference_1 GitHub code repository regarding this Bachelor thesis.CSE3000 Research ProjectComputer Science and Engineerin