Practical Verification of Infinite Structures in agda2hs
R. Schrijver (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Jesper Cockx – Mentor (TU Delft - Programming Languages)
L.F.B. Escot – Mentor (TU Delft - Programming Languages)
Qing Wang – Graduation committee member (TU Delft - Embedded Systems)
More Info
expand_more
GitHub code repository regarding this Bachelor thesis.
https://github.com/RemcoSchrijver/verification-of-infinite-structures/tree/paper_reference_1Other 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.
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.