Practical Verification of Infinite Structures in agda2hs

Title

Practical Verification of Infinite Structures in agda2hs

 Author

Schrijver, Remco (TU Delft Electrical Engineering, Mathematics and Computer Science)

Contributor

Cockx, J.G.H. (mentor)
Escot, L.F.B. (mentor)
Wang, Q. (graduation committee) ORCID 0000-0003-0950-1111

 Degree granting institution

Delft University of Technology

 Programme

Computer Science and Engineering

 Project

CSE3000 Research Project

 Date

2022-06-27

 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.

 Subject

Functional Programming
Agda
agda2hs
Haskell
infinite structures
Copatterns
Coinduction

 To reference this document use:

http://resolver.tudelft.nl/uuid:241b1dde-302d-4aae-8891-f328c36e2b36

 Bibliographical note

https://github.com/RemcoSchrijver/verification-of-infinite-structures/tree/paper_reference_1 GitHub code repository regarding this Bachelor thesis.

 Part of collection

Student theses

 Document type

bachelor thesis

 Rights

© 2022 Remco Schrijver
Files
PDF CSE_3000_Final_Report_final.pdf 232.09 KB
Close viewer